On Mon, Jul 13, 2009 at 9:18 AM, Kev Mahoney
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