Re: Type Pattern-Matching for Existential Types
At 2001-01-30 22:16, Lennart Augustsson wrote:
It has large and horrible implications. To do dynamic type tests you need to carry around the types at runtime. This is not something that Haskell does (at least you don't have to).
Hmm. In this: -- data Any = forall a. Any a a1 = Any 3 a2 = Any 'p' -- ...are you saying that a1 and a2 do not have to carry types at runtime? -- Ashley Yakeley, Seattle WA
Ashley Yakeley wrote:
At 2001-01-30 22:16, Lennart Augustsson wrote:
It has large and horrible implications. To do dynamic type tests you need to carry around the types at runtime. This is not something that Haskell does (at least you don't have to).
Hmm. In this:
-- data Any = forall a. Any a
a1 = Any 3 a2 = Any 'p' --
...are you saying that a1 and a2 do not have to carry types at runtime?
That's right. Your data type is actually degenerate. There is nothing you can do what so ever with a value of type Any (except pass it around). Slightly more interesting might be data Foo = forall a . Foo a (a -> Int) Now you can at least apply the function to the value after pattern matching. You don't have to carry any types around, because the type system ensures that you don't misuse the value. -- Lennart
Lennart Augustsson writes: [...]
Slightly more interesting might be data Foo = forall a . Foo a (a -> Int)
Now you can at least apply the function to the value after pattern matching. You don't have to carry any types around, because the type system ensures that you don't misuse the value.
Hi. In that particular example, I'd be more inclined to use the existential properties of lazy evaluation: packFoo x f = Foo x f -- The actual type of x is buried in the existential data Bar = Bar Int packBar x f = Bar (f x) -- The actual type of x is buried in the (f x) suspension Of course, when there are more usable things which can be retrieved from the type, an explicit existential is more appealing: data Foo' = forall a . Ord a => Foo' [a] packFoo' xs = Foo' xs -- The actual type of xs is buried in the existential data Bar' = Bar' [[Ordering]] packBar' xs = Bar' oss where oss = [[compare x1 x2 | x2 <- xs] | x1 <- xs] -- The actual type of xs is buried in the oss suspension, which -- is rather bloated Regards, Tom
participants (3)
-
Ashley Yakeley -
Lennart Augustsson -
Tom Pledger