多態性結果類型GADT函數

在下面的代碼中，我可以替換什麼x = ...。請注意，我不想對類別a設置類別限制（當然，a也是類型Bool，因此只能採用兩種類型之一）。多態性結果類型GADT函數

{-# LANGUAGE GADTs #-} 
{-# LANGUAGE DataKinds #-} 
{-# LANGUAGE KindSignatures #-} 

data D (a :: Bool) where 
    D1 :: D True 
    D2 :: D False 

x :: D a 
x = ...

基本上，像這樣GADTs很容易做輸入多態性（只匹配合適的構造函數），但我想在輸出中使用多態。

來源

2017-01-22 Clinton

這是不可能的，沒有辦法返回'D a'中的多態值，除非它是底部。如果/當我們得到'pi'類型（非擦除類型），那麼可以寫'x :: pi a。 D a' – chi

此外，儘管令人不快，但「任何」都是有效的類型。 'DataKinds'仍然允許類型級未定義... – Alec

只要定義了'x :: D True'和'x :: D False'，我不介意未定義。 – Clinton

這需要依賴類型 - 它沒有辦法繞過它。在伊德里斯，Haskell的類依賴性類型的語言，你可以就好了這樣寫：

data D : Bool -> Type where 
    D1 : D True 
    D2 : D False 

-- The `{ .. }` mean the argument is inferred. 
x : {a : Bool} -> D a 
x {a = True} = D1 
x {a = False} = D2

在Haskell，你可以根據調度在運行時類型的唯一途徑是通過類型類，所以你需要一個約束。事實上，正如@András指出的那樣，SingI就是爲此而生的（它來自一個包裹singletons，它正好處理這類問題）。

在你的情況，這將是：

{-# LANGUAGE GADTs, TypeInType, ScopedTypeVariables #-} 

import Data.Singletons.Prelude 

data D (a :: Bool) where 
    D1 :: D True 
    D2 :: D False 

x :: forall a. SingI a => D a 
x = case sing :: Sing a of 
     STrue -> D1 
     SFalse -> D2

這可能是值得一提的是，儘管有一個SingI約束，它都已經用它定義了適當的實例。任何其他有效的D類型但不包含Bool參數（如D Any）在編譯時失敗（沒有找到SingI實例）。

ghci> let _ = x :: D True 
ghci> let _ = x :: D False 
ghci> let _ = x :: D Any 
<interactive> error: 
    • No instance for (SingI Any) arising from a use of ‘x’ 
    • In the expression: x :: D Any 
    In a pattern binding: _ = x :: D Any

來源

2017-01-22 10:58:02 Alec

這個答案將通過類型類技術的演示得到改進。 –

@BenjaminHodgson據此更新。 – Alec

多態性結果類型GADT函數

回答

相關問題