如何用GADT進行存在量化？

我有以下數據類型：如何用GADT進行存在量化？

{-# LANGUAGE ExistentialQuantification #-} 

data ExType = forall a. One a | forall a. Two a | forall a. Three a

隨着我能夠創造異構列表：

[One 3, Two "hello", One 'G']

我已被告知，GADTs是做到這一點的新途徑。 GADT可以隱含地做我上面想要做的事情。到目前爲止，我還沒有能夠創建一個GADT類型，它允許我創建一個異構列表。我該怎麼做呢？

感謝

來源

2017-04-18 kurzweil4

通常與多態構造將有一個類型參數，這樣你就可以知道建造它的時候，如使用什麼類型GADT：

{-# LANGUAGE GADTs #-} 
data Value a where 
    Str :: String -> ExType String 
    Number :: Int -> ExType Int 
    Other :: a -> ExType a

然而，事情的關鍵存在類型確實會埋葬這種類型，所以你不知道它是用什麼構造的，僅僅是它存在的某種類型a。因此，只需從類型構造函數中以及數據構造函數的結果類型中刪除type參數即可。

{-# LANGUAGE GADTs #-} 
data ExType where 
    One :: a -> ExType 
    Two :: a -> ExType 
    Three :: a -> ExType 

foo :: [ExType] 
foo = [One 3, Two "hello", One 'G']

來源

2017-04-18 21:51:41 amalloy

注意，所有GADTs在這種情況下，你做的是使語法中含有'forall'。這裏的GADT與ADT在技術上沒有區別，它只是語法不同。 – Lazersmoke

我不知道GADT是否是新的黑色，但 - 這裏是你的例子使用這種語法。

{-# LANGUAGE ExplicitForAll  #-} 
{-# LANGUAGE GADTs    #-} 

data ExType where 
    One :: forall a. a -> ExType 
    Two :: forall a. a -> ExType 
    Three :: forall a. a -> ExType 

lst :: [ExType] 
lst = [One 3, Two "hello", Three 'A']

注意，對於GADTs獲得實例最好用{-# LANGUAGE StandaloneDeriving #-}做的，即使是像Eq基本的東西，會不會因爲約束的工作forall a.

來源

2017-04-18 21:52:19 epsilonhalbe

如何用GADT進行存在量化？

回答

相關問題