From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Original-To: caml-list@sympa.inria.fr Delivered-To: caml-list@sympa.inria.fr Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by sympa.inria.fr (Postfix) with ESMTPS id 572B07EE25 for ; Sat, 26 Oct 2013 11:07:13 +0200 (CEST) Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of oleg@okmij.org) identity=pra; client-ip=66.39.3.115; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="oleg@okmij.org"; x-sender="oleg@okmij.org"; x-conformance=sidf_compatible Received-SPF: Pass (mail2-smtp-roc.national.inria.fr: domain of oleg@okmij.org designates 66.39.3.115 as permitted sender) identity=mailfrom; client-ip=66.39.3.115; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="oleg@okmij.org"; x-sender="oleg@okmij.org"; x-conformance=sidf_compatible; x-record-type="v=spf1" Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of postmaster@www1.g3.pair.com) identity=helo; client-ip=66.39.3.115; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="oleg@okmij.org"; x-sender="postmaster@www1.g3.pair.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AnQGAIyFa1JCJwNzY2dsb2JhbABZwmGBNAMYBw4IPIIlAQEEASdSBRY0aRQZAodrBrhYj1UHhCwDmAkBlS08 X-IPAS-Result: AnQGAIyFa1JCJwNzY2dsb2JhbABZwmGBNAMYBw4IPIIlAQEEASdSBRY0aRQZAodrBrhYj1UHhCwDmAkBlS08 X-IronPort-AV: E=Sophos;i="4.93,575,1378850400"; d="scan'208";a="38885943" Received: from www1.g3.pair.com ([66.39.3.115]) by mail2-smtp-roc.national.inria.fr with SMTP; 26 Oct 2013 11:07:11 +0200 Received: (qmail 13454 invoked by uid 9370); 26 Oct 2013 09:07:11 -0000 Date: 26 Oct 2013 09:07:11 -0000 Message-ID: <20131026090711.13453.qmail@www1.g3.pair.com> From: oleg@okmij.org To: rossberg@mpi-sws.org CC: caml-list@inria.fr CC: roberto@dicosmo.org, gabriel.scherer@gmail.com In-reply-to: <526A7A3F.2090405@mpi-sws.org> Subject: Re: [Caml-list] Equality between abstract type definitions Perhaps a bit of history may help. In the Haskell compiler GHC, until version 6 as I recall, type variables in annotations have the same semantics as presently in OCaml. That is, type variables in Haskell were all `flexible', with OCaml's scoping rules. When GHC started to play with GADTs (ca 2006), the semantics of type variables has changed -- to what Andreas is proposing. That is, type variables became rigid, like they are in SML. The scoping rules are cleaned up (although whether the rules became simpler is the subject of a debate -- there are lots of corner cases to trip the unwary). The changeover from flexible to rigid did break all code that used type variables in annotations -- including mine. Well, one learns to live with it. It wasn't the first or the last time when a new version of GHC breaks code. Almost always the change is for the better. It seems the community prefers acute but short pain to the dull and prolonged. > succ :: a -> a > succ n = n+1 > > here is the system's answer > > No instance for (Num a) > arising from a use of `+' > In the expression: n + 1 > In an equation for `succ': succ n = n + 1 > > Is this really more new-user friendly? Perhaps this is a too advanced example for new users. Polymorphic numerals of Haskell per se are not new-user friendly. One is welcome to try to explain to new users the following error message: > *Prelude> 1 + "a" > > :1163:3: > No instance for (Num [Char]) > arising from a use of `+' > Possible fix: add an instance declaration for (Num [Char]) > In the expression: 1 + "a" > In an equation for `it': it = 1 + "a" And there are people who may be tempted to follow the proposed fix. In all fairness, although the error message is greatly off-putting to the new users, the surprise does not last long and people quickly get past it. It means the education does work. The same education quickly tells the users the problem with the original succ example: the type inferred typed turns out not as general as the type specified in the annotation. The type variable cannot be quantified without constraints: the Num a constraint should be added. A better example foo :: a -> a foo = not Couldn't match type `a' with `Bool' `a' is a rigid type variable bound by the type signature for foo :: a -> a at :1165:20 Expected type: a -> a Actual type: Bool -> Bool In the expression: not In an equation for `foo': foo = not gives a much more understandable error message, even to new users. GHC error messages are generally very good: note how the error message tells where the type variable is bound. Since all type variables in Haskell are rigid, there is no longer any convenient way to tell GHC that I think two sub-expression in a large definition should have the same type. That's a pity. OCaml's type variables are great for that. OCaml type variables can be understood purely declaratively, as an assertion from the programmer that all sub-expressions marked by the same type variables must have the same type, whatever it turns out to be. I often feel the need for such annotations in Haskell. There are workarounds, but they are ugly. My own suggestion is to make clear that type variables in the 'val' declarations are universally quantified. That is, the inferred type of let foo = fun x -> x should be printed as val foo : 'a. 'a -> 'a Likewise, such syntax should be encouraged for val declarations in modules (omitting the quantifier "'a ." should also be acceptable for val declarations, perhaps prompting a warning).