[Haskell-cafe] Re: Non-existing types in existential quantification?

[Ben Franksen]

Christopher Done wrote:
> On 1 October 2010 15:27, Henning Thielemann
> <lemming at henning-thielemann.de> wrote:
>>
>> Given the following code, that is accepted by GHC:
>>
>>> data Exist = forall a. Exist a
>>>
>>> exist :: Exist
>>> exist = Exist undefined
>>
>> What type has the 'undefined' ?
> 
> I think its type is `a'.
>>
>> So far I assumed that at runtime all objects have a concrete type. This
>> seems not to be true.

Haskell has a static type system. This means that the type is a property of
expressions in the source language, not (necessarily) something which
exists at runtime. Furthermore, polymorphic types (i.e. those which contain
type variables) such as

  Nothing :: forall a. Maybe a

are no less concrete than monomorphic ones (i.e. those which do not contain
type variables). It often happens that the 'same' expression has different
types in different contexts, and that some of them are monomorphic, even
though others are polymorphic. In this case the monomorphic type must be a
substitution instance of the polymorphic one (i.e. type variables have been
instatiated with (monomorphic) types). But I know of no rule that says
that /all/ type variables have to be instantiated eventually.  

> Consider the following program:
> 
> main = putStrLn $ show $ length [undefined :: a,undefined :: b]
> 
> A concrete type of the element in list doesn't need to be determined
> at runtime, or any time. a unifies with b, and that unifies with x in
> length :: [x] -> Int.

A simpler example is

  main = print Nothing

Cheers
Ben