idriserasurequantitative-types

Erased arguments in type constructors


What does it mean to erase an argument in a type constructor? For example

data Foo : (0 _ : Nat) -> Type where

as opposed to

data Foo : Nat -> Type where

My understanding is that nothing in a type constructor is used at runtime anyway, so it's effectively always 0. I guess it also leads to the perhaps more confusing question of what would a linear argument mean in a type constructor, but that's for another day.


Solution

  • Idris (2) is somewhat unusual in that it allows direct pattern matching on types. Type constructors are treated as Type's constructors.

    finSize : Type -> Maybe Nat
    finSize (Fin n) = Just n
    finSize _       = Nothing
    

    If you, say, erased Fin's argument, then matching against a Type with Fin n would make n erased, too.

    data Fin : (0 _ : Nat) -> Type where
    
    -- fails
    -- finSize : Type -> Maybe Nat
    -- finSize (Fin n) = Just n  -- have 0 copies of n, need at least 1
    -- finSize _       = Nothing
    -- succeeds
    data Erased : Type -> Type where Erase : (0 _ : a) -> Erased a
    finSize : Type -> Maybe (Erased Nat)
    finSize (Fin n) = Just (Erase n)
    finSize _       = Nothing