创建Haskell数据类型,在其构造函数之一中接受非* kind类型

2023年3月22日 268次阅读

你好.我正在玩Ivory库,它很大程度上依赖于
Haskell的现代功能.其中,它定义了类型IvoryType接受所有类型和IvoryArea接受特殊类型区域的类型.定义如下所示：

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE ExistentialQuantification #-}

-- | Proxy datatype with a phantom arbitrary-kinded type
-- and a single constructor 
data Proxy (a :: k) = Proxy

-- | The kind of memory-area types.
data Area k
  = Struct Symbol
  | Array Nat (Area k)
  | CArray (Area k)
  | Stored k
    -- ^ This is lifting for a *-kinded type

class IvoryType t where
  ivoryType :: Proxy t -> I.Type {- arguments are not important -}

-- | Guard the inhabitants of the Area type, as not all *s are Ivory *s.
class IvoryArea (a :: Area *) where
  ivoryArea :: Proxy a -> I.Type {- arguments are not important -}

好.现在让我们尝试表达我们将使用定义的ivoryType函数存储值的事实.显然,他们是IvoryType类的成员,所以答案是

data TypeStorage = TypeStorage (forall t . IvoryType t => t)

到现在为止还挺好.现在我们要存储定义了ivoryArea函数的值.让我们使用IvoryArea类作为过滤条件,就像在prevoius案例中一样：

data AreaStorage = AreaStorage (forall t . IvoryArea t => t)

令人惊讶的是,编译器(ghc版本7.8.4)输出错误

src/IvoryLL/Types.hs:59:45:
    Expected a type, but ‘t’ has kind ‘Area *’
    In the type ‘forall t. IvoryArea t => t’
    In the definition of data constructor ‘AreaBase’
    In the data declaration for ‘Area

能否解释一下,如何正确表达Haskell中ivoryArea函数的所有权？

编辑
原始声明的一些链接：

> https://github.com/GaloisInc/ivory/blob/master/ivory/src/Ivory/Language/Type.hs
> https://github.com/GaloisInc/ivory/blob/master/ivory/src/Ivory/Language/Area.hs

最佳答案 既然我们已经在评论中确定你不能直接做你想做的事情,这就是创造了一个特殊的“subkind”,我们可以使用更多的腿部来获得你想要的东西.

我们只使用(闭合)类型族将您的Area *类型解释为某种类型*然后将GADT(由Area *索引)来保存这些值.然后我们可以将整个shebang包裹在一个存在主义中,以存储这种类型的任意值,如果需要的话.

考虑这个减少的例子：

data Area k
  = Stored k
  | List (Area k)

type family InterpIvoryArea a :: * where
    InterpIvoryArea (Stored k) = k
    InterpIvoryArea (List a) = [InterpIvoryArea a]

data AreaStorage a where
    AreaStorage :: InterpIvoryArea a -> AreaStorage a

data AreaStorageExistential where
    AreaStorageExistential :: AreaStorage a -> AreaStorageExistential

testValue :: AreaStorageExistential
testValue = AreaStorageExistential (AreaStorage [1,2,3] :: AreaStorage (List (Stored Int)))
点赞