[Haskell-cafe] Re: Non-existing types in existential
quantification?
Erik Hesselink
hesselink at gmail.com
Sun Oct 3 10:37:31 EDT 2010
On Sun, Oct 3, 2010 at 14:10, Daniel Fischer <daniel.is.fischer at web.de> wrote:
> 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?
GHC has the 'Any' type, and the docs state:
"It's also used to instantiate un-constrained type variables after
type checking." [1]
So I guess at least for GHC, all type variables are instantiated after
type checking?
Regards,
Erik
[1] http://www.haskell.org/ghc/docs/6.12.2/html/libraries/ghc-prim-0.2.0.0/GHC-Prim.html#t%3AAny
More information about the Haskell-Cafe
mailing list