|Subject:||Re: [Haskell-cafe] How to understand the 'forall' ?|
|Date:||Wed, 16 Sep 2009 13:48:59 -0700|
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 + yf 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 yBoth 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 atI 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 _ = 1Cristiano _______________________________________________ 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
|<Prev in Thread]||Current Thread||[Next in Thread>|
|Previous by Date:||[Haskell-cafe] weak pointers and memoization (was Re: memoization), Rodney Price|
|Next by Date:||Re: [Haskell-cafe] Can't install Haskell Platform (Ubuntu 9.02), Paulo Tanimoto|
|Previous by Thread:||Re: [Haskell-cafe] How to understand the 'forall' ?, Cristiano Paris|
|Next by Thread:||Re: [Haskell-cafe] How to understand the 'forall' ?, Cristiano Paris|
|Indexes:||[Date] [Thread] [Top] [All Lists]|