DataKinds故障

我創建了一個非常簡單的問題示例，我使用的是GADT和DataKinds。我的真實應用顯然更復雜，但這清楚地表明瞭我的情況的本質。我試圖創建一個函數，可以返回任何類型的值（T1，T2）的測試。有沒有辦法做到這一點，還是我進入依賴類型的領域？這裏的問題看起來很相似，但我無法從他們那裏找到（或理解）我的問題的答案。我剛剛開始瞭解這些GHC擴展。謝謝。DataKinds故障

similar question 2

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

module Test where 

data TIdx = TI | TD 

data Test :: TIdx -> * where 
    T1 :: Int -> Test TI 
    T2 :: Double -> Test TD 

type T1 = Test TI 
type T2 = Test TD 

prob :: T1 -> T2 -> Test TIdx 
prob x y = undefined

----以下是錯誤---- Test.hs：14：26：

Kind mis-match 

The first argument of `Test' should have kind `TIdx', 

but `TIdx' has kind `*' 

In the type signature for `prob': prob :: T1 -> T2 -> Test TIdx

來源

2013-02-17 MFlamer

'prob'的語義應該是什麼？它應該做什麼？ – 2013-02-17 07:27:19

我添加了GHCI錯誤消息。這是一個完全人爲的例子。我希望能夠根據某些計算返回Test（測試TI或測試TD）的任何值。 – MFlamer 2013-02-17 07:37:31

我試圖猜測你想要做什麼，但最好能描述一下你想達到的目標。一旦你的意圖清楚，立刻舉例就好了。 – 2013-02-17 07:49:55

你得到的錯誤信息是因爲類型參數Test需要有那種TIdx，但有那種唯一的類型是TI和TD。類型TIdx有種*。

如果我明白你想表達什麼正確的是結果類型的prob或者是Test TI或Test TD，但實際類型是在運行時確定。但是，這不會直接工作。在編譯時通常必須知道返回類型。

你能做什麼，因爲GADT構造均可映射到特定phatom類型的一種TIdx，是返回擦除與存在或其他GADT，然後將假體類型恢復的數據類型後使用的模式結果比賽。

例如，如果我們定義需要特定種類的Test兩個功能：

fun1 :: T1 -> IO() 
fun1 (T1 i) = putStrLn $ "T1 " ++ show i 

fun2 :: T2 -> IO() 
fun2 (T2 d) = putStrLn $ "T2 " ++ show d

這種類型的檢查：

data UnknownTest where 
    UnknownTest :: Test t -> UnknownTest 

prob :: T1 -> T2 -> UnknownTest 
prob x y = undefined 

main :: IO() 
main = do 
    let a = T1 5 
     b = T2 10.0 
     p = prob a b 

    case p of 
     UnknownTest [email protected](T1 _) -> fun1 t 
     UnknownTest [email protected](T2 _) -> fun2 t

這裏值得注意的是，在case -expression儘管GADT已經擦除了幻像類型，但T1和T2構造函數提供了足夠的類型信息 n給編譯器，t在case-expression的分支內恢復其確切類型Test TI或 Test TD，允許我們例如請致電預期這些特定類型的函數。

來源

2013-02-17 08:20:14 shang

不錯！在這種情況下，我沒有意識到可以自動從數據構造函數中恢復類型索引。 – 2013-02-17 08:34:41

這很好，你可以在存在後模式匹配。但是，我想從那時起沒有辦法重建索引類型。我想我不能擁有兩全其美的世界。 – MFlamer 2013-02-17 09:12:12

這似乎是一個愚蠢的問題，但是，有沒有辦法讓T1或T2退出？我可以使用Singeton Types或PolyKinds以某種方式返回「Test TIdx」。我不確定這是否有道理。 – MFlamer 2013-02-19 02:00:04

你有兩個選擇這裏。要麼你可以從參數類型推斷返回值的類型，或者你不能。

在前一種情況下，你細化類型：

data Which :: TIdx -> * where 
    Fst :: Which TI 
    Snd :: Which TD 

prob :: Which i -> T1 -> T2 -> Test i 
prob Fst x y = x 
prob Snd x y = y

在後一種情況下，你必須刪除類型的信息：

prob :: Bool -> T1 -> T2 -> Either Int Double 
prob True (T1 x) y = Left x 
prob False x (T2 y) = Right y

您還可以通過使用擦除類型信息一個存在類型：

data SomeTest = forall i . SomeTest (Test i) 

prob :: Bool -> T1 -> T2 -> SomeTest 
prob True x y = SomeTest x 
prob False x y = SomeTest y

在這種情況下，你不能做任何有趣的事情與val你的SomeTest，但你可以在你的真實例子。

來源

2013-02-17 07:48:49

在我的真實情況下，我有一個代表不同形狀的「索引」GADT。該函數計算這些形狀（曲面）之間的幾何相交。結果將是來自類似的索引GADT的另一個形狀，直到計算完成才能知道確切的類型。此功能的示例類型簽名可能是曲面 - >曲面 - >曲線。 Surface和Curve可能每個都包含許多構造函數。如果這仍然不清楚，我可以發佈我的真實代碼。謝謝。 – MFlamer 2013-02-17 08:00:07

我所說的仍然有效 - 如果您可以將確定形狀所需的部分計算移動到類型級別，則可以編寫結果類型。否則，你將不得不抹去它。 – 2013-02-17 08:04:57

DataKinds故障

回答

相關問題