From mboxrd@z Thu Jan  1 00:00:00 1970
Return-Path: <Didier.Remy@inria.fr>
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 C3EB57EE25
	for <caml-list@sympa.inria.fr>; Sat, 26 Oct 2013 16:11:16 +0200 (CEST)
X-IronPort-AV: E=Sophos;i="4.93,576,1378850400"; 
   d="scan'208";a="38909873"
Received: from ras75-4-82-229-153-115.fbx.proxad.net (HELO MP-R19.local) ([82.229.153.115])
  by mail2-relais-roc.national.inria.fr with ESMTP/TLS/DHE-RSA-CAMELLIA256-SHA; 26 Oct 2013 16:11:10 +0200
Message-ID: <526BCD7E.6030505@inria.fr>
Date: Sat, 26 Oct 2013 16:11:10 +0200
From: Didier Remy <Didier.Remy@inria.fr>
Reply-To: Didier.Remy@inria.fr
User-Agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.9; rv:24.0) Gecko/20100101 Thunderbird/24.0.1
MIME-Version: 1.0
To: caml-list@inria.fr
References: <20131026090711.13453.qmail@www1.g3.pair.com>
In-Reply-To: <20131026090711.13453.qmail@www1.g3.pair.com>
Content-Type: text/plain; charset=ISO-8859-1; format=flowed
Content-Transfer-Encoding: 7bit
Subject: Re: [Caml-list] Equality between abstract type definitions

> 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.

Indeed, both forms are useful, since in a system that does type inferenece I
may wish to specify part of the annotations but not all of it.  Rigid
variables will make the type checker complain if the inferred type is weaker
than what I expected and flexible variables allow me to omit parts of types
that I don't care about or just say that two parts of a type should be the
same without caring what these parts exactly are.

    For example, one should be able to express annotations of the form:

        for all 'a, 'b, for some 'u, ('a -> 'b) -> 'a * 'u -> 'b * 'u

    where 'u, 'v are flexible but 'a, 'b are rigid.

    Bindings should not just be in a single type annotations but in programs,
    so that two arguments can for instance be requested to have the same type.

        let g =
            let f (for some 'a) (x : 'a) (y : 'a) = ... in
        in ...

    Notice, that the inner binding has a limited scope,  which allows
    variables that will appear in the type inferred for 'a to be generalized
    in the type of f.

In fact, now that existential variables have been introduced in the
language, via local modules or gadts, there are three kinds of bindings:
rigid (universal or existential) and flexible variables. Even though
universal and existential are treated in the same way as rigid variables
which cannot be instantiated, their meaning is different and we should
probaly reflect this by a syntactic difference.

Hence, a good design (if we were to redo it from scratch) should require the
user to always explicitly bind type variables, forcing him to say how and
were there are bound.

     Didier