删除类型构造函数中的参数

Question

删除类型构造函数中的参数意味着什么？例如

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

相对于

data Foo : Nat -> Type where

我的理解是，类型构造函数中的任何内容都不会在运行时使用，因此它实际上始终为 0。我想这也会导致一个可能更令人困惑的问题：线性参数在类型构造函数中意味着什么，但那是另一天的事了.

Answer 1

Idris (2) 有点不寻常，因为它允许对类型进行直接模式匹配。类型构造函数被视为 作为

Type

的构造函数。

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

如果你删除了

Fin

的参数，那么用

Type

匹配

Fin n

也会使

n

被删除。

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