Search code examples
haskelldependent-type

`foreach` in Haskell

This code type-checks:

type T :: Type -> foreach (r :: Type) -> Type -> Type
data T k r a

type T' :: Type -> Type
type T' a = T a Identity a
  • Why is it that the compiler requires a type of kind Type -> Type (ie., Identity) here? It fails to type-check if you replace Identity with say Int.
  • What is foreach keyword, and how does one use it in Haskell?
Solution

  • It's not a keyword, just an implicitly quantified type variable. It's like when you write a function

    foo :: Int -> foreach r -> Double
foo = undefined

main = print ( foo 123 (Just 'w')
             , foo 789 [False, True, False] )

    ...so foreach r can be unified with Maybe Char or [Bool] but not, for instance, Float.

    Now, in your example it's even more weird, because you have not applied Identity to anything. That means the foreach type in T a Identity a seems to be actually the partially applied -> operator from Identitys Type -> Type signature lifted up one level... funky stuff.