17

根据我对依赖类型的了解，我认为这应该是可能的，但我以前从未见过依赖类型语言的例子，所以我不确定从哪里开始。

我想要的是表单的功能：

f : [Int] -> (Int -> Bool)
f : [Int] -> (Int -> Int -> Bool)
f : [Int] -> (Int -> Int -> Int -> Bool)

ETC...

此函数接受一个 n 列表Ints，并返回一个以 Ints 作为参数的元数 n 的谓词函数。这种事情在依赖类型语言中是可能的吗？这样的事情将如何实施？

4

2 回答 2

21
于 2014-08-21T02:59:19.067 回答
12

@Vitus 已经提出了使用依赖类型的 Agda 解决方案。在这里，我评论的是 Haskell，因为您添加了它的标签。

在 Haskell 中，我们没有像在 Agda 中那样的依赖类型，所以我们不能length l在类型中写入。然而，我们可以使用自定义列表 GADT，它使用 Peano naturals 在类型级别公开列表的长度。

data Z
data S n

data List n a where
   Nil :: List Z a
   Cons :: a -> List n a -> List (S n) a

然后，我们可以使用类型族来计算(a -> a -> ... -> Bool)具有n参数的类型，其中n是给定的类型级别自然。

type family Fun n a
type instance Fun Z     a = Bool
type instance Fun (S n) a = a -> Fun n a

这是你如何使用它。下面将列表与提供的“参数列表”进行比较。

equalityTest :: Eq a => List n a -> Fun n a
equalityTest = go True
  where go :: Eq a => Bool -> List n a -> Fun n a
        go b Nil = b
        go b (Cons x xs) = \y -> go (x==y && b) xs

-- *ListGADT> equalityTest (Cons 1 (Cons 2 Nil)) 1 2
-- True
-- *ListGADT> equalityTest (Cons 1 (Cons 2 Nil)) 1 3
-- False
于 2014-08-21T09:28:05.037 回答