标签云

微信群

扫码加入我们

WeChat QR Code

Hello. I am playing with Ivory library which relies heavily on modern features of Haskell. Among others, it defines the typeclasses IvoryType accepting all types and IvoryArea accepting types of special kind Area. The definitions look like this:{-# 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 typeclass IvoryType t whereivoryType :: 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 *) whereivoryArea :: Proxy a -> I.Type {- arguments are not important -}OK. Now let's try to express the fact that we are going to store values with ivoryType function defined. Obviously, they are the memebers of IvoryType class, so the answer isdata TypeStorage = TypeStorage (forall t . IvoryType t => t)So far so good. Now we want to store values which have ivoryArea function defined. Let's use the IvoryArea class as a filter condition, like in the prevoius case: data AreaStorage = AreaStorage (forall t . IvoryArea t => t)Surprisingly, the compiler (ghc version 7.8.4) outputs an errorsrc/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 ‘AreaCould you please explain, how to express the ownership of ivoryArea function in Haskell properly ?EditSome links to the original declarations:https://github.com/GaloisInc/ivory/blob/master/ivory/src/Ivory/Language/Type.hshttps://github.com/GaloisInc/ivory/blob/master/ivory/src/Ivory/Language/Area.hs


I've also tried rewriting AreaStorage as GADT with the same result

1970年01月01日00分03秒

I can't reproduce your result: f :: forall t . (IvoryArea t) => t get rejected by GHC for the same reason on my machine. Would you consider posting the implementation of it?

2019年04月20日40分27秒

Most likely your f actually has a type like forall t. (IvoryArea t) => Proxy t -> ....

2019年04月20日40分27秒

So... you write that you "want to store instances of IvoryArea". consider what an instance would be. In particular IvoryArea :: Area * -> GHC.Prim.Constraint. But what is a value level inhabitant of Area * ? Types that are of kinds created by DataKinds don't have inhabitants...

2019年04月19日40分27秒

"I mean I want to store datatypes which are instances of IvoryArea" - You can only "store" values. There seems to be some critical misunderstanding about what a "value" is. There are no values of type 'Stored Int, for example. Not even undefined, whose type is forall (a :: *) . a. Strictly speaking, values are not inhabitants of kind * - types of kind * are inhabitants of kind *. Values are inhabitants of types of kind *. You probably want to define a type indexed on Area (whose kind will be Area * -> *, perhaps, or maybe even Area k -> *).

2019年04月20日40分27秒