存在性量化類型的類

什麼類型級等同於下面的存在性量化的字典，由Pipe類型的啓發：存在性量化類型的類

{-# LANGUAGE ExistentialQuantification, PolymorphicComponents #-} 

data PipeD p = forall cat . PipeD { 
    isoI  :: forall a b m r . Iso (->) (p a b m r) (cat m r a b), 
    categoryI :: forall  m r . (Monad m) => CategoryI (cat m r) , 
    monadI  :: forall a b m . (Monad m) => MonadI (p a b m)  , 
    monadTransI :: forall a b  . MonadTransI (p a b)    }

的粗略的想法，我去爲想說，鑑於(PipeLike p)約束，我們可以推斷出(MonadTrans (p a b), Monad (p a b m)和（使用僞代碼）(Category "\a b -> p a b m r")。

的CategoryI和MonadI只是我用來表達思想，Category，Monad和MonadTrans是（在某種程度上）這種PipeLike類型的超類的類型類的字典中的等價物。

的Iso類型只是以下詞典存儲的同構：

data Iso (~>) a b = Iso { 
    fw :: a ~> b , 
    bw :: b ~> a }

來源

2012-08-10 Gabriel Gonzalez

如果這確實是一個類型的類，則詞典值由類型p來決定。特別是，cat類型完全由p確定。這可以使用關聯數據類型來表示。在類定義中，相關的數據類型就像沒有右邊的數據定義一樣寫入。

一旦您將cat表示爲類型，其他成員可以很容易地更改爲鍵入類，如我已經爲Monad和MonadTrans所示。請注意，我更喜歡對複雜類型使用顯式類簽名。

{-# LANGUAGE TypeFamilies, FlexibleInstances, UndecidableInstances #-} 

class Pipe (p :: * -> * -> (* -> *) -> * -> *) where 
    data Cat p :: (* -> *) -> * -> * -> * -> * 
    isoI  :: forall a b m r. Iso (->) (p a b m r) (Category p m r a b) 
    categoryI :: forall a b m. Monad m => CategoryI (Category p m r) 

instance (Pipe p, Monad m) => Monad (p a b m) 

instance Pipe p => MonadTrans (p a b)

來源

2012-08-10 21:35:51 Heatsink

我認爲相關的數據類型可能是正確的方向，儘管我根本不需要任何字典。我希望得到類似於：class（Monad（p a b m），MonadTrans（p a b），Category（Cat p））=> PipeLike p { - empty class - }'。同構的東西只是粘在存在的量化類型上，如果我使用關聯的數據類型，這是不必要的。 – 2012-08-10 22:07:55

您無法制作'Monad'和'MonadTrans'超類，因爲給定'p'，無法選擇'a'，'b'和'm'。但是，您可以像我所示的那樣製作實例。他們將像原來的界面一樣工作。 – Heatsink 2012-08-11 13:53:46

這很有道理。感謝您清除我的想法。我會接受這個。 – 2012-08-11 16:08:25

存在性量化類型的類

回答

相關問題