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 323BC7F30A for ; Sun, 10 Mar 2013 07:55:24 +0100 (CET) Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of anthony.tavener@gmail.com) identity=pra; client-ip=209.85.215.174; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="anthony.tavener@gmail.com"; x-sender="anthony.tavener@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail2-smtp-roc.national.inria.fr: domain of anthony.tavener@gmail.com designates 209.85.215.174 as permitted sender) identity=mailfrom; client-ip=209.85.215.174; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="anthony.tavener@gmail.com"; x-sender="anthony.tavener@gmail.com"; 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@mail-ea0-f174.google.com) identity=helo; client-ip=209.85.215.174; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="anthony.tavener@gmail.com"; x-sender="postmaster@mail-ea0-f174.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AtEBAMEsPFHRVdeuiGdsb2JhbABCskuJWQGILIFYCBYOAQEBExQUBCSCKwEBBAFAARsSCwEDDAYFBAcaCBkiAREBBQEKEhkSh24BAwkGDJ4QjDKCe4NrChknAwpZiHwBBQyNS4EzBAcKDIMqA4hyjWOBHo11FimETRyBLg X-IPAS-Result: AtEBAMEsPFHRVdeuiGdsb2JhbABCskuJWQGILIFYCBYOAQEBExQUBCSCKwEBBAFAARsSCwEDDAYFBAcaCBkiAREBBQEKEhkSh24BAwkGDJ4QjDKCe4NrChknAwpZiHwBBQyNS4EzBAcKDIMqA4hyjWOBHo11FimETRyBLg X-IronPort-AV: E=Sophos;i="4.84,817,1355094000"; d="scan'208";a="6277310" Received: from mail-ea0-f174.google.com ([209.85.215.174]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/RC4-SHA; 10 Mar 2013 07:55:23 +0100 Received: by mail-ea0-f174.google.com with SMTP id q10so701770eaj.19 for ; Sat, 09 Mar 2013 22:55:23 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=mime-version:x-received:in-reply-to:references:date:message-id :subject:from:to:cc:content-type; bh=n3dveVAJ6w7MYqu0W5dQiAAh31qEvj3vldhIxragc88=; b=QnyVpAzSlTyT8LR7/S2g+kjj2qUmRFwqGXQavg1Zh8U5GUvdgwqeVSOrsTAnbaomk+ f7DcnqIJdSTtUwUdiibFpy+6NEwHxdbcnTsSWCH2C6Xs00sUQVR9fsZDOnyUcIAHYSly tazkNpLk5C51AsHDfCbP68yYfLysGxecqgFs8nuBMdberhhB396HT3Rmxyzvdlzaq7lt md0kMcwqL06nw4JhubvfdJprQSbeDJAXagO8nj6PlaZE+Q0WJexGlpwZSUxAhJW/t15F OiVN9IfPDvHnExWt6x9VfpImND9o6gt9soUZAvc8xyZwReqCZrscrk7y3bR7dktyAfVM hSkA== MIME-Version: 1.0 X-Received: by 10.14.205.68 with SMTP id i44mr23207595eeo.25.1362898523276; Sat, 09 Mar 2013 22:55:23 -0800 (PST) Received: by 10.14.2.198 with HTTP; Sat, 9 Mar 2013 22:55:23 -0800 (PST) In-Reply-To: <20130308111010.36329.qmail@www1.g3.pair.com> References: <20130308111010.36329.qmail@www1.g3.pair.com> Date: Sat, 9 Mar 2013 23:55:23 -0700 Message-ID: From: Anthony Tavener To: oleg@okmij.org Cc: "caml-list@inria.fr" Content-Type: multipart/alternative; boundary=047d7b34387a58769604d78c8a07 Subject: Re: [Caml-list] A brief guide to a bit of the OCaml type checker --047d7b34387a58769604d78c8a07 Content-Type: text/plain; charset=ISO-8859-1 This seems like a good topic to add to Lambda the Ultimate. I'm a perpetual lurker without an account, and I think "front page" topics are limited to regular contributors? I'm no type-theorist, but this is still an interesting peek under the hood. On Fri, Mar 8, 2013 at 4:10 AM, wrote: > > When studying the OCaml type checker I have come across an elegant but > seemingly little known type generalization algorithm based on type > levels. Interestingly, the same levels also help type check local > modules, existentials, and polymorphic records. I am thankful to > Didier Re'my, the discoverer of the algorithm, for describing the > bigger picture, sharing intuitions and history, and pointing out more > applications of the type levels (e.g., MLF). > > The following web page > > http://okmij.org/ftp/ML/generalization.html > > attempts to popularize the algorithm, explain it on toy type checkers > and describe its implementation in the OCaml type checker. Hopefully > one might get a better idea what the OCaml type checker is really > doing. > > > > -- > Caml-list mailing list. Subscription management and archives: > https://sympa.inria.fr/sympa/arc/caml-list > Beginner's list: http://groups.yahoo.com/group/ocaml_beginners > Bug reports: http://caml.inria.fr/bin/caml-bugs > --047d7b34387a58769604d78c8a07 Content-Type: text/html; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable
This seems like a good topic to add to Lambda the Ultimate= . I'm a perpetual lurker without an account, and I think "front pa= ge" topics are limited to regular contributors?

I'm no type-theorist, but this is still an interesting peek under the h= ood.


On Fri, Mar 8, 2013 at 4:10 AM, <oleg@okmij.org> wrote:

When studying the OCaml type checker I have come across an elegant but
seemingly little known type generalization algorithm based on type
levels. Interestingly, the same levels also help type check local
modules, existentials, and polymorphic records. I am thankful to
Didier Re'my, the discoverer of the algorithm, for describing the
bigger picture, sharing intuitions and history, and pointing out more
applications of the type levels (e.g., MLF).

The following web page

=A0 =A0 =A0 =A0 http://okmij.org/ftp/ML/generalization.html

attempts to popularize the algorithm, explain it on toy type checkers
and describe its implementation in the OCaml type checker. Hopefully
one might get a better idea what the OCaml type checker is really
doing.



--
Caml-list mailing list. =A0Subscription management and archives:
ht= tps://sympa.inria.fr/sympa/arc/caml-list
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
Bug reports: http://caml.inria.fr/bin/caml-bugs

--047d7b34387a58769604d78c8a07--