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 mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by sympa.inria.fr (Postfix) with ESMTPS id BF4B67EE25 for ; Sat, 26 Oct 2013 08:05:46 +0200 (CEST) Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of oleg@okmij.org) identity=pra; client-ip=66.39.3.115; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="oleg@okmij.org"; x-sender="oleg@okmij.org"; x-conformance=sidf_compatible Received-SPF: Pass (mail3-smtp-sop.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=mail3-smtp-sop.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 (mail3-smtp-sop.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=mail3-smtp-sop.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: An0FAD5aa1JCJwNzY2dsb2JhbABZwlyBNAMYBw4IPIIlAQEEASdSBRY0aYgaBrhmj1MHFoQWA5Qqg18BlS08 X-IPAS-Result: An0FAD5aa1JCJwNzY2dsb2JhbABZwlyBNAMYBw4IPIIlAQEEASdSBRY0aYgaBrhmj1MHFoQWA5Qqg18BlS08 X-IronPort-AV: E=Sophos;i="4.93,575,1378850400"; d="scan'208";a="31949976" Received: from www1.g3.pair.com ([66.39.3.115]) by mail3-smtp-sop.national.inria.fr with SMTP; 26 Oct 2013 08:05:45 +0200 Received: (qmail 55302 invoked by uid 9370); 26 Oct 2013 06:05:43 -0000 Date: 26 Oct 2013 06:05:43 -0000 Message-ID: <20131026060543.55301.qmail@www1.g3.pair.com> From: oleg@okmij.org cc: Didier.Remy@inria.fr To: caml-list@inria.fr In-reply-to: <526A55AE.8080208@inria.fr> Subject: Re: [Caml-list] Robust left to right flow for record disambiguation First, I'd like to state the agreement with: > Also, such a biased will encourage people to write parameters of functions > in an order that works well for the uses they have in mind. I think it odd > that type inference would have such an influence in choosing the order of > function parameters. It seems the declarative model of type inference -- type checker non-deterministically choosing type parameters -- is best to program against. This model also gives the implementor enough freedom. If we need explicit propagation, we should use bi-directional type-checking, which was designed for such a case. My main point is that record-type disambiguation is the golden opportunity for tool writers, making the great case that programming must be interactive, in interaction between a programmer and a compiler. For example, when the following snippet is submitted > type t = {a: int};; > type s = {a: string};; > List.map (fun {a} -> a + 1) [({a=2} : t)];; the compiler (or a smart editor, acting on compiler's behalf) may tell the programmer that the type of {a} in fun {a} is ambiguous, and the possible candidates are the record types 't' and 's'. Which one the programmer has in mind? The user will choose, and the editor will remember user's preference by inserting the type annotation on {a} in the source code. Interactive programming has becoming a norm in Agda (I think Epigram was one of the first successful experiments). When the type system is expressive enough, interactivity seems to be the only way forward. The alternative, a sufficiently smart compiler, has not worked out every time it was tried. One of the main reasons the classical Partial Evaluation (PE) is not used nowadays, despite great promises, is that it proved hard to program against the very smart, and capricious PE. A programmer never knows what the PE may think or do. Smart programmers eventually figured out how to write code tailored to a particular PE, and have become disappointed in the process [private communication from a person who wrote a book on PE].