相关疑难解决方法(0)

我想为Data.Map创建一个特殊的智能构造函数,对键/值对关系的类型有一定的约束.这是我试图表达的约束:

{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, DataKinds #-}

data Field = Speed | Name | ID
data Value = VFloat Float | VString ByteString | VInt Int

class Pair f b | f -> b where
    toPair :: f -> b -> (f, b)
    toPair = (,)

instance Pair Speed (VFloat f) 
instance Pair ID (VInt i)

对于每个字段,只应该与其关联的一种类型的值.就我而言,一个Speed字段映射到一个字段是没有意义的ByteString.一个Speed字段应该唯一映射到一个Float

但是我收到以下类型错误:

Kind mis-match
The first argument of `Pair' should have kind `*',
but `VInt' has kind …

所以,我终于找到了一个可以使用新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 [] …

我一直在教自己关于类型级编程,并希望编写一个简单的自然数加法类型函数.我的第一个版本如下:

data Z
data S n

type One = S Z
type Two = S (S Z)

type family Plus m n :: *
type instance Plus Z n = n
type instance Plus (S m) n = S (Plus m n)

所以在GHCi我能做到:

ghci> :t undefined :: Plus One Two
undefined :: Plus One Two :: S * (S * (S * Z))

哪个按预期工作.然后我决定通过修改Z和S类型来尝试DataKinds扩展:

data Nat = Z | S Nat

Plus系列现在可以返回Nat一种:

type family …