受約束的封閉類型家族

Question

我可以說服編譯器，一個封閉類型家族中的類型同義詞總是滿足一個約束嗎？這個家庭被一系列有限的促銷價值索引。沿

data NoShow = NoShow 
data LiftedType = V1 | V2 | V3 

type family (Show (Synonym (a :: LiftedType)) => Synonym (a :: LiftedType)) where 
    Synonym V1 = Int 
    Synonym V2 = NoShow -- no Show instance => compilation error 
    Synonym V3 =() 

線

東西我可以在開放式的家庭強制約束：

class (Show (Synonym a)) => SynonymClass (a :: LiftedType) where 
    type Synonym a 
    type Synonym a =() 

instance SynonymClass Int where 
    type Synonym V1 = Int 

-- the compiler complains here 
instance SynonymClass V2 where 
    type Synonym V2 = NoShow 

instance SynonymClass V3 

但隨後的編譯器必須能夠推論是存在的事實V1,V2和V3中的每一個的實例爲SynonymClass a？但無論如何，我寧願不使用開放式家庭。

我的要求是，我想說服編譯器，我的代碼中的封閉類型系列的所有實例都有Show/Read實例。一個簡單的例子是：

parseLTandSynonym :: LiftedType -> String -> String 
parseLTandSynonym lt x = 
    case (toSing lt) of 
    SomeSing (slt :: SLiftedType lt') -> parseSynonym slt x 

parseSynonym :: forall lt. SLiftedType lt -> String -> String 
parseSynonym slt flv = 
     case (readEither flv :: Either String (Synonym lt)) of 
     Left err -> "Can't parse synonym: " ++ err 
     Right x -> "Synonym value: " ++ show x 

[在評論認爲這是不可能提到有人 - 這是因爲它在技術上是不可能的（如果是的話，爲什麼），或者只是一個GHC實現的限制嗎？]

Answer 1

問題是我們不能將Synonym放在實例頭部，因爲它是一個類型族，並且我們不能寫出像(forall x. Show (Synonym x)) => ...這樣的「通用量化」約束，因爲Haskell中沒有這樣的東西。

然而，我們可以用兩件事情：

• forall x. f x -> a相當於(exists x. f x) -> a
• singletons的去官能讓我們把類型家庭陷入實例頭反正。

所以，我們定義了一個生存的包裝上singletons風格類型功能的工作原理：

data Some :: (TyFun k * -> *) -> * where 
    Some :: Sing x -> f @@ x -> Some f 

而且我們還包括LiftedType的去官能化符號：

import Data.Singletons.TH 
import Text.Read 
import Control.Applicative 

$(singletons [d| data LiftedType = V1 | V2 | V3 deriving (Eq, Show) |]) 

type family Synonym t where 
    Synonym V1 = Int 
    Synonym V2 =() 
    Synonym V3 = Char 

data SynonymS :: TyFun LiftedType * -> * -- the symbol for Synonym 
type instance Apply SynonymS t = Synonym t 

現在，我們可以使用Some SynonymS -> a而不是forall x. Synonym x -> a，這種形式也可以在實例中使用。

instance Show (Some SynonymS) where 
    show (Some SV1 x) = show x 
    show (Some SV2 x) = show x 
    show (Some SV3 x) = show x 

instance Read (Some SynonymS) where 
    readPrec = undefined -- I don't bother with this now... 

parseLTandSynonym :: LiftedType -> String -> String 
parseLTandSynonym lt x = 
    case (toSing lt) of 
    SomeSing (slt :: SLiftedType lt') -> parseSynonym slt x 

parseSynonym :: forall lt. SLiftedType lt -> String -> String 
parseSynonym slt flv = 
     case (readEither flv :: Either String (Some SynonymS)) of 
     Left err -> "Can't parse synonym: " ++ err 
     Right x -> "Synonym value: " ++ show x 

這並不直接爲我們提供Read (Synonym t)爲t任何具體的選擇，但我們仍然可以讀上存在標籤Some SynonymS然後模式匹配檢查，如果我們有正確的類型（如果它不是失敗對）。這幾乎涵蓋了所有的用例read。

如果這還不夠好，我們可以使用另一個包裝器，並將Some f實例提升爲「通用量化」實例。

data At :: (TyFun k * -> *) -> k -> * where 
    At :: Sing x -> f @@ x -> At f x 

At f x相當於f @@ x，但我們可以編寫實例吧。特別是，我們可以在這裏寫一個明智的通用Read實例。

instance (Read (Some f), SDecide (KindOf x), SingKind (KindOf x), SingI x) => 
    Read (At f x) where 
    readPrec = do 
     Some tag x <- readPrec :: ReadPrec (Some f) 
     case tag %~ (sing :: Sing x) of 
     Proved Refl -> pure (At tag x) 
     Disproved _ -> empty 

我們首先解析Some f，然後檢查解析式指數是否等於我們想解析指標。這是我上面提到的用於解析具有特定索引的類型的抽象。這樣更方便，因爲我們在At的模式匹配中只有一個案例，無論我們有多少指數。通知雖然SDecide約束。它提供了%~方法，如果我們在單例數據定義中包含deriving Eq，singletons派生它。把這個使用方法：

parseSynonym :: forall lt. SLiftedType lt -> String -> String 
parseSynonym slt flv = withSingI slt $ 
     case (readEither flv :: Either String (At SynonymS lt)) of 
     Left err -> "Can't parse synonym: " ++ err 
     Right (At tag x) -> "Synonym value: " ++ show (Some tag x :: Some SynonymS) 

我們也可以At和Some更容易一點之間的轉換：

curry' :: (forall x. At f x -> a) -> Some f -> a 
curry' f (Some tag x) = f (At tag x) 

uncurry' :: (Some f -> a) -> At f x -> a 
uncurry' f (At tag x) = f (Some tag x) 

parseSynonym :: forall lt. SLiftedType lt -> String -> String 
parseSynonym slt flv = withSingI slt $ 
     case (readEither flv :: Either String (At SynonymS lt)) of 
     Left err -> "Can't parse synonym: " ++ err 
     Right atx -> "Synonym value: " ++ uncurry' show atx 

Answer 2

如果我理解正確，你想做的事，這是不可能的。如果是這樣，你可以很容易地構建Proxy t -> Bool類型的非恆定功能，沿

data YesNo = Yes | No 
class Foo (yn :: YesNo) where foo :: Proxy yn -> Bool 
type family (Foo (T t) => T t) where 
    T X = Yes 
    T y = No 

f :: forall t. Proxy t -> Bool 
f _ = foo (Proxy (T t)) 

的線條，但你不能建立這樣的功能，即使所有涉及到的各種被關閉（這是當然的任根據您的觀點，GHC的功能或限制）。