From mboxrd@z Thu Jan  1 00:00:00 1970
Received: from mail1-relais-roc.national.inria.fr (mail1-relais-roc.national.inria.fr [192.134.164.82])
	by walapai.inria.fr (8.13.6/8.13.6) with ESMTP id p7K7235K021304
	for <caml-list@sympa-roc.inria.fr>; Sat, 20 Aug 2011 09:02:03 +0200
X-IronPort-Anti-Spam-Filtered: true
X-IronPort-Anti-Spam-Result: ApQAAApbT06LEwExkWdsb2JhbABCDqgSAQEBAQkLCwcUBSCBQAEBAQEDOAgBATcBDwsYLlcGiAaqQgGOCAWGSKNWOg
X-IronPort-AV: E=Sophos;i="4.68,254,1312149600"; 
   d="scan'208";a="116370026"
Received: from infao0809.mpi-sb.mpg.de (HELO hera.mpi-sb.mpg.de) ([139.19.1.49])
  by mail1-smtp-roc.national.inria.fr with ESMTP/TLS/AES256-SHA; 20 Aug 2011 09:01:57 +0200
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed;
	d=mpi-sb.mpg.de; s=mail200803; h=From:To:In-Reply-To:Subject:
	References:Message-Id:Content-Type:Content-Transfer-Encoding:
	Mime-Version:Date:Cc; bh=UMARKyFquRH9iaHKksGzL9z+HBIHdKh+pLWRMlL
	DE2k=; b=kHODg370mm4iLUxS5SihbCEzJ6m7/uD/J4pXziA5AA+K96+M5SMwjfm
	9M+9DK0/Q8PjzF32iGT+3FRRQHJTRKHUO+4u4/ZiNNUb0VmevaBr6+9SxcJQRd4f
	hNc+eYVyPFvj1Ac2nICd30wqPlZ/NLOH11VC13LkYsI8YFMMhaDc=
Received: from infao0525.mpi-klsb.mpg.de ([139.19.1.26]:59943 helo=maniac.mpi-klsb.mpg.de)
	by hera.mpi-sb.mpg.de (envelope-from <rossberg@mpi-sws.org>) 
	with esmtp (Exim 4.69) id 1QufZ2-0003d7-8v; Sat, 20 Aug 2011 09:01:54 +0200
Received: from mnch-5d875832.pool.mediaways.net ([93.135.88.50]:64962 helo=[192.168.178.31])
	by maniac.mpi-klsb.mpg.de (envelope-from <rossberg@mpi-sws.org>) 
	with esmtpsa (TLS1.0:RSA_AES_128_CBC_SHA1:16)
	(Exim 4.69) id 1QufZ1-00024V-MX; Sat, 20 Aug 2011 09:01:51 +0200
From: Andreas Rossberg <rossberg@mpi-sws.org>
To: Jacques Garrigue <garrigue@math.nagoya-u.ac.jp>
In-Reply-To: <15C8C097-A8E2-4D96-AEEC-982DBEB65DD8@math.nagoya-u.ac.jp>
References: <CAMoPVjfHn+pShaidefY7pjDYWcwciffiPQh16OkB4zHCQMVczw@mail.gmail.com> <15C8C097-A8E2-4D96-AEEC-982DBEB65DD8@math.nagoya-u.ac.jp>
Message-Id: <3F59E9D3-E0FF-4FC3-A737-39861831331B@mpi-sws.org>
Content-Type: text/plain; charset=WINDOWS-1252; format=flowed; delsp=yes
Mime-Version: 1.0 (Apple Message framework v936)
Date: Sat, 20 Aug 2011 09:01:50 +0200
Cc: Arnaud Spiwack <Arnaud.Spiwack@lix.polytechnique.fr>, caml-list@inria.fr
X-Mailer: Apple Mail (2.936)
Content-Transfer-Encoding: 8bit
X-MIME-Autoconverted: from quoted-printable to 8bit by walapai.inria.fr id p7K7235K021304
Subject: Re: [Caml-list] First-class module and higher-order types

On Aug 20, 2011, at 05.26 h, Jacques Garrigue wrote:
> On 2011/08/20, at 0:38, Arnaud Spiwack wrote:
>> 	• On the theoretical side, how hard is it to design a variant of  
>> Hindley-Milner's typing algorithm with type-family quantification?  
>> (I understand that Ocaml's typing machinery is pretty hard to  
>> change, and that it will most likely not be happening any time soon  
>> in practice)
>
> Well, Haskell has higher-order type constructors, but its type  
> system is much less structural.
> In particular, I have no idea how this would interact with recursive  
> types.

Interesting. I'm curious. The essential restriction in Haskell is that  
universally quantified type variables of non-trivial kind can only be  
instantiated with nominal type constructors (in order to avoid the  
need for higher-order unification).  Shouldn't the same work for OCaml?

Or are you referring to type normalisation for (explicit) applications  
of higher-order type constructors? Given that OCaml only allows equi- 
recursion at base kind, how could it interact in interesting ways?

Thanks,
/Andreas