在其構造函數之一中創建接受非*類型的Haskell數據類型

Hello。我正在與依賴於Haskell現代特徵的象牙圖書館玩耍。其中，它定義了接受所有類型的類型IvoryType和接受特殊類型Area的IvoryArea。定義如下：在其構造函數之一中創建接受非*類型的Haskell數據類型

{-# 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函數的所有權？

編輯一些鏈接到原始聲明：

來源

2016-03-02 grwlf

我也試着重寫AreaStorage作爲GADT具有相同的結果 – grwlf

我不能重現你的結果：'˚F:: FORALL噸。（IvoryArea t）=> t '由於同樣的原因，在我的機器上被GHC拒絕。你會考慮發佈它的實現嗎？ – zakyggaps

很可能你的'f'實際上有一個類似'forall t'的類型。（IvoryArea t）=>代理t - > ...。 –

現在，我們已經建立的評論，你想要什麼，你不能做直接，這是創建一個所有類型的特殊「subkind」，我們可以使用更多的legwork工作，以得到你想要的。

我們只是使用（封閉）類型的家庭來解釋您的Area *種類*然後GADT，索引Area *，以保存這些值。如果需要的話，我們可以將整個文件包裝在存儲中以存儲這種類型的任意值。

考慮這個砍下例如：

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)))

來源

2016-03-03 19:02:37 sclv

在其構造函數之一中創建接受非*類型的Haskell數據類型

回答

相關問題