主页 / coding / 问题 / 77851992
Accepted
joel
Asked: 2024-01-21 01:23:27 +0800 CST

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

  • 772

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

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

相对于

data Foo : Nat -> Type where

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

idris

1 个回答

  1. Best Answer

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

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

    比如说，如果你擦除了 的Fin参数，那么与Typewith匹配也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
    • 1

相关问题