Trouble with DataKinds

Question

I have created a very simple example of a problem I'm having using GADTs and DataKinds. My real application is obviously more complicated but this captures the essence of my situation clearly. I'm trying to create a function that can return any of the values (T1, T2) of type Test. Is there a way to accomplish this or am I getting into the realm of dependent types? The questions here seem similar but I could not find (or comprehend) an answer to my question from them. I'm just starting to understand these GHC extensions. Thanks.

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

----Here is the error---- 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

Sonnie

What should the semantics of prob be? What should it do? – Religieux

I added the GHCI error message. This is a totally contrived example. I want to be able to have prob return any of the values of Test (Test TI or Test TD) based on some calculation. – Sonnie

I tried to guess what you're after, but it's better to describe what exactly you want to achieve. Contrived examples are ok as soon as your intention is clear. – Religieux

Answer 1

The error message you get is because the type parameter to Test needs to have the kind TIdx, but the only types that have that kind are TI and TD. The type TIdx has the kind *.

If I understood correctly what you are trying to express is that the result type of prob is either Test TI or Test TD, but the actual type is determined at runtime. However, this won't work directly. The return type generally has to be known at compile time.

What you can do, since the GADT constructors each map to specific phatom type of kind TIdx, is to return a result that erases the phantom type with an existential or another GADT and then recover the type later using a pattern match.

For example, if we define two functions that require a specific kind of Test:

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

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

This type-checks:

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

The notable thing here is that in the case-expression, even though the UnknownTest GADT has erased the phantom type, the T1 and T2 constructors give enough type information to the compiler that t recovers its exact type Test TI or Test TD within the branch of the case-expression, allowing us to e.g. call functions that expect those specific types.

Son

Nice! I didn't realize that you can automatically restore the type index from the data constructor in this case. – Religieux

That's nice you can pattern match on the existential afterwards. But, I guess there is no way to rebuild the indexed type from then on. I suppose I can't have the best of both worlds. – Sonnie

This seems like a silly question but, is there some way to get a T1 or T2 back out of this? Can I use Singeton Types or PolyKinds to somehow return a "Test TIdx". I'm not sure of that makes any sense. – Sonnie

If you think about it, the type you call "Test TIdx" doesn't contain any more type information than UnknownTest, since the phantom type-parameter is ambiguous. In order to get a complete type back from a calculation, the information which determines the result type needs to be available at the type-level (i.e. limited or full dependent types). – Son

Answer 2

You have two options here. Either you can infer the type of the return value from the types of arguments or you can't.

In the former case, you refine the type:

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

In the latter case, you have to erase the type information:

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

You can also erase the type information by using an existential type:

data SomeTest = forall i . SomeTest (Test i)

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

In this case, you cannot do anything interesting with a value of SomeTest, but you might be able in your real example.

Religieux

In my real situation I have an "indexed" GADT that represents different shapes. The function calculates the geometric intersection between these shapes (surfaces). The result will be another shape from a similar indexed GADT, the exact type of which will not be known until the calculation is complete. An example type signature of this function might be Surface -> Surface -> Curve. Where Surface and Curve might each contain many constructors. I can post my real code if this is still not clear. Thanks. – Sonnie

What I said is still valid — if you can move the part of the computation necessary to determine the shape to the type level, then you can write the resulting type. Otherwise, you'll have to erase it. – Religieux