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

Christopher Done wrote:

On 1 October 2010 15:27, Henning Thielemann 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