Type Juggling with Existentials at Runtime

Question

I'm playing around with existentials and GADTs in Haskell, and I'm trying to define a DSL for combinators (such as SKI). I have the GADT working, as well as a reduction function which works fine (and isn't really relevant to the question)

{-# LANGUAGE GADTs, ExistentialQuantification #-}

import Control.Applicative
import Data.Monoid
import Control.Monad

data Comb t where
    S :: Comb ((a -> b -> c) -> (a -> b) -> a -> c)
    K :: Comb (a -> b -> a)
    I :: Comb (a -> a)
    B :: Comb ((b -> c) -> (a -> b) -> a -> c)
    C :: Comb ((b -> a -> c) -> a -> b -> c)
    W :: Comb ((a -> a -> b) -> a -> b)
    (:$) :: Comb (a -> b) -> Comb a -> Comb b

What I'm trying to do now is define a way to read combinator strings in from the user at runtime. Obviously, I need an existential type to do this, since the GADT's type information needs to be hidden.

data CombBox = forall a. CombBox { unCombBox :: Comb a }

($$) :: CombBox -> CombBox -> Maybe CombBox
x $$ y = undefined -- ???

I would like the ($$) function to somehow "look inside" the CombBox existentials at runtime and, if it is possible to combine the two combinators using :$ and get a well-typed result, I would like the result to be that. Otherwise, I want Nothing. So, for example,

CombBox S $$ CombBox K ==> Just (CombBox (S :$ K))
CombBox W $$ CombBox I ==> Nothing

The latter should fail because W expects a 2-ary function where I takes one argument. But I would like to relegate this check to the runtime, and I'm not sure if such a thing is possible in the Haskell (+ GHC extensions) type system.

Answer 1

Get ready to learn about dependent pairs and singletons!

---

I'm going to rewrite your system a little bit to simplify it.

First off, I'm going to shrink your universe of types from all of Haskell to a much simpler universe consisting of a single primitive type and arrows.

infixr 0 :->
data Type = Unit | Type :-> Type

Hopefully you should be able to see how to extend this with more primitive types.

I'm also going to remove most of the bits from Comb, since they can all be expressed in terms of one another.

data Comb a where
    S :: Comb ((a :-> b :-> c) :-> (a :-> b) :-> a :-> c)
    K :: Comb (a :-> b :-> a)
    (:$) :: Comb (a :-> b) -> Comb a -> Comb b

i = S :$ K :$ i
b = (S :$ (K :$ S)) :$ K
c = S :$ (S :$ (K :$ (S :$ (K :$ S) :$ K)) :$ S) :$ (K :$ K)
w = S :$ S :$ (S :$ K)

---

Now to your question. As you correctly surmised, when you're reading user input you can't predict statically what the type of the resulting term will be, so you need to existentially quantify it.

data Ex f = forall a. Ex (f a)

The problem is: how do you recover the type information in order to be able to manipulate terms? We can pair up a Comb with another value which you can pattern-match on at runtime to learn the type of the Comb. Here's a combinator for pairing things up.

data (f :*: g) i = f i :*: g i

(I lifted both of these types from the Hasochism paper.) :*: pairs up two types ensuring that their indices are equal. We'll use it together with Ex to simulate a dependent pair or sigma type: a pair of values for whom the type of the second component depends on the value of the first. The idea is that f will be a GADT which tells you something about its index, so pattern matching on f gives you information about the type of g.

type Sg f g = Ex (f :*: g)
pattern Sg x y = Ex (x :*: y)

Now the clever part: coming up with a GADT which tells you about a combinator term's type.

data Typey t where
    Unity :: Typey Unit
    Arry :: Typey a -> Typey b -> Typey (a :-> b)

Typey is called a singleton. For a given t, there exists exactly one value of type Typey t. So if you have a Typey t value, you know everything there is to know about t.

Singleton values are ultimately a hack. Typey is not Type; it's a value-level stand-in for Type's duplicated type-level copy. In a real dependently-typed system you don't need singleton glue to affix value-level stuff to type-level stuff because the distinction isn't there in the first place.

Our existentially-quantified combinators now look like this. AComb packs up a Comb with a runtime representation of its type. This technique allows us to guarantee that the boxed Comb is well-typed; we just can't say statically what that type is.

type AComb = Sg Typey Comb

---

How do we write ($$), which attempts to apply an AComb to another AComb? We need to pattern-match on their associated Typeys in order to learn whether or not it's possible to apply one to the other. In particular, we're going to need a way to know whether two types are equal.

Here comes propositional equality, a GADT proof that two type-level things are equal. You can only give a value of Refl if you can explain to GHC that a and b are in fact the same. Conversely, if you pattern-match on Refl then GHC will add a ~ b to the typing context.

data a :~: b where
    Refl :: a :~: a
withEq :: a :~: b -> (a ~ b => r) -> r
withEq Refl x = x

Here's a helper function to lift a pair of equalities through the :-> constructor.

arrEq :: (a :~: c) -> (b :~: d) -> (a :-> b) :~: (c :-> d)
arrEq Refl Refl = Refl

As promised, we can write down a function to check whether two Types are equal. We proceed by pattern-matching on their associated singleton Typeys, failing if we find the types to be incompatible. If the equality test succeeds, the spoils are a proof that the types are equal.

tyEq :: Typey t -> Typey u -> Maybe (t :~: u)
tyEq Unity Unity = Just Refl
tyEq (Arry a b) (Arry c d) = liftA2 arrEq (tyEq a c) (tyEq b d)
tyEq _ _ = Nothing

withTyEq :: Typey t -> Typey u -> (t ~ u => a) -> Maybe a
withTyEq t u x = fmap (\p -> withEq p x) (tyEq t u)

Finally, we can write $$. The typing rule goes like this:

f : a -> b    y : a
------------------- App
      f y : b

That is, if the left-hand term of $$ is a function type, and the type of the right-hand term matches the function's domain, we can type the application. So the implementation of this rule has to test (using withTyEq) whether the relevant types match in order to return the resulting term.

($$) :: AComb -> AComb -> Maybe AComb
Sg (Arry a b) x $$ Sg t y = withTyEq a t $ Sg b (x :$ y)
_ $$ _ = Nothing

---

Generating Typey terms corresponds to the act of type-checking. In other words, a function parse :: String -> AComb has to do both parsing and type-checking. In real compilers, these two phases are separated.

So I'd advise parsing the user input into an untyped syntax tree, which admits ill-formed terms, and then generating typing information separately.

data Expr = S | K | Expr :$ Expr
parse :: String -> Parser Expr
typeCheck :: Expr -> Maybe AComb

A fun exercise (in more-dependently-typed languages) is to modify typeCheck to return a more detailed explanation of why type-checking failed, like this bit of pseudo-Agda:

data Void : Set where
Not : Set -> Set
Not a = a -> Void

data TypeError : Expr -> Set where
    notArr : Not (IsFunction f) -> TypeError (f :$ x)
    mismatch : Not (domain f :~: type x) -> TypeError (f :$ x)
    inFunc : TypeError f -> TypeError (f :$ x)
    inArg : TypeError x -> TypeError (f :$ x)

typeCheck : (e : Expr) -> Either (TypeError e) AComb

You can also make typeCheck more precise by giving assurance that it doesn't change the term you give it (another exercise).

For further reading, see The View from the Left, which features a verified type-checker for the lambda calculus.

Answer 2

Not a proper answer, but might be helpful.

Parametricity doesn't allow control flow to depend on types, so you need some first-order representation of types. Haskell has Typeable:

deriving instance Typeable Comb

data CombBox = forall a. Typeable a => CombBox { unCombBox :: Comb a }

Using it we can define

castApply1 :: (Typeable a, Typeable b, Typeable ab) => Comb ab -> Comb a -> Maybe (Comb b)
castApply1 f x = (:$ x) <$> cast f

However

($$) :: CombBox -> CombBox -> Maybe CombBox
CombBox f $$ CombBox x = CombBox <$> castApply f x

throws

Could not deduce (Typeable a0) arising from a use of `CombBox' …
    from the context (Typeable a)
    or from (Typeable a1)
    The type variable `a0' is ambiguous

The problem is that b is specified in the return type of castApply1, but if we immediately apply CombBox to castApply f x, then b doesn't get specified and hence remains ambiguous.

We can specify b by providing Proxy b as an argument:

castApply2 :: (Typeable a, Typeable b, Typeable ab) => Proxy b -> Comb ab -> Comb a -> Maybe (Comb b)
castApply2 p = castApply1

Which allows to wrap the result in CombBox:

castApply3 :: (Typeable a, Typeable b, Typeable ab) => Proxy b -> Comb ab -> Comb a -> Maybe CombBox
castApply3 p f x = CombBox <$> castApply2 p f x

We can finally define something that doesn't mention that annoying b:

data SomeTypeable = forall a. Typeable a => SomeTypeable (Proxy a)

castApply4 :: (Typeable a, Typeable ab) => SomeTypeable -> Comb ab -> Comb a -> Maybe CombBox
castApply4 (SomeTypeable p) = castApply3 p

Now having

typeRepToSomeTypeable :: TypeRep -> SomeTypeable

We can define

castApply :: (Typeable a, Typeable ab) => TypeRep -> Comb ab -> Comb a -> Maybe CombBox
castApply t = castApply4 (typeRepToSomeTypeable t)

($$) :: CombBox -> CombBox -> Maybe CombBox
CombBox f $$ CombBox x = funResultTy (typeRep f) (typeRep x) >>= \t -> castApply t f x

funResultTy is a function in Data.Typeable that returns the codomain of a first argument if its domain matches the second argument.

But how to define typeRepToSomeTypeable? It doesn't seem it was implemented somewhere. At least I haven't found it neither in Data.Typeable nor in Singletons.