[prev in list] [next in list] [prev in thread] [next in thread]
List: haskell-cafe
Subject: Re: [Haskell-cafe] Rigid type variables and their role in type checking
From: Brandon Allbery <allbery.b () gmail ! com>
Date: 2016-08-24 16:29:46
Message-ID: CAKFCL4Xf6LJAkp2rVD0BoDW7wZ=rAfpCYupJcuv8K6FZSM+moQ () mail ! gmail ! com
[Download RAW message or body]
[Attachment #2 (multipart/alternative)]
On Wed, Aug 24, 2016 at 11:49 AM, Morten Olsen Lysgaard <morten@lysgaard.no>
wrote:
> Lastly consider:
>
> foo3 :: a -> Int
> foo3 x = x
>
> The inferred type of `foo3` is, again, `foo3 :: t -> t`, when unified with
> the annotated type, `a -> Int`, we find that `t` must have the same type as
> `a`, and `t` must be of type `Int`, thus `t = a = Int`. Everything works
> out!?
I mentioned this when you were asking about this in IRC, but you may have
missed it.
All type variables are implicitly qualified at top level in standard
Haskell (and in ghc if they are not explicitly qualified at some level).
Thus the actual type signature is
foo3 :: forall a. a -> Int
and (forall a. a) does *not* unify with Int. This does not work in both
directions, though; in your second example, the *inferred* type (t -> t) is
permitted to unify with an explicitly specified type (Int -> Int). It is
only explicitly specified types that do this (this is what "rigid" means:
explicitly specified, therefore not permitted to unify with a more specific
type).
The reason for this is that the type signature specifies the contract with
callers. (a -> a) which means (forall a. a -> a) promises the caller you
will accept any (a) the *caller* chooses. This is why such explicit
signatures are rigid: you promised the caller you will accept any (a), so
you may not renege on that contract and always produce (Int).
--
brandon s allbery kf8nh sine nomine associates
allbery.b@gmail.com ballbery@sinenomine.net
unix, openafs, kerberos, infrastructure, xmonad http://sinenomine.net
[Attachment #5 (text/html)]
<div dir="ltr"><div class="gmail_extra"><br><div class="gmail_quote">On Wed, Aug 24, \
2016 at 11:49 AM, Morten Olsen Lysgaard <span dir="ltr"><<a \
href="mailto:morten@lysgaard.no" target="_blank">morten@lysgaard.no</a>></span> \
wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px \
#ccc solid;padding-left:1ex">Lastly consider:<br><br>foo3 :: a -> Int<br>foo3 x = \
x<br><br>The inferred type of `foo3` is, again, `foo3 :: t -> t`, when unified \
with the annotated type, `a -> Int`, we find that `t` must have the same type as \
`a`, and `t` must be of type `Int`, thus `t = a = Int`. Everything works \
out!?</blockquote></div><br>I mentioned this when you were asking about this in IRC, \
but you may have missed it.</div><div class="gmail_extra"><br></div><div \
class="gmail_extra">All type variables are implicitly qualified at top level in \
standard Haskell (and in ghc if they are not explicitly qualified at some level). \
Thus the actual type signature is</div><div class="gmail_extra"><br></div><div \
class="gmail_extra"> foo3 :: forall a. a -> Int</div><div \
class="gmail_extra"><br></div><div class="gmail_extra">and (forall a. a) does *not* \
unify with Int. This does not work in both directions, though; in your second \
example, the *inferred* type (t -> t) is permitted to unify with an explicitly \
specified type (Int -> Int). It is only explicitly specified types that do this \
(this is what "rigid" means: explicitly specified, therefore not permitted \
to unify with a more specific type).<br><br>The reason for this is that the type \
signature specifies the contract with callers. (a -> a) which means (forall a. a \
-> a) promises the caller you will accept any (a) the *caller* chooses. This is \
why such explicit signatures are rigid: you promised the caller you will accept any \
(a), so you may not renege on that contract and always produce (Int).<br \
clear="all"><div><br></div>-- <br><div class="gmail_signature" \
data-smartmail="gmail_signature"><div dir="ltr"><div>brandon s allbery kf8nh \
sine nomine associates</div><div><a href="mailto:allbery.b@gmail.com" \
target="_blank">allbery.b@gmail.com</a> \
<a href="mailto:ballbery@sinenomine.net" \
target="_blank">ballbery@sinenomine.net</a></div><div>unix, openafs, kerberos, \
infrastructure, xmonad <a href="http://sinenomine.net" \
target="_blank">http://sinenomine.net</a></div></div></div> </div></div>
[Attachment #6 (text/plain)]
_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
[prev in list] [next in list] [prev in thread] [next in thread]
Configure |
About |
News |
Add a list |
Sponsored by KoreLogic