[Haskell-cafe] Rigid type variables and their role in type checking
18 views
Skip to first unread message
Message has been deleted
Morten Olsen Lysgaard
Aug 24, 2016, 11:49:19 AM8/24/16
to Haskell Cafe
I am making a toy compiler for a polymorphic lambda calculus working of Stephen Diehls excellent Write You a Haskell [1].
I would like to add explicit type annotations to the language, eg. type signatures for functions, but yesterday stumbled over a nut I still haven't been able to crack.
The problem is with the semantics of programmer specified type annotations, type variables contained in those signatures and how they interact with the type checker.
First off, the WYAH type inference algorithm is a text-book implementation of Hindley-Milner algorithm. It is designed to take a program without any explicit type information, and if type checking succeeds, it outputs the types of every part of the AST.
This works fine, the issue surfaced when I added explicit type annotations to the AST.
Lets say I have the function:
foo1 :: a -> a
foo1 x = x
The inferred type of `foo1` is `foo1 :: t -> t`, when unified with the annotated type, `a -> a`, the substitution [t = a] is found. Everything works out, as it should.
Now consider:
foo2 :: Int -> Int
foo2 x = x
The inferred type of `foo2` is `foo2 :: t -> t` when unified with the annotated type, `Int -> Int`, a substitution [t = Int] is found. Everything works out, as it should.
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!?
This is of course not intended behavior, the type annotation on foo3 is horribly wrong, and is blatantly lying about the actual type of the function. When I found this my first instinct was to check how the Haskell compiler would check this function.
I found that Haskell complains:
Couldn't match expected type `a' with actual type `Int'
`a' is a rigid type variable bound by
the type signature for foo3 :: a -> Int at foo3.hs:1:9
As far as I understand, Haskell has the notion of a rigid type variable, which my compiler is missing, I am also guessing that these rigid type variables have different rules with respect to unification?
Where can I read more about these strange things?
I have been trying to form the rules for unification from my intuition about Haskell type checking, but still haven't grasped the whole story, eg. how does one decide if the rigid type variable can be "specialized" or not. In `foo2` it is ok to specialize `a` into `Int`, but in `foo3`, this is not ok.
I am struggling to see the underlying rules for this, and would gladly appreciate any pointers to enlightenment!
Bonus question! Given the function:
foo4 :: a -> a
foo4 x = -(x :: Int)
The inferred type of `foo4` is `foo4 :: Int -> Int`. When unified with the annotated type, `a -> a`, the substitution [a = Int] is found, everything checks out!
From intuition we know that the type annotation for `foo4` is "to general", that is, `generalness(Int -> Int) < generalness(a -> a)`, but how does one actually express that in code? That is, what is the algorithm that lies behind the function `generalness`?
[1] http://dev.stephendiehl.com/fun/
I would like to add explicit type annotations to the language, eg. type signatures for functions, but yesterday stumbled over a nut I still haven't been able to crack.
The problem is with the semantics of programmer specified type annotations, type variables contained in those signatures and how they interact with the type checker.
First off, the WYAH type inference algorithm is a text-book implementation of Hindley-Milner algorithm. It is designed to take a program without any explicit type information, and if type checking succeeds, it outputs the types of every part of the AST.
This works fine, the issue surfaced when I added explicit type annotations to the AST.
Lets say I have the function:
foo1 :: a -> a
foo1 x = x
The inferred type of `foo1` is `foo1 :: t -> t`, when unified with the annotated type, `a -> a`, the substitution [t = a] is found. Everything works out, as it should.
Now consider:
foo2 :: Int -> Int
foo2 x = x
The inferred type of `foo2` is `foo2 :: t -> t` when unified with the annotated type, `Int -> Int`, a substitution [t = Int] is found. Everything works out, as it should.
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!?
This is of course not intended behavior, the type annotation on foo3 is horribly wrong, and is blatantly lying about the actual type of the function. When I found this my first instinct was to check how the Haskell compiler would check this function.
I found that Haskell complains:
Couldn't match expected type `a' with actual type `Int'
`a' is a rigid type variable bound by
the type signature for foo3 :: a -> Int at foo3.hs:1:9
As far as I understand, Haskell has the notion of a rigid type variable, which my compiler is missing, I am also guessing that these rigid type variables have different rules with respect to unification?
Where can I read more about these strange things?
I have been trying to form the rules for unification from my intuition about Haskell type checking, but still haven't grasped the whole story, eg. how does one decide if the rigid type variable can be "specialized" or not. In `foo2` it is ok to specialize `a` into `Int`, but in `foo3`, this is not ok.
I am struggling to see the underlying rules for this, and would gladly appreciate any pointers to enlightenment!
Bonus question! Given the function:
foo4 :: a -> a
foo4 x = -(x :: Int)
The inferred type of `foo4` is `foo4 :: Int -> Int`. When unified with the annotated type, `a -> a`, the substitution [a = Int] is found, everything checks out!
From intuition we know that the type annotation for `foo4` is "to general", that is, `generalness(Int -> Int) < generalness(a -> a)`, but how does one actually express that in code? That is, what is the algorithm that lies behind the function `generalness`?
[1] http://dev.stephendiehl.com/fun/
Brandon Allbery
Aug 24, 2016, 12:29:53 PM8/24/16
to Morten Olsen Lysgaard, Haskell Cafe
On Wed, Aug 24, 2016 at 11:49 AM, Morten Olsen Lysgaard <mor...@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).
--
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
unix, openafs, kerberos, infrastructure, xmonad http://sinenomine.net
Reply all
Reply to author
Forward
0 new messages