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

On Sunday 03 October 2010 10:43:24, Henning Thielemann wrote:

On Sun, 3 Oct 2010, Ben Franksen wrote:

...

Christopher Done wrote:

...

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

This seems to be a different example, because "GHCi -Wall" says that the type variable defaults to (). Thus 'Nothing' has monomorphic type at runtime. The difference is certainly that 'print' requires a Show instance, whereas Christopher's example does not require a type constraint.

Yup. Prelude> print $ length [undefined :: a, undefined :: b] 2 Prelude> print $ length [undefined :: a, undefined :: Num b => b] <interactive>:1:32: Warning: Defaulting the following constraint(s) to type `Integer' `Num a' arising from an expression type signature at <interactive>:1:32-54 In the expression: undefined :: (Num b) => b In the first argument of `length', namely `[undefined :: a, undefined :: (Num b) => b]' In the second argument of `($)', namely `length [undefined :: a, undefined :: (Num b) => b]' 2 Prelude> print $ length [undefined :: a, undefined :: Num b => c -> b] <interactive>:1:32: Warning: Defaulting the following constraint(s) to type `Integer' `Num b' arising from an expression type signature at <interactive>:1:32-59 In the expression: undefined :: (Num b) => c -> b In the first argument of `length', namely `[undefined :: a, undefined :: (Num b) => c -> b]' In the second argument of `($)', namely `length [undefined :: a, undefined :: (Num b) => c -> b]' 2 At runtime, a type variable has to be either unconstrained or instantiated with a concrete type?

Henning Thielemann wrote:

On Sun, 3 Oct 2010, Ben Franksen wrote:

...

Christopher Done wrote:

...

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

This seems to be a different example, because "GHCi -Wall" says that the type variable defaults to (). Thus 'Nothing' has monomorphic type at runtime. The difference is certainly that 'print' requires a Show instance, whereas Christopher's example does not require a type constraint.

Right. I always forget about defaulting. This is an obscure feature of the language. Are there any programs that rely on defaulting and could not be easily re-written so as not to? Cheers Ben