Probleme mit DataKinds
Ich habe ein sehr einfaches Beispiel für ein Problem bei der Verwendung von GADTs und DataKinds erstellt. Meine eigentliche Anwendung ist offensichtlich komplizierter, aber dies fängt das Wesentliche meiner Situation klar ein. Ich versuche, eine Funktion zu erstellen, die einen der Werte (T1, T2) vom Typ Test zurückgeben kann. Gibt es eine Möglichkeit, dies zu erreichen, oder komme ich in das Reich der abhängigen Typen? Die Fragen hier scheinen ähnlich zu sein, aber ich konnte keine Antwort auf meine Frage von ihnen finden (oder verstehen). Ich fange gerade an, diese GHC-Erweiterungen zu verstehen. Vielen Dank.
{-# 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
---- Hier ist der Fehler ---- 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