[Haskell] Re: GHC Error question
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 ___ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
Re: [Haskell] Re: GHC Error question
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 ___ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
[Haskell] 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... 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 ___ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
[Haskell] Re: GHC Error question
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. ___ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
Re: [Haskell] Re: GHC Error question
[EMAIL PROTECTED] 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 ___ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
