4

我有以下源代码：

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

class Digit d  

data Zero
data One
data Two
data Three
data Four
data Five
data Six

instance Digit Zero
instance Digit One
instance Digit Two
instance Digit Three
instance Digit Four
instance Digit Five
instance Digit Six


class Sum a b c | a b -> c, a c -> b, c b -> a 

incSize :: (Digit z, Digit x, Sum x One z) => x -> z --written by me
incSize _ = undefined

intToSize :: (Digit x, Num a, Sum x One x) => a -> x -> t --inferred by GHCI
intToSize n v = intToSize (n-1) (incSize v)

intToSize' :: (Digit b, Sum b One b) => Int -> t -> b -> b --inferred by GHCI
intToSize' n v = foldr (.) id (replicate n incSize)

intToSize'' :: (Digit a, Digit b1, Digit b, Digit c, Sum a One b1, Sum b1 One b, Sum b One c) => a -> c --inferred by GHCI
intToSize'' = incSize . incSize . incSize

本质上，目标是获取Int并将其转换为上面定义的数据类型之一。该功能incSize正常工作；它将大小增加一。该功能inToSize''也有效；它将给定数字增加3。但是，两者都intToSize不起作用intToSize'；GHCI 如上所述推断它们的类型（显然，a+1 =/= a）。我不确定为什么手动编写组合可以正常工作，而其他任何事情都会失败（我确定为无法编译的函数，但无论何时使用它们都会出错。）使用应该如下所示：

> :t intToSize'' (undefined :: Zero)
> intToSize'' (undefined :: Zero) :: Three

然而，最终目标是编写一个函数，该函数接受一个列表，并给出一个数据类型，该数据类型将列表的长度编码为其类型（本质上是一个向量）：

data Vect s v = Vect v
instance forall s v . Show (Vect s v) where
     --toInt is a function which takes a type number and returns its data level value
     show (Vect v) = "Vect " ++ (show . toInt) (undefined :: s) ++ show v  

> let l = [1,2,3,4,5]
> vector l 
> Vect 5 [1,2,3,4,5]

您可能已经注意到缺少一些代码；看起来很无聊，所以我把它放在底部。

instance Sum  Zero  Zero  Zero
instance Sum  Zero  One   One
instance Sum  Zero  Two   Two
instance Sum  Zero  Three Three
instance Sum  Zero  Four  Four
instance Sum  Zero  Five  Five
instance Sum  Zero  Six   Six
instance Sum  One   Zero  One
instance Sum  One   One   Two
instance Sum  One   Two   Three
instance Sum  One   Three Four
instance Sum  One   Four  Five
instance Sum  One   Five  Six
instance Sum  Two   Zero  Two
instance Sum  Two   One   Three
instance Sum  Two   Two   Four
instance Sum  Two   Three Five
instance Sum  Two   Four  Six
instance Sum  Three Zero  Three
instance Sum  Three One   Four
instance Sum  Three Two   Five
instance Sum  Three Three Six
instance Sum  Four  Zero  Four
instance Sum  Four  One   Five
instance Sum  Four  Two   Six
instance Sum  Five  Zero  Five
instance Sum  Five  One   Six
instance Sum  Six   Zero  Six
4

1 回答 1

10

问题是您想将多态类型的函数传递给foldr. 请注意，虽然foldr它本身具有多态类型，但它希望其参数具有单态类型。

对于将多态函数作为参数的函数（实际上以多态方式使用这些参数函数），您需要所谓的高阶多态性。好消息是 GHC 支持更高级别的多态类型（使用RankNTypes扩展）；坏消息是类型推断对他们来说是不可判定的。因此，您将需要在代码中明确类型签名，以使类型检查器相信您的代码是正确的。那么问题当然会出现，您的函数需要什么类型签名intToSize'？然后还有更多坏消息：由于您的函数类型需要取决于您提供的整数值，因此不能直接用 Haskell 表示。

也就是说，使用 GADT 和类型系列，您可以朝着您所追求的目标迈进一大步：

{-# LANGUAGE GADTs        #-}
{-# LANGUAGE TypeFamilies #-}

data Zero
data Succ n

type One   = Succ Zero
type Two   = Succ One
type Three = Succ Two

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

zero  = Zero
one   = Succ zero
two   = Succ one
three = Succ two

type family Sum m n          :: *
type instance Sum Zero n     =  n
type instance Sum (Succ m) n =  Succ (Sum m n)

add            :: Nat m -> Nat n -> Nat (Sum m n)
add Zero n     =  n
add (Succ m) n =  Succ (add m n)

incSize :: Nat m -> Nat (Sum One m)
incSize = add one  -- or just: Succ

例如：

> :t incSize two
incSize two :: Nat (Sum One (Succ (Succ Zero)))

并注意Sum One (Succ (Succ Zero)))与 相同Three。

至于你更大的目标，写“一个函数，它接受一个列表，并给出一个数据类型，它在其类型中编码列表的长度”：你根本不能这样做。您不能拥有一个静态（即编译时）类型的函数，这取决于一个可能直到运行时才知道的值（列表的长度）。

您可以获得的最接近的方法是将向量类型包装在存在包装器中：

{-# LANGUAGE DataKinds    #-}
{-# LANGUAGE GADTs        #-}
{-# LANGUAGE TypeFamilies #-}

data Nat = Zero | Succ Nat

data Vec :: Nat -> * -> * where
  Nil  :: Vec Zero a
  Cons :: a -> Vec n a -> Vec (Succ n) a

data EVec :: * -> * where
  Exists :: Vec n a -> EVec a

enil :: EVec a
enil =  Exists Nil

econs               :: a -> EVec a -> EVec a
econs x (Exists xs) =  Exists (Cons x xs)

vector :: [a] -> EVec a
vector =  foldr econs enil

现在，只要你有一个 type 的值EVec，你就可以打开它并对包含的向量进行各种处理，通过在其类型中对其长度进行编码来提高类型安全性。

于 2013-06-03T23:16:11.310 回答