[Haskell-cafe] Are GADTs what I need?

[Kev Mahoney]

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 <chris at eidhof.nl>:
> 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 <chris at eidhof.nl>:
>>>
>>> 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 at haskell.org
>>>> http://www.haskell.org/mailman/listinfo/haskell-cafe
>>>
>>>
>
>