[Haskell-cafe] Language extensions [was: Memoization]

[Martin Percossi]

I really liked this explanation -- very clear, with good analogies.

Thanks!

Martin
My music: http://www.youtube.com/profile?user=thetonegrove

Claus Reinke wrote:

>
>>> quantified types (forall/exist):
>>>  an easy way to memorize this is to think of 'forall' as a big 'and'
>>>  and of 'exists' as a big 'or'.
>>>    e :: forall a. a  -- e has type 'Int' and type 'Bool' and type ..
>>>    e :: exists a. a  -- e has type 'Int' or  type 'Bool' or  type ..
>>
>>
>> That doesn't entirely make sense. (What am I on about? That doesn't 
>> make *any* sense...)
>
>
> indeed?-) then you've probably already figured out what those types
> mean! there aren't many variations of an expression that has *all* types
> ("you can't please everyone"), and if an expression has a type but we
> have no way of knowing what that type is, there isn't much we can do
> with it (like advice from the Oracle of Delphi).  but both of these
> kinds of quantified types make a lot more sense in larger contexts.
> lets take 'forall'/'big and' first: the problem with 'forall a. a' is to
> produce something that is everything to everyone, which is rather hard;
> but what about 'forall a. a -> a'? that is like a general shipping
> agency - they don't care what you give them, they just put it in a box
> and move it from one place to another (if it doesn't like to be shipped
> in such an indifferent way, it'll break, but that's not their problem);
> such general shipping is both 'Integer' shipping *and* 'String' shipping
> *and* ..; other examples are 'forall a. a -> a -> a', which is a general
> selector (given two 'a's, it returns one of them), or 'forall a,b. a 
> -> b -> a' (given an 'a' and a 'b', it returns the 'a').
>
> 'id :: forall a. a -> a' can be instantiated to 'id :: Bool -> Bool'
> *and* to 'id :: Char -> Char' *and* to all other identities on rank-1
> types besides, so one could say that it really has *all* of those types.
>
> what about 'exists'/'big or' then? the problem with 'exists a. a' is
> that while we know there exists a type, we have no way of knowing what 
> that type is, so we can't really do anything with an expression of 
> such a type.
> that is very much like an abstract data type, implemented on top
> of a hidden representation type. what we need are some operations on 
> that abstract type, so how about
>    'exists r.(r a, r a -> a -> r a, r a -> a)'
>
> we still don't know what 'r' is, but we have some 'r a', we have a way
> to combine 'r a' and 'a' into a new 'r a', and a way to extract an 'a'
> from an 'r a', so we're no longer entirely helpless. in fact, that looks
> a lot like an abstract container type, perhaps a stack with push and
> top, or a queue with add and front, or a cell with put and get. 
> whatever it may be, the 'r' is hidden, so it could be
>    '([a], [a]->a->[a], [a]->a)'
> *or* it could be
>    '(Set a, Set a -> a -> Set a, Set a -> a)'
> *or* it could be based on *any* other rank-1 type constructor.
>
> hth,
> claus
>
> oracle advice: 'invade :: exists great_empire. great_empire -> ()'
>
>
>
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe