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 340567EEF8 for ; Sun, 12 Jul 2015 21:09:16 +0200 (CEST) Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of maxime.lesourd@ens-lyon.fr) identity=pra; client-ip=140.77.51.2; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="maxime.lesourd@ens-lyon.fr"; x-sender="maxime.lesourd@ens-lyon.fr"; x-conformance=sidf_compatible Received-SPF: Pass (mail2-smtp-roc.national.inria.fr: domain of maxime.lesourd@ens-lyon.fr designates 140.77.51.2 as permitted sender) identity=mailfrom; client-ip=140.77.51.2; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="maxime.lesourd@ens-lyon.fr"; x-sender="maxime.lesourd@ens-lyon.fr"; 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@jabiru.ens-lyon.fr) identity=helo; client-ip=140.77.51.2; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="maxime.lesourd@ens-lyon.fr"; x-sender="postmaster@jabiru.ens-lyon.fr"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: A0BzBQA4uqJVhwIzTYxbFoNSaYMiggmnEgGOUIIcAQmHHkwBAQEBAQESAQEBCA0JByMuhCgUEXUBBjcCJBIBBQFXiAwNoXCCBYEsPjGLP5YSjjeCOIIXDC8SgTEFlDGEaYcbggSPTYVQNYETAhEGgWQKghxvAQGCSQEBAQ X-IPAS-Result: A0BzBQA4uqJVhwIzTYxbFoNSaYMiggmnEgGOUIIcAQmHHkwBAQEBAQESAQEBCA0JByMuhCgUEXUBBjcCJBIBBQFXiAwNoXCCBYEsPjGLP5YSjjeCOIIXDC8SgTEFlDGEaYcbggSPTYVQNYETAhEGgWQKghxvAQGCSQEBAQ X-IronPort-AV: E=Sophos;i="5.15,458,1432591200"; d="scan'208";a="169970757" Received: from jabiru.ens-lyon.fr ([140.77.51.2]) by mail2-smtp-roc.national.inria.fr with ESMTP; 12 Jul 2015 21:09:15 +0200 Received: from localhost (localhost [127.0.0.1]) by jabiru.ens-lyon.fr (Postfix) with ESMTP id 9051D1EB0CD for ; Sun, 12 Jul 2015 21:09:15 +0200 (CEST) X-Virus-Scanned: by amavisd-new-2.7.1 (20120429) (Debian) at ens-lyon.fr Received: from jabiru.ens-lyon.fr ([127.0.0.1]) by localhost (jabiru.ens-lyon.fr [127.0.0.1]) (amavisd-new, port 10024) with ESMTP id HgQSpuWHJDZs for ; Sun, 12 Jul 2015 21:09:14 +0200 (CEST) Received: from mail-lb0-f170.google.com (mail-lb0-f170.google.com [209.85.217.170]) (using TLSv1.2 with cipher ECDHE-RSA-AES128-GCM-SHA256 (128/128 bits)) (Client CN "smtp.gmail.com", Issuer "Google Internet Authority G2" (not verified)) by jabiru.ens-lyon.fr (Postfix) with ESMTPSA id B23401EB0C2 for ; Sun, 12 Jul 2015 21:09:14 +0200 (CEST) Received: by lbbpo10 with SMTP id po10so114110785lbb.3 for ; Sun, 12 Jul 2015 12:09:13 -0700 (PDT) X-Received: by 10.152.170.234 with SMTP id ap10mr29228548lac.28.1436728153945; Sun, 12 Jul 2015 12:09:13 -0700 (PDT) MIME-Version: 1.0 From: Maxime Lesourd Date: Sun, 12 Jul 2015 19:09:04 +0000 Message-ID: To: caml-list@inria.fr Content-Type: multipart/alternative; boundary=089e01229758414148051ab25766 X-Validation-by: maxime.lesourd@gmail.com Subject: [Caml-list] Modifying the typechecker --089e01229758414148051ab25766 Content-Type: text/plain; charset=UTF-8 Hello, I am trying to add session types to the OCaml language. We have an inference algorithm for a type and effect system which I am currently trying to implement by modifying the typechecker. For now I am only targeting the core of the language (no objects, GADTs) and I mostly need to be able to prevent generalization of some type variables. The issue I am running into is that documentation about this part of the compiler seems to be very sparse, I have found some documentation about ML type inference in general [1], generalization [2] and the value restriction [3] but I was wondering if there was more information available about the actual implementation of the inference algorithm. Thanks, Maxime [1] : http://cristal.inria.fr/attapl/ [2] : http://okmij.org/ftp/ML/generalization.html [3] : http://www.math.nagoya-u.ac.jp/~garrigue/papers/morepoly-long.pdf --089e01229758414148051ab25766 Content-Type: text/html; charset=UTF-8 Content-Transfer-Encoding: quoted-printable
Hello,

I am trying to add= session types to the OCaml language. We have an inference algorithm for a = type and effect system which I am currently trying to implement by modifyin= g the typechecker. For now I am only targeting the core of the language (no= objects, GADTs) and I mostly need to be able to prevent generalization of = some type variables.

The issue I am running into is that docum= entation about this part of the compiler seems to be very sparse, I have fo= und some documentation about ML type inference in general [1], generalizati= on [2] and the value restriction [3] but I was wondering if there was more = information available about the actual implementation of the inference algo= rithm.

Thanks,
Maxime
--089e01229758414148051ab25766--