Re: GHC Error question
Norman Ramsey wrote:
compile1 :: (Builder b box) => t -> Name -> Ir.ANF -> b t compile1 f x body = do env <- compile body empty wire (Arg W) (env x) return f class (Monad b) => Builder b box where wire :: Source box -> Sink box -> b () This program is rejected by GHC with the following message:
Ccomp.hs:54:23: Could not deduce (Builder b box1) from the context (Builder b box) arising from use of `wire' at Ccomp.hs:54:23-42
He continued, [paraphrase] however, compile1 is accepted if the signature is removed. Furthermore, the inferred signature seems identical to the one given above. That is not a bug. We observe that in the explicitly given signature of compile1
compile1 :: (Builder b box) => t -> Name -> Ir.ANF -> b t
the type variable 'box' occurs only in the constraint Builder. The use of `wire' in the body of compile1 entails the constraint `Builder b1 box1' (we alpha-renamed the type variables). Now, we know that the result of the wire is the monadic value 'b1 ()', and compile1, according to the signature, produces the monadic value 'b t. So, the typechecker concludes that b = b1. However, there is nothing in the code that lets the typechecker conclude that box1 is the same as box. Hence the error: the given constraint (Builder b box) differs from the required (Builder b box1). What to do? If applicable, add a functional dependency (either per class or per instance) so to tell the typechecker that a particular 'b' (always, or in some cases) entails the particular 'box'. That will provide the missing improvement equation `box = box1'. Or, one may use the local type variable to the same end
compile1 :: forall b t box. (Builder b box) => t -> Name -> Ir.ANF -> b t compile1 f x body = do env <- compile body empty wire ((Arg W)::Source box) (env x) return f
the explicit `forall' binder is required.
Norman Ramsey wrote:
compile1 :: (Builder b box) => t -> Name -> Ir.ANF -> b t compile1 f x body = do env <- compile body empty wire (Arg W) (env x) return f class (Monad b) => Builder b box where wire :: Source box -> Sink box -> b () This program is rejected by GHC...
He continued, [paraphrase] however, compile1 is accepted if the signature is removed. Furthermore, the inferred signature seems identical to the one given above.
That is not a bug...
What to do? If applicable, add a functional dependency ...
Or, one may use the local type variable to the same end
compile1 :: forall b t box. (Builder b box) => t -> Name -> Ir.ANF -> b t compile1 f x body = do env <- compile body empty wire ((Arg W)::Source box) (env x) return f
the explicit `forall' binder is required.
This suggestion, I like. I have always hated that ML and Haskell leave the foralls implicit. Bad design. To be sure I understand: the reason the explicit forall is required is to bring 'box' into scope so it can be used in the type constraint on (Arg W)? Norman
Or, one may use the local type variable to the same end
compile1 :: forall b t box. (Builder b box) => t -> Name -> Ir.ANF -> b t compile1 f x body = do env <- compile body empty wire ((Arg W)::Source box) (env x) return f
the explicit `forall' binder is required.
This suggestion, I like. I have always hated that ML and Haskell leave the foralls implicit. Bad design.
I'm afraid I may disagree about the quantification. Also, I'm cautious about the phrase "ML and Haskell". In GHC 6.4, local type variables behave pretty much like those in ML (actually, GHC 6.2 was closer). In GHC 6.6, the behavior is completely different! Regarding the quantification: in ML (OCaml) we can write let foo (x:'a) y = (x+1,(y:'a)) That does not mean that foo has the type forall 'a. 'a -> 'a -> ... Indeed, foo is not polymorphic and its inferred type is int -> int -> int * int. If there should be a quantifier in the above type, it probably should be 'exists' rather than 'forall'. It seems in ML, the type variables are better understood as names of some types; if two subterms are annotated with the same type variable, these two subterms must have the same type. Thus the annotation adds an equation/constraint to the pool of type equations to solve. I must admit I find that constraint-based view quite intuitive. GHC 6.6 has changed things dramatically for the sake of wobbly inference and boxy types (or boxy inference and wobbly types...). Now, a type variable is a rigid type variable. The new GHC rules are described in http://www.haskell.org/ghc/docs/latest/html/users_guide/type-extensions.html in Section 7.4.10, Lexically scoped type variables. In particular, Subsection 7.4.10.2 confirms your understanding for the need of the explicit forall. Incidentally, as far as your example is concerned, forall as a binder is required already in GHC 6.4.
oleg@pobox.com wrote:
I'm afraid I may disagree about the quantification. Also, I'm cautious about the phrase "ML and Haskell". In GHC 6.4, local type variables behave pretty much like those in ML (actually, GHC 6.2 was closer). In GHC 6.6, the behavior is completely different!
Regarding the quantification: in ML (OCaml) we can write let foo (x:'a) y = (x+1,(y:'a)) That does not mean that foo has the type forall 'a. 'a -> 'a -> ... Indeed, foo is not polymorphic and its inferred type is int -> int -> int * int. If there should be a quantifier in the above type, it probably should be 'exists' rather than 'forall'. It seems in ML, the type variables are better understood as names of some types;
Be cautious about the phrase "ML" here as well. ;-) Because what you describe only applies to OCaml. In Standard ML, the semantics of type variables in annotations is saner: the equivalent of the above declaration would be rejected. AFAICS it is basically equivalent to the new behaviour of GHC 6.6. Cheers, - Andreas
Regarding the quantification: in ML (OCaml) we can write let foo (x:'a) y = (x+1,(y:'a)) That does not mean that foo has the type forall 'a. 'a -> 'a -> ...
Type annotations in OCaml are completely broken and always have been. They use 'unifies with' instead of 'is an instance of' and it renders type annotations nearly useless. If you want to ensure that a function is polymorphic, you have to play horrible games with uninhabited types. I am extremely bitter about this. The analogous declaration in *Standard* ML, which gets this right, is fun 'a foo (x:'a) y = (x + 1, (y:'a)) and as might be expected, this declaration is vigorously rejected by the type checker. As it damn well ought to be. Thanks for the pointers to the new GHC rules. Maybe one day I will learn them well enough to know if I should be bitter about them, too :-) Norman
The analogous declaration in *Standard* ML, which gets this right, is
fun 'a foo (x:'a) y = (x + 1, (y:'a))
Following up my own post, I thought it might be kind to explain the arcana of the SML syntax. The explicit 'a between 'fun' and 'foo' is SML syntax for an explicit type-lambda (or /\ or \Lambda as you prefer). In my opinion, the syntax is a bit sneaky, but it sure is useful to be able to bind those type variables explicitly. Regrettably, I know of no way to write an explicit forall in an SML type. GHC 6.6 appears to have taken the dual approach, in which the explicit forall in the type signature magically serves also as an explicit type-lambda in the definition of the term. Since I like to keep my type language and term language distinct, I find this design a bit confusing. It would be great if it were possible to write an explicit type-lambda in the term language as well, but because Haskell does not lexically distinguish term variables from type variables, I can't imagine a convenient syntax. Norman
participants (3)
-
Norman Ramsey -
oleg＠pobox.com -
rossberg＠ps.uni-sb.de