Re: [Haskell-cafe] Are GADTs what I need?

newer
Program with profiling runs faster...

older
Removing polymorphism from type...

Chris Eidhof

13 Jul 2009 13 Jul '09

11:54 a.m.

Then you could add a specific constructor for String. The main point is: the case construct only works for values, not for types. There is no typecase construct. If you want to have certain restrictions on the 'a', such as the Show class, you could also do something like this:

...

data Value where VWrapper :: (Show a) => a -> Value

If you could elaborate a bit on what you're trying to accomplish (from a higher viewpoint) then maybe we can help you some more. -chris On 13 jul 2009, at 17:42, Kev Mahoney wrote:

...

Thanks, that helps.

I was hoping to not have to parametrize Value as there is a fair bit of code to change, and it cascades down through the data structures (maybe a forall a . Value a will help here?)

I will have a go at this approach. In case anyone is interested the code is at http://github.com/KMahoney

2009/7/13 Chris Eidhof :

...
Hey Kev,

The types are "thrown away" during compile time. Therefore, if you have a constructor "VWrapper :: a -> Value" nothing is known about that "a" when you scrutinize it.

What you could do, however, is something like this:

...
data Value a where VInt :: Integer -> Value Integer ... VWrapper :: a -> Value a

And then you can write a function doSomething:

...
doSomething :: Value String -> String doSomething (VWrapper s) = s

HTH,

-chris

On 13 jul 2009, at 12:41, Kev Mahoney wrote:

...
Hi there,

I'm currently writing an interpreter that I would like to be able to use with other haskell programs. I would like to be able to pass along arbitrary types though the interpreter. I've seen hints that GADTs can do this, but I am having trouble understanding them.

So far, I've learnt you can do this:

data Value where VInt :: Integer -> Value ... VWrapper :: a -> Value

which can let you encode arbitrary 'dynamic' types into Value. I was hoping to be able to pattern match to get the value out again e.g.

doSomething :: Value -> .... doSomething (VWrapper String s) = .....

Also, anything that can help me out with GADTs in general will be much appreciated.

Thanks, Kevin. _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

Show replies by date

Kev Mahoney

13 Jul 13 Jul

12:18 p.m.

New subject: Are GADTs what I need?

Oops, wrong mail account for my last email. Apologies. What I'm trying to accomplish is being able to write haskell libraries for the interpreter that don't use the interpreter's predefined Value types, without having to edit the Value type itself and add a new constructor (i.e. it's abstracted away). I believe the concept is called 'userdata' in Lua, for example. In C interpreters it is usually accomplished by throwing away type information and casting to 'void*' and then casting back to the type to get it out again. 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. 2009/7/13 Chris Eidhof :

...

Then you could add a specific constructor for String. The main point is: the case construct only works for values, not for types. There is no typecase construct. If you want to have certain restrictions on the 'a', such as the Show class, you could also do something like this:

...
data Value where VWrapper :: (Show a) => a -> Value

If you could elaborate a bit on what you're trying to accomplish (from a higher viewpoint) then maybe we can help you some more.

-chris

On 13 jul 2009, at 17:42, Kev Mahoney wrote:

...
Thanks, that helps.

I was hoping to not have to parametrize Value as there is a fair bit of code to change, and it cascades down through the data structures (maybe a forall a . Value a will help here?)

I will have a go at this approach. In case anyone is interested the code is at http://github.com/KMahoney

2009/7/13 Chris Eidhof :

...
Hey Kev,

The types are "thrown away" during compile time. Therefore, if you have a constructor "VWrapper :: a -> Value" nothing is known about that "a" when you scrutinize it.

What you could do, however, is something like this:

...
data Value a where VInt :: Integer -> Value Integer ... VWrapper :: a -> Value a

And then you can write a function doSomething:

...
doSomething :: Value String -> String doSomething (VWrapper s) = s

HTH,

-chris

On 13 jul 2009, at 12:41, Kev Mahoney wrote:

...
Hi there,

I'm currently writing an interpreter that I would like to be able to use with other haskell programs. I would like to be able to pass along arbitrary types though the interpreter. I've seen hints that GADTs can do this, but I am having trouble understanding them.

So far, I've learnt you can do this:

data Value where VInt :: Integer -> Value ... VWrapper :: a -> Value

which can let you encode arbitrary 'dynamic' types into Value. I was hoping to be able to pattern match to get the value out again e.g.

doSomething :: Value -> .... doSomething (VWrapper String s) = .....

Also, anything that can help me out with GADTs in general will be much appreciated.

Thanks, Kevin. _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

Ryan Ingram

12:41 p.m.

New subject: Are GADTs what I need?

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

Ashley Yakeley

14 Jul 14 Jul

1:52 a.m.

New subject: Are GADTs what I need?

Ryan Ingram wrote:

...

...
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)

"Type" here is what I call a simple type witness. Simple type witnesses are useful because they can be compared by value, and if they have the same value, then they have the same type. So you can write this: data EqualType a b where MkEqualType :: EqualType t t matchWitness :: Type a -> Type b -> Maybe (EqualType a b) matchWitness TInt TInt = Just MkEqualType matchWitness TBool TBool = Just MkEqualType matchWitness TChar TChar = Just MkEqualType matchWitness (TList w1) (TList w2) = do MkEqualType <- matchWitness w1 w2 return MkEqualType matchWitness (TFun wa1 wb1) (TFun wa2 wb2) = do MkEqualType <- matchWitness wa1 wa2 MkEqualType <- matchWitness wb1 wb2 return MkEqualType matchWitness _ _ = Nothing Now whenever you match some value with MkEqualType, the compiler will infer the identity of the two types. See my "witness" package: http://hackage.haskell.org/cgi-bin/hackage-scripts/package/witness -- Ashley Yakeley

Jason Dagit

2:20 a.m.

New subject: Are GADTs what I need?

On Mon, Jul 13, 2009 at 10:52 PM, Ashley Yakeley wrote:

...

Ryan Ingram wrote:

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)

"Type" here is what I call a simple type witness. Simple type witnesses are useful because they can be compared by value, and if they have the same value, then they have the same type.

So you can write this:

data EqualType a b where MkEqualType :: EqualType t t

Is there any reason to prefer this over: data EqualType a b where MkEqualType :: EqualType a a In the darcs source code we use a definition similar to the one I just gave. I never thought about making the definition like you gave. I wonder if it would have changed things, but I'm not sure what. Your example type checks the same with both versions of EqualType and a type signature is required for matchWitness with both definitions. Playing with the two, I don't really see any way in which they are different. Certainly, both versions of MkEqualType have the same type, but I'm just surprised you don't have to involve a or b in the type of MkEqualType. After playing with both definitions for a bit, I think I see why they have the same type and behave the same way. Initially I was thinking t was an existential type, but because of where it appears it is actually universally quantifed, like the type variable 'a' in my version, so they end up being equivalent. Jason

Ashley Yakeley

2:33 a.m.

New subject: Are GADTs what I need?

On Mon, 2009-07-13 at 23:20 -0700, Jason Dagit wrote:

...

data EqualType a b where MkEqualType :: EqualType t t

Is there any reason to prefer this over: data EqualType a b where MkEqualType :: EqualType a a

They're exactly the same. Yours just looks a bit "left-biased", that's all. -- Ashley Yakeley

Luke Palmer

2:38 a.m.

New subject: Are GADTs what I need?

On Mon, Jul 13, 2009 at 10:33 PM, Ashley Yakeley wrote:

...

On Mon, 2009-07-13 at 23:20 -0700, Jason Dagit wrote:

...
data EqualType a b where MkEqualType :: EqualType t t

Is there any reason to prefer this over: data EqualType a b where MkEqualType :: EqualType a a

They're exactly the same. Yours just looks a bit "left-biased", that's all.

For GADTs I prefer the kind color: data EqualType :: * -> * -> * where MkEqualType :: EqualType a a Except I don't usually use it, because I mostly use GADT syntax pedagogically, as introduction to algebraic data types, and introducing kinds just seems to confuse things further. Luke

5792

Age (days ago)

5793

Last active (days ago)

List overview

Download

6 comments

6 participants

participants (6)

Ashley Yakeley
Chris Eidhof
Jason Dagit
Kev Mahoney
Luke Palmer
Ryan Ingram