Проблема с DataKinds

Question

Я создал очень простой пример проблемы, с которой я пользуюсь GADT и DataKinds. Мое реальное применение явно сложнее, но это ясно отражает суть моей ситуации. Я пытаюсь создать функцию, которая может возвращать любые значения (T1, T2) типа Test. Есть ли способ достичь этого или я попадаю в область зависимых типов? Вопросы здесь кажутся похожими, но я не мог найти (или постигнуть) ответ на мой вопрос от них. Я только начинаю понимать эти расширения GHC. Благодарю.

similar question 1

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 

Answer 1

сообщение об ошибке вы получаете, потому что параметр типа для 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 t@(T1 _) -> fun1 t 
     UnknownTest t@(T2 _) -> fun2 t 

Примечательным здесь является то, что в case -expression , хотя UnknownTest GADT стирает фантомный тип, конструкторы T1 и T2 дают достаточно информации о размере n компилятору, что t восстанавливает свой точный тип Test TI или Test TD в пределах ветки выражения case, что позволяет нам, например, вызовите функции, которые ожидают этих конкретных типов.

Answer 2

У вас есть два варианта здесь , Либо вы можете вывести тип возвращаемого значения из типов аргументов, либо вы не можете.

В первом случае вы уточнить тип:

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 ue от SomeTest, но вы можете быть в своем реальном примере.