9

所以，我终于找到了一个可以使用新DataKinds扩展的任务（使用 ghc 7.4.1）。这是Vec我正在使用的：

data Nat = Z | S Nat deriving (Eq, Show)

data Vec :: Nat -> * -> * where
    Nil :: Vec Z a
    Cons :: a -> Vec n a -> Vec (S n) a

现在，为方便起见，我想实现fromList. 简单的递归/折叠基本上没有问题——但我不知道如何给它正确的类型。作为参考，这是 Agda 版本：

fromList : ∀ {a} {A : Set a} → (xs : List A) → Vec A (List.length xs)

我的 Haskell 方法，使用我在这里看到的语法：

fromList :: (ls :: [a]) -> Vec (length ls) a
fromList [] = Nil 
fromList (x:xs) = Cons x (fromList xs)

这给了我一个parse error on input 'a'. 我发现的语法是正确的，还是他们改变了它？我还在链接的代码中添加了一些更多的扩展，这也没有帮助（目前我有GADTs, DataKinds, KindSignatures, TypeOperators, TypeFamilies, UndecidableInstances）。

我的另一个怀疑是我不能绑定多态类型，但我对此进行了测试：

bla :: (n :: Nat) -> a -> Vec (S n) a
bla = undefined

也失败了Kind mis-match Expected kind 'ArgKind', but 'n' has kind 'Nat'（不知道那是什么意思）。

任何人都可以帮助我提供一个工作版本fromList并澄清其他问题吗？不幸的是，DataKinds它的文档还没有很好，并且似乎假设每个使用它的人都具有深厚的类型理论知识。

4

3 回答 3

10

与 Agda 不同，Haskell 没有依赖类型，因此无法完全按照您的意愿行事。类型不能通过值参数化，因为 Haskell 强制在运行时和编译时之间进行阶段区分。概念上的工作方式DataKinds实际上非常简单：将数据类型提升为种类（类型的类型），并将数据构造函数提升为类型。 

 fromList :: (ls :: [a]) -> Vec (length ls) a

有几个问题：(ls :: [a])没有真正意义（至少当您只是通过提升伪造依赖类型时），并且length是类型变量而不是类型函数。你想说的是

 fromList :: [a] -> Vec ??? a

???列表的长度在哪里。问题是您无法在编译时获取列表的长度......所以我们可以尝试

 fromList :: [a] -> Vec len a

但这是错误的，因为它说fromList可以返回任意长度的列表。相反，我们想说的是

 fromList :: exists len. [a] -> Vec len a

但 Haskell 不支持这一点。反而

 data VecAnyLength a where
     VecAnyLength :: Vec len a -> VecAnyLength a 

 cons a (VecAnyLength v) = VecAnyLength (Cons a v)

 fromList :: [a] -> VecAnyLength a
 fromList []     = VecAnyLength Nil
 fromList (x:xs) = cons x (fromList xs)

您实际上可以使用VecAnyLengthby 模式匹配，从而获得（本地）伪依赖类型的值。

相似地，

bla :: (n :: Nat) -> a -> Vec (S n) a

不起作用，因为 Haskell 函数只能采用 kind 参数*。相反，您可以尝试

data HNat :: Nat -> * where
   Zero :: HNat Z
   Succ :: HNat n -> HNat (S n)

bla :: HNat n -> a -> Ven (S n) a

这甚至是可以定义的

bla Zero a     = Cons a Nil
bla (Succ n) a = Cons a (bla n a)
于 2012-06-28T11:50:31.653 回答
4

您可以在这里使用一些类型类魔法（更多信息请参见HList）：

{-# LANGUAGE GADTs, KindSignatures, DataKinds, FlexibleInstances
  , NoMonomorphismRestriction, FlexibleContexts #-}

data Nat = Z | S Nat deriving (Eq, Show)

data Vec :: Nat -> * -> * where
  Nil :: Vec Z a
  Cons :: a -> Vec n a -> Vec (S n) a

instance Show (Vec Z a) where
  show Nil = "."

instance (Show a, Show (Vec m a)) => Show (Vec (S m) a) where
  show (Cons x xs) = show x ++ " " ++ show xs

class FromList m where
  fromList :: [a] -> Vec m a

instance FromList Z where
  fromList [] = Nil

instance FromList n => FromList (S n) where
  fromList (x:xs) = Cons x $ fromList xs

t5 = fromList [1, 2, 3, 4, 5]

但这并不能真正解决问题：

> :t t5
t5 :: (Num a, FromList m) => Vec m a

列表是在运行时形成的，它们的长度在编译时是未知的，因此编译器无法推断 的类型t5，必须明确指定：

*Main> t5

<interactive>:99:1:
    Ambiguous type variable `m0' in the constraint:
      (FromList m0) arising from a use of `t5'
    Probable fix: add a type signature that fixes these type variable(s)
    In the expression: t5
    In an equation for `it': it = t5
*Main> t5 :: Vec 'Z Int
*** Exception: /tmp/d.hs:20:3-19: Non-exhaustive patterns in function fromList

*Main> t5 :: Vec ('S ('S ('S 'Z))) Int
1 2 3 *** Exception: /tmp/d.hs:20:3-19: Non-exhaustive patterns in function fromList

*Main> t5 :: Vec ('S ('S ('S ('S ('S 'Z))))) Int
1 2 3 4 5 .
*Main> t5 :: Vec ('S ('S ('S ('S ('S ('S ('S 'Z))))))) Int
1 2 3 4 5 *** Exception: /tmp/d.hs:23:3-40: Non-exhaustive patterns in function fromList

具有依赖类型的语言都有术语到类型的映射，类型也可以在运行时动态形成，所以不存在这个问题。

于 2012-06-28T13:09:23.493 回答
0

在以前的答案之上：

  • 价值水平，从[a]到exist n. Vec n a

  • value to typed value, from [a]to Vec 5 a，您必须在其中提供特定的n.

第一次变换的变体，就像

reify :: [a] -> (forall (n::Nat). Proxy n -> Vec n a -> w) -> w
reify [] k = k (Proxy @ 'Z) Nil
reify (x:xs) k = reify xs (\(_ :: Proxy n) v -> k (Proxy @ ('S n)) (Cons x v))

它仍然从一个值变为一个（静态）量化[a]的类型化值。这类似于方法，没有引入实际的数据类型来执行量化。Vec n anVecAnyLength

这里proxy是明确的nas a Nat。它可以从代码中删除并n保持沉默，仅出现在 typeVec n a中，而不像在Proxy @ ('S n).

于 2019-01-10T10:39:24.237 回答