[Haskell-cafe] Are GADTs what I need?

[Ryan Ingram]

On Mon, Jul 13, 2009 at 9:18 AM, Kev Mahoney<maillist at kevinmahoney.co.uk> wrote:
> That said, I think I may defer this until I understand the ins and
> outs of Haskell's type system a little better. I think a parametrized
> type will be the only way to do it. The only reason I thought GADTs
> may be able to do this is because I read some literature that
> suggested GADTs could be used as a kind of typecase construct (I think
> it was 'Fun with Phantom Types'?) but I could have very easily
> misunderstood it.

The big problem is that you haven't parametrized your Value type at
all, so there's no information about the value inside.

Try this:

> data Value a where
>     VPrim :: Type a -> a -> Value a
>     VAbs :: Type a -> (Value a -> Value b) -> Value (a -> b)
>     VApp :: Value (a -> b) -> Value a -> Value b

> data Type a where
>    TInt :: Type Int
>    TBool :: Type Bool
>    TChar :: Type Char
>    TList :: Type a -> Type [a]
>    TFun :: Type a -> Type b -> Type (a -> b)

data SomeType = forall a. SomeType (Type a)
data SomeValue = forall a. SomeValue (Value a)

Now you can do:

> interpret :: Value a -> a
> interpret (VPrim _ x) = x
> interpret (VAbs t f) = \x -> f (VPrim t x)
> interpret (VApp f x) = interpret f $ interpret x

And:

> typeOf :: Value a -> Type a
> typeOf (VPrim t _) = t
> typeOf (VAbs t f) = typeOf (f $ VPrim t (representative t))
> typeOf (VApp f _) = case typeOf f of (TFun _ b) -> b
>
> representative :: Type a -> a
> representative TInt = 0
> representative TBool = False
> representative TChar = 'a'
> representative (TList _) = []
> representative (TFun _ b) = \_ -> representative b

Your compiler will generally have type (String -> Maybe SomeValue), or
(String -> Type a -> Maybe (Value a)).

  -- ryan