Re: [Haskell-cafe] How to understand the 'forall' ?

[Dan Weston]

There is no magic here. This is merely explicit type specialization from 
the most general inferred type to something more specific. The 
denotational semantics of a function whose type is specialized does not 
change for those values belonging to the more specialized type.

f :: forall a. (Num a) => a -> a -> a
f x y = x + y

g :: Int -> Int -> Int
g x y = x + y

f and g denote (extensionally) the identical function, differing only in 
their type. g is a specialization of f. It is possible that 
(operationally) f could be slower if the compiler is not clever enough 
to avoid passing a type witness dictionary.

h :: forall b. b -> Char
h = const 'a'

k :: () -> Char
k = const 'a'

data Void
m :: Void -> Char
m = const 'a'

n :: (forall a. a) -> Char
n = const 'a'

h, k, m, and n yield *identical* values for any input compatible with 
the type of any two of the functions.

In constrast, whether a function is strict or non-strict is *not* a 
function of type specialization. Strictness is not reflected in the type 
system. Compare:

u x y = y `seq` const x y
v x y = const x y

Both have type forall a b. a -> b -> a but are denotationally different 
functions:

u 2 undefined = undefined
v 2 undefined = 2

Cristiano Paris wrote:
> On Wed, Sep 16, 2009 at 7:12 PM, Ryan Ingram <ryani.spam@xxxxxxxxx> wrote:
> > Here's the difference between these two types:
> >
> > test1 :: forall a. a -> Int
> > -- The caller of test1 determines the type for test1
> > test2 :: (forall a. a) -> Int
> > -- The internals of test2 determines what type, or types, to instantiate the
> > argument at
>
> I can easily understand your explanation for test2: the type var a is
> closed under existential (?) quantification. I can't do the same for
> test1, even if it seems that a is closed under universal (?)
> quantification as well.
>
> > Or, to put it another way, since there are no non-bottom objects of type
> > (forall a. a):
>
> Why?
>
> > test1 converts *anything* to an Int.
>
> Is the only possible implementation of test1 the one ignoring its
> argument (apart from bottom of course)?
>
> > test2 converts *nothing* to an Int
> >
> > -- type-correct implementation
> > -- instantiates the (forall a. a) argument at Int
> > test2 x = x
>
> > -- type error, the caller chose "a" and it is not necessarily Int
> > -- test1 x = x
> >
> > -- type-correct implementation: ignore the argument
> > test1 _ = 1
>
> Cristiano
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe@xxxxxxxxxxx
> http://www.haskell.org/mailman/listinfo/haskell-cafe

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