[Haskell-cafe] Are GADTs what I need?
Ryan Ingram
ryani.spam at gmail.com
Mon Jul 13 12:41:39 EDT 2009
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
More information about the Haskell-Cafe
mailing list