Создание типа данных типа Haskell, принимающего тип не-вида в одном из его конструкторов

Question

Здравствуйте. Я играю с библиотекой Ivory, которая в значительной степени опирается на современные возможности Haskell. Среди прочего, он определяет модели IvoryType, принимающий все типы, и IvoryArea, принимающие типы специального вида Area. Определения выглядят так:

{-# 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 

могли бы вы объяснить, как чтобы выразить собственность ivoryArea функции в Haskell правильно?

Редактировать Некоторые ссылки на оригинальные декларациях:

• 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

Answer 1

Теперь, когда мы установили в комментариях, что вы не можете делать то, что вы хотите напрямую, который создает специальный «подкидык» всех типов, мы можем использовать немного больше, чтобы получить то, что вы хотите.

Мы просто используем (закрытое) семейство типов, чтобы интерпретировать ваш вид 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)))