From aravara at fct.unl.pt  Wed Jan 21 07:42:55 2015
From: aravara at fct.unl.pt (Antonio Ravara)
Date: Wed, 21 Jan 2015 12:42:55 +0000
Subject: [TYPES] Looking for concurrent imperative core Java calculi
Message-ID: <54BF9ECF.9000804@fct.unl.pt>

Dear all,

I'm looking for references of works with imperative core Java calculi 
modelling thread-based concurrency and lock-based synchronisation.

I've found Johan ?stlund and Tobias Wrigstad Welterweight Java, but I 
wonder if there are other and/or more recent works.

Thanks,
antonio
-- 
Antonio Ravara

Member of NOVA-LINCS (URL: nova-lincs.di.fct.unl.pt/)
Assistant Professor at Dep. of Informatics, FCT, Univ. NOVA de Lisboa 
(New University of Lisbon)
Web page: ctp.di.fct.unl.pt/~aravara/

From gabriel.scherer at gmail.com  Wed Jan 21 11:15:17 2015
From: gabriel.scherer at gmail.com (Gabriel Scherer)
Date: Wed, 21 Jan 2015 17:15:17 +0100
Subject: [TYPES] Looking for concurrent imperative core Java calculi
In-Reply-To: <54BF9ECF.9000804@fct.unl.pt>
References: <54BF9ECF.9000804@fct.unl.pt>
Message-ID: <CAPFanBHR9vHv6-whQtS5CHSxGja4un8KTS6nfE9K7s=jxTdh=Q@mail.gmail.com>

I'm thinking of
  Plan B: A Buffered Memory Model for Java
  Delphine Demange, Vincent Laporte, Lei Zhao, Suresh Jagannathan,
David Pichardie and Jan Vitek
  http://www.irisa.fr/celtique/pichardie/papers/popl13.pdf
but it focuses on the memory model rather than the language itself, so
the "core" calculus is minimal language-wise (it models memory read
and write, monitor locks acquire/release, creating new threads and
detecting their termination).

On Wed, Jan 21, 2015 at 1:42 PM, Antonio Ravara <aravara at fct.unl.pt> wrote:
> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
>
> Dear all,
>
> I'm looking for references of works with imperative core Java calculi
> modelling thread-based concurrency and lock-based synchronisation.
>
> I've found Johan ?stlund and Tobias Wrigstad Welterweight Java, but I wonder
> if there are other and/or more recent works.
>
> Thanks,
> antonio
> --
> Antonio Ravara
>
> Member of NOVA-LINCS (URL: nova-lincs.di.fct.unl.pt/)
> Assistant Professor at Dep. of Informatics, FCT, Univ. NOVA de Lisboa (New
> University of Lisbon)
> Web page: ctp.di.fct.unl.pt/~aravara/

From aleks0 at gmail.com  Wed Jan 21 11:26:57 2015
From: aleks0 at gmail.com (Aleks Kissinger)
Date: Wed, 21 Jan 2015 16:26:57 +0000
Subject: [TYPES] Looking for concurrent imperative core Java calculi
In-Reply-To: <54BF9ECF.9000804@fct.unl.pt>
References: <54BF9ECF.9000804@fct.unl.pt>
Message-ID: <CAJGV=uZnCM=LOi-Wb_u7nBVYh=iC2xYAwtq35UGRET6kzsQv_g@mail.gmail.com>

Dear Antonio,

It might be worth having a look at Jinja:

http://afp.sourceforge.net/entries/Jinja.shtml
http://www21.in.tum.de/~nipkow/pubs/Jinja/jinja.pdf

and Jinja with Threads:

http://afp.sourceforge.net/entries/JinjaThreads.shtml


Best,

Aleks



On 21 January 2015 at 12:42, Antonio Ravara <aravara at fct.unl.pt> wrote:
> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
>
> Dear all,
>
> I'm looking for references of works with imperative core Java calculi
> modelling thread-based concurrency and lock-based synchronisation.
>
> I've found Johan ?stlund and Tobias Wrigstad Welterweight Java, but I wonder
> if there are other and/or more recent works.
>
> Thanks,
> antonio
> --
> Antonio Ravara
>
> Member of NOVA-LINCS (URL: nova-lincs.di.fct.unl.pt/)
> Assistant Professor at Dep. of Informatics, FCT, Univ. NOVA de Lisboa (New
> University of Lisbon)
> Web page: ctp.di.fct.unl.pt/~aravara/

From massimo.merro at univr.it  Fri Jan 23 04:13:31 2015
From: massimo.merro at univr.it (Massimo Merro)
Date: Fri, 23 Jan 2015 10:13:31 +0100
Subject: [TYPES] Looking for concurrent imperative core Java calculi
In-Reply-To: <54BF9ECF.9000804@fct.unl.pt>
References: <54BF9ECF.9000804@fct.unl.pt>
Message-ID: <8A16D5ED-F4C7-492D-8023-6B1E3B559F80@univr.it>

Dear Antonio, 

we just finisched a paper on semantics for locking specifications in Java. In the paper 
you can find a core Java calculus modelling thread-based concurrency and locking semantics. 

Semantics for Locking Specifications
Michael Ernst, Damiano Macedonio, Massimo Merro and Fausto Spoto.

Here is a references:

> http://arxiv.org/abs/1501.05338


All the best, 
--Massimo


Il giorno Jan 21, 2015, alle ore 1:42 PM, Antonio Ravara ha scritto:

> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
> 
> Dear all,
> 
> I'm looking for references of works with imperative core Java calculi modelling thread-based concurrency and lock-based synchronisation.
> 
> I've found Johan ?stlund and Tobias Wrigstad Welterweight Java, but I wonder if there are other and/or more recent works.
> 
> Thanks,
> antonio
> -- 
> Antonio Ravara
> 
> Member of NOVA-LINCS (URL: nova-lincs.di.fct.unl.pt/)
> Assistant Professor at Dep. of Informatics, FCT, Univ. NOVA de Lisboa (New University of Lisbon)
> Web page: ctp.di.fct.unl.pt/~aravara/


From grosu at illinois.edu  Sat Jan 24 08:12:41 2015
From: grosu at illinois.edu (Rosu, Grigore)
Date: Sat, 24 Jan 2015 13:12:41 +0000
Subject: [TYPES] Looking for concurrent imperative core Java calculi
In-Reply-To: <8A16D5ED-F4C7-492D-8023-6B1E3B559F80@univr.it>
References: <54BF9ECF.9000804@fct.unl.pt>,
 <8A16D5ED-F4C7-492D-8023-6B1E3B559F80@univr.it>
Message-ID: <0A9D1F138D97BC4F9ACD513FCDC400174ACBD5BE@CITESMBX4.ad.uillinois.edu>

Massimo, you may also want to take a look at K-Java, recently presented at POPL'15, which is a complete formal semantics of Java 1.4 (including threads).

Grigore



________________________________________
From: Types-list [types-list-bounces at lists.seas.upenn.edu] on behalf of Massimo Merro [massimo.merro at univr.it]
Sent: Friday, January 23, 2015 3:13 AM
To: Antonio Ravara
Cc: types-list at lists.seas.upenn.edu
Subject: Re: [TYPES] Looking for concurrent imperative core Java calculi

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

Dear Antonio,

we just finisched a paper on semantics for locking specifications in Java. In the paper
you can find a core Java calculus modelling thread-based concurrency and locking semantics.

Semantics for Locking Specifications
Michael Ernst, Damiano Macedonio, Massimo Merro and Fausto Spoto.

Here is a references:

> http://arxiv.org/abs/1501.05338


All the best,
--Massimo


Il giorno Jan 21, 2015, alle ore 1:42 PM, Antonio Ravara ha scritto:

> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
>
> Dear all,
>
> I'm looking for references of works with imperative core Java calculi modelling thread-based concurrency and lock-based synchronisation.
>
> I've found Johan ?stlund and Tobias Wrigstad Welterweight Java, but I wonder if there are other and/or more recent works.
>
> Thanks,
> antonio
> --
> Antonio Ravara
>
> Member of NOVA-LINCS (URL: nova-lincs.di.fct.unl.pt/)
> Assistant Professor at Dep. of Informatics, FCT, Univ. NOVA de Lisboa (New University of Lisbon)
> Web page: ctp.di.fct.unl.pt/~aravara/


From vladimir at ias.edu  Thu Jan 29 07:46:21 2015
From: vladimir at ias.edu (Vladimir Voevodsky)
Date: Thu, 29 Jan 2015 07:46:21 -0500
Subject: [TYPES] Gentzen proof and Kantor ordering
Message-ID: <1A4DE56D-7E09-477B-90B6-40066C57B662@ias.edu>

If I recall correctly the ordinal numbers smaller than epsilon zero can be represented by finite rooted trees (non planar). It is then not difficult to describe constructively the ordinal partial ordering on them. Gentzen theorem says that if this partial ordering is well-founded then Peano arithmetic is consistent.

What can we prove about this ordering in Coq?

Can it be shown that any decidable subset in the set of trees that is inhabited has a smallest element relative to this ordering?

If not then can the system of Coq me extended *constructively* (i.e. preserving canonicity) so that in the extended system such smallest elements can be found?

Vladimir.



From n.krishnaswami at cs.bham.ac.uk  Thu Jan 29 10:10:49 2015
From: n.krishnaswami at cs.bham.ac.uk (Neelakantan Krishnaswami)
Date: Thu, 29 Jan 2015 15:10:49 +0000
Subject: [TYPES] [Coq-Club] Gentzen proof and Kantor ordering
In-Reply-To: <CAF=gwXQvq_C8qk8bd9geCQ5zwxJFW3KRrYUs=t4SLR_HUtsFOQ@mail.gmail.com>
References: <1A4DE56D-7E09-477B-90B6-40066C57B662@ias.edu>
 <CAF=gwXQvq_C8qk8bd9geCQ5zwxJFW3KRrYUs=t4SLR_HUtsFOQ@mail.gmail.com>
Message-ID: <54CA4D79.6050804@cs.bham.ac.uk>

Hello,

Paul Taylor has written about how to formulate ordinals in constructive
set theory in his paper "Intuitionistic Sets and Ordinals" [1].

The fixed point theorem Taylor mentions in the introduction to this
paper can be proved by the elegant argument of Pataraia (which Pataraia
himself never published, but Martin Escardo reproduced the proof in his
paper "Joins in the frame of nuclei" [2]).

Best,
Neel

[1] http://www.monad.me.uk/~pt/ordinals/intso.pdf
[2] http://www.cs.bham.ac.uk/~mhe/papers/hmj.pdf

On 29/01/15 14:59, roux cody wrote:
> Dear Vladimir,
>
> Coq is more than powerful enough to prove well ordering of epsilon zero,
> *for a constructive notion of well ordering*. This is usually defined by
> *accessibility*: if some property about ordinals is closed by successor
> and limits, then it holds for all ordinals.
>
> Sadly, this is not constructively equivalent to the fact that any subset
> of ordinals has a least element.
>
> The n-lab seems to sum the situation up quite nicely:
>
> http://ncatlab.org/nlab/show/well-founded+relation
>
> Without references I'm afraid.
>
> Note that the constructive formulation of well-foundedness is sufficient
> for most applications! What application did you have in mind?
>
> Best,
>
> Cody
>
> On Thu, Jan 29, 2015 at 7:46 AM, Vladimir Voevodsky <vladimir at ias.edu
> <mailto:vladimir at ias.edu>> wrote:
>
>     If I recall correctly the ordinal numbers smaller than epsilon zero
>     can be represented by finite rooted trees (non planar). It is then
>     not difficult to describe constructively the ordinal partial
>     ordering on them. Gentzen theorem says that if this partial ordering
>     is well-founded then Peano arithmetic is consistent.
>
>     What can we prove about this ordering in Coq?
>
>     Can it be shown that any decidable subset in the set of trees that
>     is inhabited has a smallest element relative to this ordering?
>
>     If not then can the system of Coq me extended *constructively* (i.e.
>     preserving canonicity) so that in the extended system such smallest
>     elements can be found?
>
>     Vladimir.
>
>
>

From freek at cs.ru.nl  Thu Jan 29 10:17:33 2015
From: freek at cs.ru.nl (Freek Wiedijk)
Date: Thu, 29 Jan 2015 16:17:33 +0100
Subject: [TYPES] [Coq-Club] Gentzen proof and Kantor ordering
In-Reply-To: <54CA4D79.6050804@cs.bham.ac.uk>
References: <1A4DE56D-7E09-477B-90B6-40066C57B662@ias.edu>
 <CAF=gwXQvq_C8qk8bd9geCQ5zwxJFW3KRrYUs=t4SLR_HUtsFOQ@mail.gmail.com>
 <54CA4D79.6050804@cs.bham.ac.uk>
Message-ID: <20150129151733.GA18493@wheezy.localdomain>

Hello,

The ordinals up to epsilon zero are one of the fundamental
notions in the ACL2 system.  See for instance:

<http://www.ccs.neu.edu/home/pete/pub/acl2-ordinal-arithmetic-acl2.pdf>

Note that in the ACL2 representation of ordinals there is
no limit constructor, it's all about powers of omega (the
"finite rooted trees" that Vladimir was talking about).

Freek

From m.escardo at cs.bham.ac.uk  Thu Jan 29 11:55:21 2015
From: m.escardo at cs.bham.ac.uk (Martin Escardo)
Date: Thu, 29 Jan 2015 16:55:21 +0000
Subject: [TYPES] Gentzen proof and Kantor ordering
In-Reply-To: <1A4DE56D-7E09-477B-90B6-40066C57B662@ias.edu>
References: <1A4DE56D-7E09-477B-90B6-40066C57B662@ias.edu>
Message-ID: <54CA65F9.1030002@cs.bham.ac.uk>



On 29/01/15 12:46, Vladimir Voevodsky wrote:
> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
>
> If I recall correctly the ordinal numbers smaller than epsilon zero can be represented by finite rooted trees (non planar). It is then not difficult to describe constructively the ordinal partial ordering on them. Gentzen theorem says that if this partial ordering is well-founded then Peano arithmetic is consistent.
>
> What can we prove about this ordering in Coq?
>
> Can it be shown that any decidable subset in the set of trees that is inhabited has a smallest element relative to this ordering?
>
> If not then can the system of Coq me extended *constructively* (i.e. preserving canonicity) so that in the extended system such smallest elements can be found?

In a weak fragment of dependent type theory, it is possible to define 
epslon0 and higher.

Here I did it in Agda, with comments explaining what is (not) needed:

http://www.cs.bham.ac.uk/~mhe/papers/ordinals/ordinals.html

Martin

From streicher at mathematik.tu-darmstadt.de  Sat Jan 31 05:47:24 2015
From: streicher at mathematik.tu-darmstadt.de (Thomas Streicher)
Date: Sat, 31 Jan 2015 11:47:24 +0100
Subject: [TYPES] Gentzen proof and Kantor ordering
In-Reply-To: <1A4DE56D-7E09-477B-90B6-40066C57B662@ias.edu>
References: <1A4DE56D-7E09-477B-90B6-40066C57B662@ias.edu>
Message-ID: <20150131104724.GA9691@mathematik.tu-darmstadt.de>

> If I recall correctly the ordinal numbers smaller than epsilon zero can be represented by finite rooted trees (non planar). It is then not difficult to describe constructively the ordinal partial ordering on them. Gentzen theorem says that if this partial ordering is well-founded then Peano arithmetic is consistent.
> 
> What can we prove about this ordering in Coq?

Already intuitionisti second order arithmetic does the job and thus so
does Coq.
Pure MLTT without universes wan't do it unless you have sufficient W-types.
But such a pure MLTT cannot even prove  not(0 = suc(x)). However,
adding a constant for that is possible and we'd arrive at a system of
the strength of HA whih can't recognize indutivity of epsilon_0.

thomas

From gershomb at gmail.com  Mon Mar  2 18:06:54 2015
From: gershomb at gmail.com (Gershom B)
Date: Mon, 2 Mar 2015 18:06:54 -0500
Subject: [TYPES] Localizing Hypotheses?
Message-ID: <CAM8RHpE7ciE4qAPQa1Zad098GsNA8Afv-1sUi-4M_Spau7kC1w@mail.gmail.com>

In the course notes for Automated Theorem Proving (2004) [1], Pfenning
describes the introduction of contexts in a Natural Deduction system as
"Localizing Hypotheses" (see section 2.3). I cannot find many other
examples of this terminology. Is this just a felicitous turn of phrase, or
is there literature that makes the connection explicit to familiar notions
of localization in, for example, algebraic, category-theoretic, or
topos-theoretic settings?

[1] http://www.cs.cmu.edu/~fp/courses/atp/handouts/ch2-natded.pdf

Thanks,
Gershom

From gabriel.scherer at gmail.com  Tue Mar  3 04:59:12 2015
From: gabriel.scherer at gmail.com (Gabriel Scherer)
Date: Tue, 3 Mar 2015 10:59:12 +0100
Subject: [TYPES] Localizing Hypotheses?
In-Reply-To: <CAM8RHpE7ciE4qAPQa1Zad098GsNA8Afv-1sUi-4M_Spau7kC1w@mail.gmail.com>
References: <CAM8RHpE7ciE4qAPQa1Zad098GsNA8Afv-1sUi-4M_Spau7kC1w@mail.gmail.com>
Message-ID: <CAPFanBHKbSErVzP_p1MkS9ZT9XHdxNG0diD5rwSiiYvyduLHoA@mail.gmail.com>

I suspect you've been reading too much into the chosen name. I simply
understand it as making local (to each step of inference rule) something
that was global to the whole derivation -- the annoying upward dots
describing hypothetical judgments, first presented page 4 of the PDF you
link, and sometimes described as bracketing of hypotheses. It is clearly
explained as such in the lecture notes. "Localization" is a fine name in
this regard, and I would be surprised if it was related to the other uses
you mention in other ways than coincidence.

On Tue, Mar 3, 2015 at 12:06 AM, Gershom B <gershomb at gmail.com> wrote:

> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list
> ]
>
> In the course notes for Automated Theorem Proving (2004) [1], Pfenning
> describes the introduction of contexts in a Natural Deduction system as
> "Localizing Hypotheses" (see section 2.3). I cannot find many other
> examples of this terminology. Is this just a felicitous turn of phrase, or
> is there literature that makes the connection explicit to familiar notions
> of localization in, for example, algebraic, category-theoretic, or
> topos-theoretic settings?
>
> [1] http://www.cs.cmu.edu/~fp/courses/atp/handouts/ch2-natded.pdf
>
> Thanks,
> Gershom
>

From fp at cs.cmu.edu  Tue Mar  3 09:06:01 2015
From: fp at cs.cmu.edu (Frank Pfenning)
Date: Tue, 3 Mar 2015 09:06:01 -0500
Subject: [TYPES] Localizing Hypotheses?
In-Reply-To: <CAPFanBHKbSErVzP_p1MkS9ZT9XHdxNG0diD5rwSiiYvyduLHoA@mail.gmail.com>
References: <CAM8RHpE7ciE4qAPQa1Zad098GsNA8Afv-1sUi-4M_Spau7kC1w@mail.gmail.com>
 <CAPFanBHKbSErVzP_p1MkS9ZT9XHdxNG0diD5rwSiiYvyduLHoA@mail.gmail.com>
Message-ID: <CAFzeOF7PCF=Vy2zHOFnO4y0Em5LfBpRYng869E+ErB4v8SwVaA@mail.gmail.com>

That's right --- I did not intend any connection to other uses of
the term "localization".

  - Frank


On Tue, Mar 3, 2015 at 4:59 AM, Gabriel Scherer <gabriel.scherer at gmail.com>
wrote:

> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list
> ]
>
> I suspect you've been reading too much into the chosen name. I simply
> understand it as making local (to each step of inference rule) something
> that was global to the whole derivation -- the annoying upward dots
> describing hypothetical judgments, first presented page 4 of the PDF you
> link, and sometimes described as bracketing of hypotheses. It is clearly
> explained as such in the lecture notes. "Localization" is a fine name in
> this regard, and I would be surprised if it was related to the other uses
> you mention in other ways than coincidence.
>
> On Tue, Mar 3, 2015 at 12:06 AM, Gershom B <gershomb at gmail.com> wrote:
>
> > [ The Types Forum,
> http://lists.seas.upenn.edu/mailman/listinfo/types-list
> > ]
> >
> > In the course notes for Automated Theorem Proving (2004) [1], Pfenning
> > describes the introduction of contexts in a Natural Deduction system as
> > "Localizing Hypotheses" (see section 2.3). I cannot find many other
> > examples of this terminology. Is this just a felicitous turn of phrase,
> or
> > is there literature that makes the connection explicit to familiar
> notions
> > of localization in, for example, algebraic, category-theoretic, or
> > topos-theoretic settings?
> >
> > [1] http://www.cs.cmu.edu/~fp/courses/atp/handouts/ch2-natded.pdf
> >
> > Thanks,
> > Gershom
> >
>



-- 
Frank Pfenning, Professor and Head
Department of Computer Science
Carnegie Mellon University
Pittsburgh, PA 15213-3891

http://www.cs.cmu.edu/~fp
+1 412 268-6343
GHC 7019

From smcdirm at microsoft.com  Wed Mar  4 20:50:08 2015
From: smcdirm at microsoft.com (Sean McDirmid)
Date: Thu, 5 Mar 2015 01:50:08 +0000
Subject: [TYPES] Basic principal type terminology
Message-ID: <3F3565D51190DB4A8944293A526072730E16D284@HKNPRD3002MB001.064d.mgd.msft.net>

Hi,

A principal type is defined in wiki as "a type for a term such that all other types for this term are an instance of it." What about a type defined as "a type for a term such that it is an instance of all types required of this term?" Whereas a principal type seems to be an intersection over bindings, such a "usage" type is a union over uses. Please forgive this OO example, but it is the best I could think of to exemplify the difference in my head:

trait HousePet
  def DoHousePetThing()
trait Mammal:
  def DoMammalThing()
trait Dog : Mammal
trait Cat : Mammal

val B : Dog
val C : Cat
A = B
A = C 
// the principal type of A is Mammal
A.DoHousePetThing()
A.DoMammalThing()
// the usage type of A is HousePet + Mammal

The principal type of A is the intersection of Dog and Cat (say Mammal). The X type I'm computing in my system is based on usage, so it is just "HousePet" + "Mammal." So while a principle type starts at top and becomes more specific with each bind (top -> Dog -> Mammal), a usage type starts at bottom and becomes more general with each use (bottom -> HousePet -> HousePet + Mammal).

Could this "usage" type be the opposite of a principal type, and if so, what has it been called in the literature? Or maybe I'm just looking at this all wrong: would such the usage type "HousePet + Mammal" still be a principle type if it was propagated backwards during type inference to bindings so that B is "Dog + HousePet" and C is "Cat + HousePet?"

Thanks,

Sean

From gabriel.scherer at gmail.com  Thu Mar  5 04:28:00 2015
From: gabriel.scherer at gmail.com (Gabriel Scherer)
Date: Thu, 5 Mar 2015 10:28:00 +0100
Subject: [TYPES] Basic principal type terminology
In-Reply-To: <3F3565D51190DB4A8944293A526072730E16D284@HKNPRD3002MB001.064d.mgd.msft.net>
References: <3F3565D51190DB4A8944293A526072730E16D284@HKNPRD3002MB001.064d.mgd.msft.net>
Message-ID: <CAPFanBG-VH7zc5yjSMLMWHbun0j_6dfRYXDa7ztdpJ4vefuB_w@mail.gmail.com>

I think you need to be more precise about the typing of assignment and
method calls. Assuming that A.DoHousePetThing() requires A to have trait
HousePet to be well-typed, Mammal cannot be the principal type of A because
it is not a valid type for A (A.DoHousePetThing() is not well-typed if we
only have (A : Mammal)). Conversely, (Mammal + Housepet) does not seem to
be a valid type for A, because intuitively (A = C) would not be well-typed.

In usual type system, there is a strong relation between what you call
"types of a term" and "required types for a time": if a type T is required
(imposed by a usage context) for a term A, then any "type for A" should be
instantiable into T, otherwise the whole program is not well-typed. In
particular, the principal type should be instantiable into any "required
type": the two notions you distinguish are equivalent.

(I suspect you've got the order reversed when you say "a type for a term
such that it is an instance of all types required of this term", my
understanding is that you rather talk about "a type which is *instantiable*
into all types required for this term". These ordering questions are always
tricky, but I think both required types HousePet and Mammal are instances
of your candidate HousePet+Mammal, not the other way around.)

On Thu, Mar 5, 2015 at 2:50 AM, Sean McDirmid <smcdirm at microsoft.com> wrote:

> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list
> ]
>
> Hi,
>
> A principal type is defined in wiki as "a type for a term such that all
> other types for this term are an instance of it." What about a type defined
> as "a type for a term such that it is an instance of all types required of
> this term?" Whereas a principal type seems to be an intersection over
> bindings, such a "usage" type is a union over uses. Please forgive this OO
> example, but it is the best I could think of to exemplify the difference in
> my head:
>
> trait HousePet
>   def DoHousePetThing()
> trait Mammal:
>   def DoMammalThing()
> trait Dog : Mammal
> trait Cat : Mammal
>
> val B : Dog
> val C : Cat
> A = B
> A = C
> // the principal type of A is Mammal
> A.DoHousePetThing()
> A.DoMammalThing()
> // the usage type of A is HousePet + Mammal
>
> The principal type of A is the intersection of Dog and Cat (say Mammal).
> The X type I'm computing in my system is based on usage, so it is just
> "HousePet" + "Mammal." So while a principle type starts at top and becomes
> more specific with each bind (top -> Dog -> Mammal), a usage type starts at
> bottom and becomes more general with each use (bottom -> HousePet ->
> HousePet + Mammal).
>
> Could this "usage" type be the opposite of a principal type, and if so,
> what has it been called in the literature? Or maybe I'm just looking at
> this all wrong: would such the usage type "HousePet + Mammal" still be a
> principle type if it was propagated backwards during type inference to
> bindings so that B is "Dog + HousePet" and C is "Cat + HousePet?"
>
> Thanks,
>
> Sean
>

From smcdirm at microsoft.com  Thu Mar  5 04:55:24 2015
From: smcdirm at microsoft.com (Sean McDirmid)
Date: Thu, 5 Mar 2015 09:55:24 +0000
Subject: [TYPES] Basic principal type terminology
In-Reply-To: <CAPFanBG-VH7zc5yjSMLMWHbun0j_6dfRYXDa7ztdpJ4vefuB_w@mail.gmail.com>
References: <3F3565D51190DB4A8944293A526072730E16D284@HKNPRD3002MB001.064d.mgd.msft.net>
 <CAPFanBG-VH7zc5yjSMLMWHbun0j_6dfRYXDa7ztdpJ4vefuB_w@mail.gmail.com>
Message-ID: <3F3565D51190DB4A8944293A526072730E16D5EF@HKNPRD3002MB001.064d.mgd.msft.net>

Hi Gabriel,

Ah, I see! I think my question was a bit confusing (or rather I was confused) since I think I conflated principal type computation vs. what a principal type is. I'm just computing the principal type differently, but it is still a principal type rather than something else, just because it came from one direction and not the other. 

Thanks for the clarification!

Sean

From: Gabriel Scherer [mailto:gabriel.scherer at gmail.com] 
Sent: Thursday, March 5, 2015 5:28 PM
To: Sean McDirmid
Cc: types-list at lists.seas.upenn.edu
Subject: Re: [TYPES] Basic principal type terminology

I think you need to be more precise about the typing of assignment and method calls. Assuming that A.DoHousePetThing() requires A to have trait HousePet to be well-typed, Mammal cannot be the principal type of A because it is not a valid type for A (A.DoHousePetThing() is not well-typed if we only have (A : Mammal)). Conversely, (Mammal + Housepet) does not seem to be a valid type for A, because intuitively (A = C) would not be well-typed.
In usual type system, there is a strong relation between what you call "types of a term" and "required types for a time": if a type T is required (imposed by a usage context) for a term A, then any "type for A" should be instantiable into T, otherwise the whole program is not well-typed. In particular, the principal type should be instantiable into any "required type": the two notions you distinguish are equivalent.
(I suspect you've got the order reversed when you say "a type for a term such that it is an instance of all types required of this term", my understanding is that you rather talk about "a type which is *instantiable* into all types required for this term". These ordering questions are always tricky, but I think both required types HousePet and Mammal are instances of your candidate HousePet+Mammal, not the other way around.)

On Thu, Mar 5, 2015 at 2:50 AM, Sean McDirmid <smcdirm at microsoft.com> wrote:
[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

Hi,

A principal type is defined in wiki as "a type for a term such that all other types for this term are an instance of it." What about a type defined as "a type for a term such that it is an instance of all types required of this term?" Whereas a principal type seems to be an intersection over bindings, such a "usage" type is a union over uses. Please forgive this OO example, but it is the best I could think of to exemplify the difference in my head:

trait HousePet
? def DoHousePetThing()
trait Mammal:
? def DoMammalThing()
trait Dog : Mammal
trait Cat : Mammal

val B : Dog
val C : Cat
A = B
A = C
// the principal type of A is Mammal
A.DoHousePetThing()
A.DoMammalThing()
// the usage type of A is HousePet + Mammal

The principal type of A is the intersection of Dog and Cat (say Mammal). The X type I'm computing in my system is based on usage, so it is just "HousePet" + "Mammal." So while a principle type starts at top and becomes more specific with each bind (top -> Dog -> Mammal), a usage type starts at bottom and becomes more general with each use (bottom -> HousePet -> HousePet + Mammal).

Could this "usage" type be the opposite of a principal type, and if so, what has it been called in the literature? Or maybe I'm just looking at this all wrong: would such the usage type "HousePet + Mammal" still be a principle type if it was propagated backwards during type inference to bindings so that B is "Dog + HousePet" and C is "Cat + HousePet?"

Thanks,

Sean


From rossberg at mpi-sws.org  Fri Mar  6 03:09:58 2015
From: rossberg at mpi-sws.org (Andreas Rossberg)
Date: Fri, 6 Mar 2015 09:09:58 +0100
Subject: [TYPES] Basic principal type terminology
In-Reply-To: <3F3565D51190DB4A8944293A526072730E16D284@HKNPRD3002MB001.064d.mgd.msft.net>
References: <3F3565D51190DB4A8944293A526072730E16D284@HKNPRD3002MB001.064d.mgd.msft.net>
Message-ID: <3E753D40-0939-4021-95E6-EEDDD3A4879C@mpi-sws.org>

On Mar 5, 2015, at 02:50 , Sean McDirmid <smcdirm at microsoft.com> wrote:
> 
> A principal type is defined in wiki as "a type for a term such that all other types for this term are an instance of it." What about a type defined as "a type for a term such that it is an instance of all types required of this term?" Whereas a principal type seems to be an intersection over bindings, such a "usage" type is a union over uses. Please forgive this OO example, but it is the best I could think of to exemplify the difference in my head:

Sounds to me like you are looking for principal typings, not principal types.

/Andreas


> 
> trait HousePet
>  def DoHousePetThing()
> trait Mammal:
>  def DoMammalThing()
> trait Dog : Mammal
> trait Cat : Mammal
> 
> val B : Dog
> val C : Cat
> A = B
> A = C 
> // the principal type of A is Mammal
> A.DoHousePetThing()
> A.DoMammalThing()
> // the usage type of A is HousePet + Mammal
> 
> The principal type of A is the intersection of Dog and Cat (say Mammal). The X type I'm computing in my system is based on usage, so it is just "HousePet" + "Mammal." So while a principle type starts at top and becomes more specific with each bind (top -> Dog -> Mammal), a usage type starts at bottom and becomes more general with each use (bottom -> HousePet -> HousePet + Mammal).
> 
> Could this "usage" type be the opposite of a principal type, and if so, what has it been called in the literature? Or maybe I'm just looking at this all wrong: would such the usage type "HousePet + Mammal" still be a principle type if it was propagated backwards during type inference to bindings so that B is "Dog + HousePet" and C is "Cat + HousePet?"
> 
> Thanks,
> 
> Sean


From r.iemhoff at uu.nl  Fri Mar 27 08:25:20 2015
From: r.iemhoff at uu.nl (Iemhoff, R. (Rosalie))
Date: Fri, 27 Mar 2015 12:25:20 +0000
Subject: [TYPES] Utrecht Workshop on Proof Theory
Message-ID: <672EA9D6-9ED2-4EFB-AB10-BE824828F890@solisom.uu.nl>

>From April 16-18, 2015 the Utrecht Workshop on Proof Theory will 
take place at Utrecht University, the Netherlands.

The aim of this workshop is to bring together researchers from 
different areas in proof theory to share results, ideas and methods.

Everybody is welcome to attend the workshop. Please register 
by sending an email to fan.yang.c at gmail.com. Giving a talk is 
by invitation only.   

For details, see http://www.phil.uu.nl/~iemhoff/Conferenties/UWPT/


From Ramana.Kumar at cl.cam.ac.uk  Thu Apr  2 13:37:10 2015
From: Ramana.Kumar at cl.cam.ac.uk (Ramana Kumar)
Date: Thu, 2 Apr 2015 18:37:10 +0100
Subject: [TYPES] completeness of type inference for stateful ML
Message-ID: <CAMej=25kAedLgokq3n_p=ghBFmzOtgBYKa-rOKZ=VswRFJBteQ@mail.gmail.com>

Hi list!

I'm looking for any pointers to proofs of (soundness and) completeness for
a type inference algorithm for ML-with-references (and the value
restriction). I'm especially interested in formal proofs.

So far, I've found some mechanised proofs about type inference algorithms
by Garrigue, by Nipkow, and by Dubois, but nothing yet that covers
imperative features like references.

Cheers,
Ramana

From james.cheney at gmail.com  Wed Apr  8 07:32:17 2015
From: james.cheney at gmail.com (James Cheney)
Date: Wed, 8 Apr 2015 12:32:17 +0100
Subject: [TYPES] mechanized formalizations of the pi calculus
Message-ID: <CAAdciC1AHc3+9HyEpPLWMM5bs4uuBs8t4-XGiYcRqwMrgsPM1A@mail.gmail.com>

Dear types-list,

I'm trying to construct a complete bibliography of formalizations/proofs of
properties of the pi calculus, or close relatives (typed, untyped, applied,
...), in any system.  The references I've found so far (from a morning of
Googling) are at the end of this message.

I have the impression that there are probably formalizations out there that
have been performed in other contexts (e.g. in modeling security
protocols), and it might not be easy to find these examples from searching
paper titles/abstracts.  Also, there may be tutorial or demo examples that
haven't been described by publications.  So, I'd welcome any suggestions
I've missed - either of formalizations themselves, or publications
describing them.

I'm also interested in understanding which approaches are suitable / have
been successful for proving different properties, and in the track records
of different approaches with respect to extensibility or reuse.

I'm happy to collect responses off-list and summarize to the list.

--James

T. F. Melham. 1994. A mechanized theory of the pi-calculus in Hol. *Nordic
J. of Computing* 1, 1 (March 1994), 50-76.

Otmane A?t Mohamed. 1995. Mechanizing a pi-Calculus Equivalence in
HOL. In *Proceedings
of the 8th International Workshop on Higher Order Logic Theorem Proving and
Its Applications*, E. Thomas Schubert, Phillip J. Windley, and Jim
Alves-Foss (Eds.). Springer-Verlag, London, UK, UK, 1-16.

Daniel Hirschkoff. 1997. A Full Formalisation of pi-Calculus Theory in the
Calculus of Constructions. In *Proceedings of the 10th International
Conference on Theorem Proving in Higher Order Logics* (TPHOLs '97), Elsa L.
Gunter and Amy P. Felty (Eds.). Springer-Verlag, London, UK, UK, 153-169.

Jo?lle Despeyroux. 2000. A Higher-Order Specification of the pi-Calculus.
In *Proceedings of the International Conference IFIP on Theoretical
Computer Science, Exploring New Frontiers of Theoretical Informatics* (TCS
'00), Jan van Leeuwen, Osamu Watanabe, Masami Hagiya, Peter D. Mosses, and
Takayasu Ito (Eds.). Springer-Verlag, London, UK, UK, 425-439.

Christine R?ckl, Daniel Hirschkoff, and Stefan Berghofer. 2001.
Higher-Order Abstract Syntax with Induction in Isabelle/HOL: Formalizing
the pi-Calculus and Mechanizing the Theory of Contexts. In *Proceedings of
the 4th International Conference on Foundations of Software Science and
Computation Structures* (FoSSaCS '01), Furio Honsell and Marino Miculan
(Eds.). Springer-Verlag, London, UK, UK, 364-378.

Simon J. Gay. 2001. A Framework for the Formalisation of Pi Calculus Type
Systems in Isabelle/HOL. In *Proceedings of the 14th International
Conference on Theorem Proving in Higher Order Logics* (TPHOLs '01), Richard
J. Boulton and Paul B. Jackson (Eds.). Springer-Verlag, London, UK, UK,
217-232.

Furio Honsell, Marino Miculan, and Ivan Scagnetto. 2001. Pi-calculus in
(Co)inductive-type theory. *Theor. Comput. Sci.* 253, 2 (February 2001),
239-285. DOI=10.1016/S0304-3975(00)00095-5
http://dx.doi.org/10.1016/S0304-3975(00)00095-5

Christine R?ckl and Daniel Hirschkoff. 2003. A fully adequate shallow
embedding of the ?-calculus in Isabelle F;HOL with mechanized syntax
analysis. *J. Funct. Program.* 13, 2 (March 2003), 415-451.
DOI=10.1017/S0956796802004653 http://dx.doi.org/10.1017/S0956796802004653

Murdoch J. Gabbay,

*in ?Thirty Five Years of Automating Mathematics?, Kluwer Applied Logic
series, Volume 28, Pages 247-269, 2004, ISBN 978-1-4020-1656-5*Alwen Tiu
and Dale Miller. 2005. A Proof Search Specification of the ?-Calculus.
*Electron.
Notes Theor. Comput. Sci.* 138, 1 (September 2005), 79-101.
DOI=10.1016/j.entcs.2005.05.006
http://dx.doi.org/10.1016/j.entcs.2005.05.006

Jesper Bengtson and Joachim Parrow. 2007. Formalising the \&\#960;-calculus
using nominal logic. In *Proceedings of the 10th international conference
on Foundations of software science and computational structures*
(FOSSACS'07), Helmut Seidl (Ed.). Springer-Verlag, Berlin, Heidelberg,
63-77.

Jesper Bengtson and Joachim Parrow. 2007. A Completeness Proof for
Bisimulation in the pi-calculus Using Isabelle. *Electron. Notes Theor.
Comput. Sci.* 192, 1 (October 2007), 61-75. DOI=10.1016/j.entcs.2007.08.017
http://dx.doi.org/10.1016/j.entcs.2007.08.017

Reynald Affeldt and Naoki Kobayashi. 2008. A Coq Library for Verification
of Concurrent Programs. *Electron. Notes Theor. Comput. Sci.* 199 (February
2008), 17-32. DOI=10.1016/j.entcs.2007.11.010
http://dx.doi.org/10.1016/j.entcs.2007.11.010

Kevin Watkins, Iliano Cervesato, Frank Pfenning, and David Walker. 2008.
Specifying Properties of Concurrent Computations in CLF. *Electron. Notes
Theor. Comput. Sci.* 199 (February 2008), 67-87.
DOI=10.1016/j.entcs.2007.11.013
http://dx.doi.org/10.1016/j.entcs.2007.11.013

Temesghen Kahsai and Marino Miculan. 2008. Implementing Spi Calculus Using
Nominal Techniques. In *Proceedings of the 4th conference on Computability
in Europe: Logic and Theory of Algorithms* (CiE '08), Arnold Beckmann,
Costas Dimitracopoulos, and Benedikt Lowe (Eds.). Springer-Verlag, Berlin,
Heidelberg, 294-305. DOI=10.1007/978-3-540-69407-6_33
http://dx.doi.org/10.1007/978-3-540-69407-6_33

Jesper Bengtson, Joachim Parrow
<http://dblp.uni-trier.de/pers/hd/p/Parrow:Joachim>:
Formalising the pi-calculus using nominal logic. Logical Methods in
Computer Science 5(2)
<http://dblp.uni-trier.de/db/journals/lmcs/lmcs5.html#abs-0809-3960> (2009)

Jesper Bengtson and Joachim Parrow. 2009. Psi-calculi in Isabelle. In
*Proceedings
of the 22nd International Conference on Theorem Proving in Higher Order
Logics* (TPHOLs '09), Stefan Berghofer, Tobias Nipkow, Christian Urban, and
Makarius Wenzel (Eds.). Springer-Verlag, Berlin, Heidelberg, 99-114.
DOI=10.1007/978-3-642-03359-9_9
http://dx.doi.org/10.1007/978-3-642-03359-9_9

Alwen Tiu and Dale Miller. 2010. Proof search specifications of
bisimulation and modal logics for the ?-calculus. *ACM Trans. Comput. Logic*
11, 2, Article 13 (January 2010), 35 pages. DOI=10.1145/1656242.1656248
http://doi.acm.org/10.1145/1656242.1656248

Jesper Bengtson, Magnus Johansson
<http://dblp.uni-trier.de/pers/hd/j/Johansson:Magnus>, Joachim Parrow
<http://dblp.uni-trier.de/pers/hd/p/Parrow:Joachim>, Bj?rn Victor
<http://dblp.uni-trier.de/pers/hd/v/Victor:Bj=ouml=rn>:
Psi-calculi: a framework for mobile processes with nominal data and
logic. Logical
Methods in Computer Science 7(1)
<http://dblp.uni-trier.de/db/journals/lmcs/lmcs7.html#abs-1101-3262> (2011)

Jesper Bengtson:
The pi-calculus in nominal logic. Archive of Formal Proofs 2012
<http://dblp.uni-trier.de/db/journals/afp/afp2012.html#Bengtson12a> (2012)

Jesper Bengtson:
Psi-calculi in Isabelle. Archive of Formal Proofs 2012
<http://dblp.uni-trier.de/db/journals/afp/afp2012.html#Bengtson12> (2012)

From james.cheney at gmail.com  Tue Apr 14 11:16:42 2015
From: james.cheney at gmail.com (James Cheney)
Date: Tue, 14 Apr 2015 16:16:42 +0100
Subject: [TYPES] mechanized formalizations of the pi calculus
In-Reply-To: <CAAdciC1AHc3+9HyEpPLWMM5bs4uuBs8t4-XGiYcRqwMrgsPM1A@mail.gmail.com>
References: <CAAdciC1AHc3+9HyEpPLWMM5bs4uuBs8t4-XGiYcRqwMrgsPM1A@mail.gmail.com>
Message-ID: <CAAdciC3eQ1JSLP3q0FEi6LKp0rJ4icQbbA_9Y641bRGw28__AQ@mail.gmail.com>

Hi again,

I have combined my original list with helpful responses from several people
to write a blog post here:

http://why-lambda.blogspot.co.uk/2015/04/mechanized-formalizations-of-pi.html

Thanks to Robert Harper, Dale Miller, Dominic Orchard, Francois Pottier,
Ivan Scagnetto, Gabriel Scherer, and Tjark Weber for their suggestions.

I'm happy to update it (or add further pointers to a follow-up post) if
there are any more responses.

--James

From hgualandi at inf.puc-rio.br  Sun Jun 14 23:08:50 2015
From: hgualandi at inf.puc-rio.br (hgualandi at inf.puc-rio.br)
Date: Mon, 15 Jun 2015 00:08:50 -0300 (BRT)
Subject: [TYPES] I'm searching for a survey on type system feature
	combinations
Message-ID: <44181.179.218.44.118.1434337730.squirrel@webmail.inf.puc-rio.br>

I'm interested in the problems that appear when you mix together different
programming language features in the same language and type system. For
example, parametric polymorphism and subtyping are very simple and easy to
use by themselves but lots of tricky variance and type inference problems
pop up when you mix both of them in a single language.

I was wondering if there exists a comprehensive survey somewhere that
covers how different type system features interact with each other. The
only one I know of is Barendregt's Lambda Cube -- each axis of the cube is
a different "feature" and each vertex corresponds to a different
combination of features. However, the Lambda Cube doesn't cover things
like subtyping, mutable references, intersection/union types, etc. Is
there something out there that does?

From gabriel.scherer at gmail.com  Mon Jun 15 11:27:19 2015
From: gabriel.scherer at gmail.com (Gabriel Scherer)
Date: Mon, 15 Jun 2015 17:27:19 +0200
Subject: [TYPES] I'm searching for a survey on type system feature
	combinations
In-Reply-To: <44181.179.218.44.118.1434337730.squirrel@webmail.inf.puc-rio.br>
References: <44181.179.218.44.118.1434337730.squirrel@webmail.inf.puc-rio.br>
Message-ID: <CAPFanBH+9s8TiDNGKFc=bxbW-K066p_3_jFW18BBWkkyc8O-tA@mail.gmail.com>

To my knowledge, the reference you ask for does not exist (and I would
be very interested if it did exist!). One reason I feel pessimistic
about such a reference is that it is not hard to throw in a few more
items to your list to end up with active research questions (for
example the best/right/satisfying way to combine "linearity" and
"dependent types" is still in discussion, as well as "dependent types"
plus "continuations").

You might however still be interested in references that cross
some of these non-trivial bridges between features, looking at
the elephant(s) from different angles. The pointers below are in no
way intended as pinpointing the first paper to discuss these ideas,
but rather entry points that I personally found enlightening on these
questions.

(1) Polymorphism, subtyping, and recursive types. An interesting work
on how to compose these features in a system that seeks to be
"maximally expressive" and remain sound is the following PhD thesis,

  "Erasable coercions: a unified approach to type systems"
  Julien Cr?tin, 2014
  http://phd.ia0.fr/

The system exposed in this work subsumes, in a composable way,
existing type systems mixing polymorphism and subtyping (such as
F-eta, various flavors of F-sub, MLF, and ML dialects with ground
subtyping constraints). It is however more on the semantic side: it
will show how to compose those features to automagically obtain an
expressive system (that is sound), but it does not tell you anything
about decidability of the resulting system or type-inference. (It also
contains a reconstruction of variance using refinement kinds.)

(2) Mutable references, subtyping and intersection/union types. I
appreciated the hands-on explanation of the interaction of mutable
state and intersection/union types in

  "Type Assignment for Intersections and Unions in Call-by-Value Languages"
  Joshua Dunfield and Frank Pfenning, 2003
  http://www.cs.cmu.edu/~joshuad/papers/union-assignment/

I found that they rather crisply motivate the need for a "context
restriction", which is the intriguing dual of the value restriction
that is not part of the working experience of ML programmers. (The
algorithmic aspect of the type system are not described in this paper
but in later work on "tridirectional type-checking"). At a more
semantic level, two papers explain *why* this phenomenon appear in
programming languages:

  "Refinement Types and Computational Duality",
  Noam Zeilberger, 2009
  http://www.cs.cmu.edu/~noam/refinements/

  "Focalisation and classical realisability",
  Guillaume Munch-Maccagnoni, 2009
  http://guillaume.munch.name/papers/#focreal

(It has been known for much longer than implicit union or existential
types require careful handling when doing syntactic soundness proof
through subject reduction, see for example "Intersection and Union
Types: Syntax and Semantics", Franco Barbanera, Mariangola
Dezani-Ciancaglini and Ugo De'Liguoro, 1995)

(3) Subtyping and mutable state, fine-grained. I was first surprised
to learn that, whereas ML-style "weak" references are invariant (and
in some sense this is the reason for the need for the value
restriction), linear, uniquely-owned "strong" references, which
support strong updates (changing the type of the reference), can
soundly be made covariant. The invariance requirement comes from the
sharing / duplicability of weak references, or the fact that its
implementation on top of strong references requires hidden state.
(There work on sound higher-order programming and sound concurrent
programming meet again: duplicable weak references and concurrent
locks seem to be two sides of the same coin.). See for example the
2014 online draft

  "The design and formalization of Mezzo, a permission-based
programming language",
  Thibaut Balabonski, Fran?ois Pottier, and Jonathan Protzenko,
  http://gallium.inria.fr/~fpottier/publis/bpp-mezzo-journal.pdf
  (the relevant remark is the bottom half of page A:35)


(4) Making them work all together. Semantic techniques have been
unreasonably effective at making all these aspects work together. For
a model of all of subtyping, mutable references, and
union/intersection, universal and existential types, and recursive
types, see for example

  "A Very Modal Model of a Modern, Major, General Type System"
  Andrew Appel, Paul-Andr? Melli?s, Christopher D. Richards, J?r?me
Vouillon, 2007
  http://www.pps.univ-paris-diderot.fr/~vouillon/publi/modalmodel.pdf

On Mon, Jun 15, 2015 at 5:08 AM,  <hgualandi at inf.puc-rio.br> wrote:
> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
>
> I'm interested in the problems that appear when you mix together different
> programming language features in the same language and type system. For
> example, parametric polymorphism and subtyping are very simple and easy to
> use by themselves but lots of tricky variance and type inference problems
> pop up when you mix both of them in a single language.
>
> I was wondering if there exists a comprehensive survey somewhere that
> covers how different type system features interact with each other. The
> only one I know of is Barendregt's Lambda Cube -- each axis of the cube is
> a different "feature" and each vertex corresponds to a different
> combination of features. However, the Lambda Cube doesn't cover things
> like subtyping, mutable references, intersection/union types, etc. Is
> there something out there that does?

From hgualandi at inf.puc-rio.br  Tue Jun 16 11:23:26 2015
From: hgualandi at inf.puc-rio.br (hgualandi at inf.puc-rio.br)
Date: Tue, 16 Jun 2015 12:23:26 -0300 (BRT)
Subject: [TYPES] I'm searching for a survey on type system feature
 combinations
In-Reply-To: <CAPFanBH+9s8TiDNGKFc=bxbW-K066p_3_jFW18BBWkkyc8O-tA@mail.gmail.com>
References: <44181.179.218.44.118.1434337730.squirrel@webmail.inf.puc-rio.br>
 <CAPFanBH+9s8TiDNGKFc=bxbW-K066p_3_jFW18BBWkkyc8O-tA@mail.gmail.com>
Message-ID: <60189.179.218.44.118.1434468206.squirrel@webmail.inf.puc-rio.br>

Thanks for the very helpful links, Julien and Gabriel. Its going to take a
while for me to fully digest all of that (its slightly above by level :))
but the basic impression I am getting so far is that it is important to at
least separate "surface-level" type system features from "kernel-level"
ones, in order to focus our attention on soundness instead of on type
inference.

Anyway, one last question: While getting a comprehensive list of how type
systems interact runs into too many open research issues, is there at
least such a thing as a "big list of kernel-level type system features"?
Are Pierces "Types and programming languages" and "advanced topics in type
systems" comprehensive or is there somewhere else I could go to if all I
cared about was a big list?

The reason I ask this is that I am working a survey on type systems for
dynamically typed languages^1 and the impression I get from the literature
on that is that it focuses a lot on type-inference issues (because you
start out from languages with no type annotations) and that almost any
kind of static program analysis counts as a type system^2. I think that a
consistent list of kernel-level type system features might help me
categorize things.

----

1^ If you want to be pedantic, type systems for statically typed dialects
of unityped languages. :)
2^ For example, some "Soft Typing" systems are actually doing
control-flow-analysis / closure-analysis to determine what lambdas from
the source code flow into each call-site. The resulting "types" are things
like "The variable f may reference the lambda from line #17 or the numeric
constant from line #18" instead of things like "f is of type int->int".
Mentioning line numbers like that is not like most type systems I am used
to.

From Peter.Sewell at cl.cam.ac.uk  Tue Jun 16 15:38:24 2015
From: Peter.Sewell at cl.cam.ac.uk (Peter Sewell)
Date: Tue, 16 Jun 2015 20:38:24 +0100
Subject: [TYPES] I'm searching for a survey on type system feature
	combinations
In-Reply-To: <60189.179.218.44.118.1434468206.squirrel@webmail.inf.puc-rio.br>
References: <44181.179.218.44.118.1434337730.squirrel@webmail.inf.puc-rio.br>
 <CAPFanBH+9s8TiDNGKFc=bxbW-K066p_3_jFW18BBWkkyc8O-tA@mail.gmail.com>
 <60189.179.218.44.118.1434468206.squirrel@webmail.inf.puc-rio.br>
Message-ID: <CAHWkzRQCKUB1Si3po00XuzUe7Ff2urCY7dCsV6MR=toDDMsicw@mail.gmail.com>

You might want to look at Levin & Pierce's TinkerType:

http://www.cis.upenn.edu/~bcpierce/papers/index.shtml#Modular%20Type%20Systems

which IIRC had some notion of type-system-feature incompatibility.

Peter

On 16 June 2015 at 16:23,  <hgualandi at inf.puc-rio.br> wrote:
> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
>
> Thanks for the very helpful links, Julien and Gabriel. Its going to take a
> while for me to fully digest all of that (its slightly above by level :))
> but the basic impression I am getting so far is that it is important to at
> least separate "surface-level" type system features from "kernel-level"
> ones, in order to focus our attention on soundness instead of on type
> inference.
>
> Anyway, one last question: While getting a comprehensive list of how type
> systems interact runs into too many open research issues, is there at
> least such a thing as a "big list of kernel-level type system features"?
> Are Pierces "Types and programming languages" and "advanced topics in type
> systems" comprehensive or is there somewhere else I could go to if all I
> cared about was a big list?
>
> The reason I ask this is that I am working a survey on type systems for
> dynamically typed languages^1 and the impression I get from the literature
> on that is that it focuses a lot on type-inference issues (because you
> start out from languages with no type annotations) and that almost any
> kind of static program analysis counts as a type system^2. I think that a
> consistent list of kernel-level type system features might help me
> categorize things.
>
> ----
>
> 1^ If you want to be pedantic, type systems for statically typed dialects
> of unityped languages. :)
> 2^ For example, some "Soft Typing" systems are actually doing
> control-flow-analysis / closure-analysis to determine what lambdas from
> the source code flow into each call-site. The resulting "types" are things
> like "The variable f may reference the lambda from line #17 or the numeric
> constant from line #18" instead of things like "f is of type int->int".
> Mentioning line numbers like that is not like most type systems I am used
> to.

From mgree at cis.upenn.edu  Tue Jun 16 15:59:49 2015
From: mgree at cis.upenn.edu (Michael Greenberg)
Date: Tue, 16 Jun 2015 15:59:49 -0400
Subject: [TYPES] I'm searching for a survey on type system feature
	combinations
Message-ID: <CACL6qXdQfqPHmsS_5EW=v-Np-MUB=8kfePo0qbQZR3gQzsy9BA@mail.gmail.com>

If you're interested in theoretical work on mixing types and dynamic
languages, the related work section of Wadler and Findler's 2007 Scheme
Workshop is a nice (but now slightly dated) place to start. Table 5.2 in my
thesis might be helpful, too (
http://repository.upenn.edu/dissertations/AAI3609166/).

There's been a lot of work on soundly mixing type disciplines with untyped
code---references (Siek and Taha 2006), effects (Ba?ados Schwerter, Garcia,
and Tanter 2014)---but some features have remained hard to incorporate. In
particular, parametric polymorphism is an open problem (but see Ahmed,
Findler, Siek, and Wadler http://plt.eecs.northwestern.edu/blame-for-all/).
People are just starting to work out details of how ADTs and other
structures work (how eagerly do we move a product type from dynamic to
static; how do we deal with wrapping and object equality [Allende, Fabry,
Garcia, Tanter 2014]).

There a lots of questions left about the right way to do things, soundness
aside (Siek, Vitousek, Cimini, and Boyland
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=5031). And of
course there's tons of work where people are trying these ideas out in real
languages (Typed Racket, Python, Ruby, JS, and I'm sure others).

Cheers,
Michael

On Tue, Jun 16, 2015 at 11:23 AM, <hgualandi at inf.puc-rio.br> wrote:

> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list
> ]
>
> Thanks for the very helpful links, Julien and Gabriel. Its going to take a
> while for me to fully digest all of that (its slightly above by level :))
> but the basic impression I am getting so far is that it is important to at
> least separate "surface-level" type system features from "kernel-level"
> ones, in order to focus our attention on soundness instead of on type
> inference.
>
> Anyway, one last question: While getting a comprehensive list of how type
> systems interact runs into too many open research issues, is there at
> least such a thing as a "big list of kernel-level type system features"?
> Are Pierces "Types and programming languages" and "advanced topics in type
> systems" comprehensive or is there somewhere else I could go to if all I
> cared about was a big list?
>
> The reason I ask this is that I am working a survey on type systems for
> dynamically typed languages^1 and the impression I get from the literature
> on that is that it focuses a lot on type-inference issues (because you
> start out from languages with no type annotations) and that almost any
> kind of static program analysis counts as a type system^2. I think that a
> consistent list of kernel-level type system features might help me
> categorize things.
>
> ----
>
> 1^ If you want to be pedantic, type systems for statically typed dialects
> of unityped languages. :)
> 2^ For example, some "Soft Typing" systems are actually doing
> control-flow-analysis / closure-analysis to determine what lambdas from
> the source code flow into each call-site. The resulting "types" are things
> like "The variable f may reference the lambda from line #17 or the numeric
> constant from line #18" instead of things like "f is of type int->int".
> Mentioning line numbers like that is not like most type systems I am used
> to.
>

From matthias at ccs.neu.edu  Tue Jun 16 18:38:20 2015
From: matthias at ccs.neu.edu (Matthias Felleisen)
Date: Tue, 16 Jun 2015 18:38:20 -0400
Subject: [TYPES] I'm searching for a survey on type system feature
	combinations
In-Reply-To: <60189.179.218.44.118.1434468206.squirrel@webmail.inf.puc-rio.br>
References: <44181.179.218.44.118.1434337730.squirrel@webmail.inf.puc-rio.br>
 <CAPFanBH+9s8TiDNGKFc=bxbW-K066p_3_jFW18BBWkkyc8O-tA@mail.gmail.com>
 <60189.179.218.44.118.1434468206.squirrel@webmail.inf.puc-rio.br>
Message-ID: <BB4A5832-CA5E-41BE-B3ED-B2EC0B84E935@ccs.neu.edu>


On Jun 16, 2015, at 11:23 AM, hgualandi at inf.puc-rio.br wrote:

> The reason I ask this is that I am working a survey on type systems for
> dynamically typed languages^1 and the impression I get from the literature
> on that is that it focuses a lot on type-inference issues (because you
> start out from languages with no type annotations) and that almost any
> kind of static program analysis counts as a type system^2. 


This is a mistaken assumption (as Michael indicated in his response). 

I have conducted research on adding types to untyped^1 languages since 1988, 
starting with a (failed) collaboration with Mike Fagan and Corky Cartwright. 

To be precise, I proposed viewing untyped languages as unityped languages 
with a universal type plus injections and projections. Fritz Henglein worked
out the idea in the mid 1990s. 

My goal has always been to work out the theory and to implement it to see 
whether it would work pragmatically. 

From ~92 to 2004, I focused on inferring types with three soft type systems: 
one based on Hindley-Milner type inference and another two using SBA (or CFA, 
almost) based type inference.  Andrew Wright's dissertation and Soft Typed Scheme
(co-adviced by Corky and myself), Cormac Flanagan's on SBA and MrSpidey Scheme, 
and Phiippe Meunier on contracted SBA were the major results along the way. 
Theoretically all three look fine. Pragmatically all three suffer from serious
problems when it comes to explaining failures of type inference. (And i can 
tell you from observations of numerous uses, that failure means suffering.)

Recognizing this problem in the late 90s, Robby Findler and I explored contracts
as (at first) a supplement for type inference and/or a replacement for type systems. 
His dissertation or our ICFP 2002 paper are good starting points. Racket (then
PLT Scheme) showed that contracts were useful, and programmers quickly started 
using them in lieu of types. 

Around 2005 I decided to try a new path with Sam Tobin-Hochstadt, the incremental 
addition of explicit type annotation. I realized that we needed to protect the 
already typed parts from untyped code, which may have different expectations of
the code than the type annotations express. Not surprisingly, contracts were the 
solution to this problem, which our experience with soft type systems had suggested. 

We immediately realized that these protection mechanisms would impose a significant
run-time cost so we focused on the conversion of entire modules. While our DSL 2006
paper does not use the slogan 'gradual typing', we essentially co-invented the 
idea one month apart from Siek and Taha (who published in the Scheme Workshop). 
Now we call 

 Siek and Taha's idea "micro gradual typing"  (applies to individual expressions) 
 our own approach we dubbed "macro gradual typing" (applies to modules only) 

The theoretical difficulty of adding type annotations to untyped languages is 
that untyped languages promote multi-typed thinking and the programming idioms
that develop show this. So your type system has to accommodate these grown idioms, 
otherwise programmers reject this. For theoretical ideas on what we need to accommodate
idioms see 

 POPL 2008
 ESOP 2009  
 ICFP 2010
 OOPSLA 2012

For practical insights, see 

 Scheme 2007
 STOP 2009 
 PLDI 2011  
 PADL 2012 
 ECOOP 2015 (my favorite related work section, start tracing back from here) 

Both the Siek/Taha approach and the Tobin-Hochstadt/Felleisen approach emphasize SOUNDness 
of the interaction. See Dimoulas 2012 for a pragmatic proof technique; Wadler and Findler
introduced a theoretical proof technique (see Michael's message) but you should also look
at Fritz's work from the mid-90s for ideas here. 

In addition to sound gradual typing, people have also explored unsound gradual typing, 
which you may also dub optional type systems. My personal acquaintance with such approaches
dates back to Common Lisp's idea of "optional types" in the mid 1980s. 

The above is my personal strand of work, not a complete history: 

-- Soft typing was anticipated by work on SmallTalk in the early 1980s; see POPL. 
-- Theoretical approaches to (gradual?) types for Lisp show up in Cartwright's dissertation (76)
-- parallel to Fagan, we also have quasi-static typing (Thatte)
-- adding DYN to statically typed languages (Abadi Cardelli Pierce and Plotkin) 

And lastly, your mail implies a compiler-biased view. There are numerous approaches
to infer something like types inside the compilers for dynamically typed languages 
for performance reasons. While I can see classifying these 'things' as types, I would
reserve the word 'type' and 'type system' for linguistic constructs that somehow
interact with the compiler. 

-----
^1 While semantically such languages are unityped, pragmatically they 
are multi-typed. Sadly and contrary to Jim Morris's advice, and perhaps 
following his example, PL researchers tend to substitute 'easy' semantics
problems for the 'hard' pragmatics problem that real programmers face in 
the real world. 

From hgualandi at inf.puc-rio.br  Tue Jun 16 19:46:37 2015
From: hgualandi at inf.puc-rio.br (hgualandi at inf.puc-rio.br)
Date: Tue, 16 Jun 2015 20:46:37 -0300 (BRT)
Subject: [TYPES] I'm searching for a survey on type system feature
 combinations
In-Reply-To: <BB4A5832-CA5E-41BE-B3ED-B2EC0B84E935@ccs.neu.edu>
References: <44181.179.218.44.118.1434337730.squirrel@webmail.inf.puc-rio.br>
 <CAPFanBH+9s8TiDNGKFc=bxbW-K066p_3_jFW18BBWkkyc8O-tA@mail.gmail.com>
 <60189.179.218.44.118.1434468206.squirrel@webmail.inf.puc-rio.br>
 <BB4A5832-CA5E-41BE-B3ED-B2EC0B84E935@ccs.neu.edu>
Message-ID: <38007.139.82.100.2.1434498397.squirrel@webmail.inf.puc-rio.br>

Maybe I shouldn't have mentioned the dynamic typing bit. That opened up a
huge can of worms... Right now the part I am having more trouble with the
"static type system" part than the "interacting between static and dynamic
code" part.

I appreciate the links on gradual typing and the discussion though. I
thought that my bibliography on that was very comprehensive but this list
is still proving me wrong :)

> This is a mistaken assumption (as Michael indicated in his response).

I agree, although I think part of it is just me not communicating precisely.

> The theoretical difficulty of adding type annotations to untyped languages
> is that untyped languages promote multi-typed thinking and the programming
> idioms that develop show this. So your type system has to accommodate
these grown
> idioms, otherwise programmers reject this.

Exactly! However what is idiomatic depends a lot on the original language.
For example, Typed Lua devotes a big chunk of their type system to model
incremental table definition via multiple assignment statements. In Typed
Racket this isn't an issue because untyped Racket already encourages you
to declare the field names in your data types. (OTOH, Typed Racket needs
to model the numeric tower and variadic map and filter, which are not
common in Lua)

What confuses me is that in an attempt to tame these dynamic language
idioms type system designers end up using almost every type system
technology under the sun. Its very overwhelming and I naively wished that
there might be something to help me organize the tools that all those
languages use.

From gabriel.scherer at gmail.com  Wed Jun 17 04:54:00 2015
From: gabriel.scherer at gmail.com (Gabriel Scherer)
Date: Wed, 17 Jun 2015 10:54:00 +0200
Subject: [TYPES] I'm searching for a survey on type system feature
	combinations
In-Reply-To: <38007.139.82.100.2.1434498397.squirrel@webmail.inf.puc-rio.br>
References: <44181.179.218.44.118.1434337730.squirrel@webmail.inf.puc-rio.br>
 <CAPFanBH+9s8TiDNGKFc=bxbW-K066p_3_jFW18BBWkkyc8O-tA@mail.gmail.com>
 <60189.179.218.44.118.1434468206.squirrel@webmail.inf.puc-rio.br>
 <BB4A5832-CA5E-41BE-B3ED-B2EC0B84E935@ccs.neu.edu>
 <38007.139.82.100.2.1434498397.squirrel@webmail.inf.puc-rio.br>
Message-ID: <CAPFanBGAjNT4QiW0_K6G48hbrFZuNMSnuhabygBpZUW4twQq_Q@mail.gmail.com>

On Wed, Jun 17, 2015 at 12:38 AM, Matthias Felleisen
<matthias at ccs.neu.edu> wrote:
> There are numerous approaches
> to infer something like types inside the compilers for dynamically typed languages
> for performance reasons. While I can see classifying these 'things' as types, I would
> reserve the word 'type' and 'type system' for linguistic constructs that somehow
> interact with the compiler.

My personal take on the nuance between "program analysis" and "type
system" is that type systems, inside the space of program analyses,
are characterized by compositionality. It is arguably a side-effect of
type-system design that it gives a way to analyze a system without the
full view of its sub-parts, only their type -- it naturally comes from
having support for abstraction. (In the general program analysis
literature, what we consider "types" are called "summaries".)

The presence of types as linguistic constructs can be
backward-justified as a consequence of this compositionality
requirement: the guarantees given on open terms / partial components
by the type system are strong enough that providing them without
explicit annotations would be undecidable, and thus they must appear
in the syntax of programs. By contrast, many program analyses used
inside compiler are either (1) composable but pure approximations
providing no guarantees at all (eg. inlineability of small functions:
as "not inlineable" is always a valid answer, it is not affected by
Rice's theorem) or (2) non-composable / whole-program, and thus
significantly easier to compute without (linguistic) help from the
user.


On Wed, Jun 17, 2015 at 1:46 AM,  <hgualandi at inf.puc-rio.br> wrote:
> What confuses me is that in an attempt to tame these dynamic language
> idioms type system designers end up using almost every type system
> technology under the sun. Its very overwhelming and I naively wished that
> there might be something to help me organize the tools that all those
> languages use.

When designing type system or type analyses for dynamically-typed
languages, I think it is very important to have a clear picture of the
workflow you have in mind for your users: it will impact the design of
your analysis greatly.
For example, if you have a requirement to be able to analyze /
type-check large existing codebases without changing them, you cannot
afford to require your users to add type annotations. This gives
strong incentives to use a simple whole-program analysis. Yet that is
in tension with the need for scalability; it's still probably easier
to pick a global analysis requiring no annotations, sacrifice some
precision, and focus on making it go really fast.
If you design linguistic constructs for your user to support the
analysis, you may still expect to let your users write the code
exactly as before (only, annotated), or require changes of idioms in
the typed part. The former approach tends to require greater
sophistication; for example it led to the introduction of occurrence
typing for Typed Racket, which is arguably more complex to type-check
than ML-style pattern-matching but supports the idiomatic Scheme style
(in ML, constructor names are required, and serve as additional
annotations).

On Wed, Jun 17, 2015 at 1:46 AM,  <hgualandi at inf.puc-rio.br> wrote:
> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
>
> Maybe I shouldn't have mentioned the dynamic typing bit. That opened up a
> huge can of worms... Right now the part I am having more trouble with the
> "static type system" part than the "interacting between static and dynamic
> code" part.
>
> I appreciate the links on gradual typing and the discussion though. I
> thought that my bibliography on that was very comprehensive but this list
> is still proving me wrong :)
>
>> This is a mistaken assumption (as Michael indicated in his response).
>
> I agree, although I think part of it is just me not communicating precisely.
>
>> The theoretical difficulty of adding type annotations to untyped languages
>> is that untyped languages promote multi-typed thinking and the programming
>> idioms that develop show this. So your type system has to accommodate
> these grown
>> idioms, otherwise programmers reject this.
>
> Exactly! However what is idiomatic depends a lot on the original language.
> For example, Typed Lua devotes a big chunk of their type system to model
> incremental table definition via multiple assignment statements. In Typed
> Racket this isn't an issue because untyped Racket already encourages you
> to declare the field names in your data types. (OTOH, Typed Racket needs
> to model the numeric tower and variadic map and filter, which are not
> common in Lua)
>
> What confuses me is that in an attempt to tame these dynamic language
> idioms type system designers end up using almost every type system
> technology under the sun. Its very overwhelming and I naively wished that
> there might be something to help me organize the tools that all those
> languages use.

From matthias at ccs.neu.edu  Wed Jun 17 08:46:37 2015
From: matthias at ccs.neu.edu (Matthias Felleisen)
Date: Wed, 17 Jun 2015 08:46:37 -0400
Subject: [TYPES] I'm searching for a survey on type system feature
	combinations
In-Reply-To: <38007.139.82.100.2.1434498397.squirrel@webmail.inf.puc-rio.br>
References: <44181.179.218.44.118.1434337730.squirrel@webmail.inf.puc-rio.br>
 <CAPFanBH+9s8TiDNGKFc=bxbW-K066p_3_jFW18BBWkkyc8O-tA@mail.gmail.com>
 <60189.179.218.44.118.1434468206.squirrel@webmail.inf.puc-rio.br>
 <BB4A5832-CA5E-41BE-B3ED-B2EC0B84E935@ccs.neu.edu>
 <38007.139.82.100.2.1434498397.squirrel@webmail.inf.puc-rio.br>
Message-ID: <A62416E1-65F8-48A0-BDC3-C6F8A542B03F@ccs.neu.edu>


On Jun 16, 2015, at 7:46 PM, hgualandi at inf.puc-rio.br wrote:

>> The theoretical difficulty of adding type annotations to untyped languages
>> is that untyped languages promote multi-typed thinking and the programming
>> idioms that develop show this. So your type system has to accommodate
> these grown
>> idioms, otherwise programmers reject this.
> 
> Exactly! However what is idiomatic depends a lot on the original language.
> For example, Typed Lua devotes a big chunk of their type system to model
> incremental table definition via multiple assignment statements. In Typed
> Racket this isn't an issue because untyped Racket already encourages you
> to declare the field names in your data types. (OTOH, Typed Racket needs
> to model the numeric tower and variadic map and filter, which are not
> common in Lua)


This is totally correct. A (sound) gradual type system must be tailored to 
the existing language because programmers (on the average) will not 
tolerate breaking their habits, i.e., changing their idioms to accommodate
the type checker. They already have (probably subconsciously) incorporated
a type-like system for thinking about their code and impedance mismatches
between two different systems of thinking are hard to overcome. (This
doesn't just apply to type systems.) 

My hunch is that 
 (1) even Lua can benefit from FP TR's most interesting innovation 
       (occurrence typing; NOTE: contrary to the implication in Gabriel's 
        next message, TR does of course NOT require a global program 
        analysis.) 

 (2) Lua might benefit from Asumu Takikawa's approach to OO TR

 (3) you would most likely benefit from Shriram Krishnamurthi and Arjun 
       Gua's work on JavaScript types because (a) they also face a table-ish 
       and imperative approach to typing. They have also pioneered an 
       elegant integration of type checking and flow analysis (and yet, 
       they integrate occurrence typing too). 

[This is partly based on meetings with Roberto.]


> What confuses me is that in an attempt to tame these dynamic language
> idioms type system designers end up using almost every type system
> technology under the sun. Its very overwhelming and I naively wished that
> there might be something to help me organize the tools that all those
> languages use.


Not only did we integrate a lot of features from existing type system work 
(true unions, parametric polymorphism; first-class polymorphism;;  local inference), we 
also had to invent and add new ideas (occurrence typing, variable-arity polymorphism, 
row-polymorphism, for mixins). Beyond that, sound gradual typing work had to 
ensure that every linguistic construct in the type language can be compiled to 
contracts (or at least, we need to error out if someone connects typed and 
untyped modules when the former use non-dynamic feature).^1 

Again the key is that dynamically typed (untyped) languages have developed
idioms that are based on programmers' ways of mixing and matching "type 
systems" to reason about their code. Whether they do it explicitly (like I do) 
or implicitly (I assume the vast majority) doesn't matter. A type system
must accommodate this mixing and matching. 

Theoreticians ought to have fun with this playing field, but I will admit, it 
first takes a lot of labor to understand the pragmatics behind a code base. 

-- Matthias

-----
^1 Always keep in mind that 'type systems' can express more properties
about program (values) than code. 



From jeremy.siek at gmail.com  Wed Jun 17 10:30:50 2015
From: jeremy.siek at gmail.com (Jeremy Siek)
Date: Wed, 17 Jun 2015 10:30:50 -0400
Subject: [TYPES] I'm searching for a survey on type system feature
	combinations
In-Reply-To: <38007.139.82.100.2.1434498397.squirrel@webmail.inf.puc-rio.br>
References: <44181.179.218.44.118.1434337730.squirrel@webmail.inf.puc-rio.br>
 <CAPFanBH+9s8TiDNGKFc=bxbW-K066p_3_jFW18BBWkkyc8O-tA@mail.gmail.com>
 <60189.179.218.44.118.1434468206.squirrel@webmail.inf.puc-rio.br>
 <BB4A5832-CA5E-41BE-B3ED-B2EC0B84E935@ccs.neu.edu>
 <38007.139.82.100.2.1434498397.squirrel@webmail.inf.puc-rio.br>
Message-ID: <CA+_ehTRP+VRKByuRnD59=cmB02cyp6+4EwH0i+cgshu5NOtRNA@mail.gmail.com>

Sam maintains a bibliography of papers related to gradual typing:

https://github.com/samth/gradual-typing-bib

Cheers,
Jeremy


On Tue, Jun 16, 2015 at 7:46 PM, <hgualandi at inf.puc-rio.br> wrote:

> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list
> ]
>
> Maybe I shouldn't have mentioned the dynamic typing bit. That opened up a
> huge can of worms... Right now the part I am having more trouble with the
> "static type system" part than the "interacting between static and dynamic
> code" part.
>
> I appreciate the links on gradual typing and the discussion though. I
> thought that my bibliography on that was very comprehensive but this list
> is still proving me wrong :)
>
> > This is a mistaken assumption (as Michael indicated in his response).
>
> I agree, although I think part of it is just me not communicating
> precisely.
>
> > The theoretical difficulty of adding type annotations to untyped
> languages
> > is that untyped languages promote multi-typed thinking and the
> programming
> > idioms that develop show this. So your type system has to accommodate
> these grown
> > idioms, otherwise programmers reject this.
>
> Exactly! However what is idiomatic depends a lot on the original language.
> For example, Typed Lua devotes a big chunk of their type system to model
> incremental table definition via multiple assignment statements. In Typed
> Racket this isn't an issue because untyped Racket already encourages you
> to declare the field names in your data types. (OTOH, Typed Racket needs
> to model the numeric tower and variadic map and filter, which are not
> common in Lua)
>
> What confuses me is that in an attempt to tame these dynamic language
> idioms type system designers end up using almost every type system
> technology under the sun. Its very overwhelming and I naively wished that
> there might be something to help me organize the tools that all those
> languages use.
>

From dreyer at mpi-sws.org  Wed Jun 17 15:18:40 2015
From: dreyer at mpi-sws.org (Derek Dreyer)
Date: Wed, 17 Jun 2015 12:18:40 -0700
Subject: [TYPES] I'm searching for a survey on type system feature
	combinations
In-Reply-To: <44181.179.218.44.118.1434337730.squirrel@webmail.inf.puc-rio.br>
References: <44181.179.218.44.118.1434337730.squirrel@webmail.inf.puc-rio.br>
Message-ID: <CAEX2k5GvRMDP7_+bmUUtkt3sWDa_Q8jdb0B1rqev5BuRDMLJHw@mail.gmail.com>

To inject a different point of view into this discussion:

There's a lot more to the "interaction" of different type system
features than just how the combination of those features affects
typechecking, type soundness, etc., which seems to be the main focus
of the discussion so far.  In particular, from my perspective, one of
the most important functions of types (particularly ADTs) is to enable
programmers to reason modularly about their code.  And indeed
programmers often do alarmingly sophisticated (informal) modular
reasoning about their code without batting an eye.  But the
correctness of such reasoning can be easily subverted by subtle
interaction of language features.

I myself got interested in semantics and verification research about 8
years ago, when I realized that the correctness of very standard kinds
of programming patterns, involving the ubiquitous combination of
higher-order functions, ADTs and mutable state, did not rest on any
solid semantic foundations.  There had been a long line of prior work
attempting to build such foundations, by Reynolds, Oles, O'Hearn,
Tennent, Felleisen, Hieb, Mason, Talcott, Birkedal, Harper, Pitts,
Stark, Reddy, Benton, Sumii, Pierce, St?vring, Lassen, Levy, and
Sangiorgi, among others, but it was not up to the task of accounting
for the unrestricted combination of such features that one finds in,
say, ML.  This led us to a series of papers attempting to establish
such foundations, building on recent developments in Kripke logical
relations (notably Appel et al.'s "step-indexing" technique).  A good
entry point would be these two papers (although I would suggest you
gloss over the technical details at first and focus on the informal
exposition):

- "State-dependent representation independence."
Ahmed, Dreyer, Rossberg.  In POPL 2009.
http://www.mpi-sws.org/~dreyer/papers/sdri/main-short.pdf

- "The impact of higher-order state and control effects on local
relational reasoning."
Dreyer, Neis, Birkedal.  In ICFP 2010, later in JFP'12.
http://www.mpi-sws.org/~dreyer/papers/stslr/journal.pdf

There were also various competing approaches based on different kinds
of bisimulations -- see the latter paper above for citations and
comparison.  That paper in particular was inspired by Abramsky et
al.'s work on the "semantic cube", a programme in game semantics
research to build fully abstract characterizations of different axes
in the design space of language expressiveness (e.g. control
operators, higher-order state) in terms of the presence/absence of
various restrictions on game strategies.  We developed some analogous
axes in the reasoning space of Kripke logical relations.  However, the
particular techniques we used were pretty different from the
game-semantic ones, and our focus was on developing practical
techniques for reasoning about common programming patterns rather than
on full abstraction.

In more recent years, we (and various collaborators) have extended
these kinds of semantic models to handle features like concurrency and
substructural typing as well, and we have developed higher-order
separation logics for abstracting the relevant reasoning principles
that these models support.  We have not (yet) looked at
intersection/union types or subtyping.

Best regards,
Derek


On Sun, Jun 14, 2015 at 8:08 PM,  <hgualandi at inf.puc-rio.br> wrote:
> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
>
> I'm interested in the problems that appear when you mix together different
> programming language features in the same language and type system. For
> example, parametric polymorphism and subtyping are very simple and easy to
> use by themselves but lots of tricky variance and type inference problems
> pop up when you mix both of them in a single language.
>
> I was wondering if there exists a comprehensive survey somewhere that
> covers how different type system features interact with each other. The
> only one I know of is Barendregt's Lambda Cube -- each axis of the cube is
> a different "feature" and each vertex corresponds to a different
> combination of features. However, the Lambda Cube doesn't cover things
> like subtyping, mutable references, intersection/union types, etc. Is
> there something out there that does?

From n.krishnaswami at cs.bham.ac.uk  Thu Jun 18 06:04:05 2015
From: n.krishnaswami at cs.bham.ac.uk (Neelakantan Krishnaswami)
Date: Thu, 18 Jun 2015 11:04:05 +0100
Subject: [TYPES] I'm searching for a survey on type system feature
	combinations
In-Reply-To: <CAEX2k5GvRMDP7_+bmUUtkt3sWDa_Q8jdb0B1rqev5BuRDMLJHw@mail.gmail.com>
References: <44181.179.218.44.118.1434337730.squirrel@webmail.inf.puc-rio.br>
 <CAEX2k5GvRMDP7_+bmUUtkt3sWDa_Q8jdb0B1rqev5BuRDMLJHw@mail.gmail.com>
Message-ID: <55829795.5050508@cs.bham.ac.uk>

On 17/06/15 20:18, Derek Dreyer wrote:
>
> In more recent years, we (and various collaborators) have extended
> these kinds of semantic models to handle features like concurrency and
> substructural typing as well, and we have developed higher-order
> separation logics for abstracting the relevant reasoning principles
> that these models support.  We have not (yet) looked at
> intersection/union types or subtyping.

This is veering off the original topic quite a bit, but Pierre
Pradic, Nick Benton and I looked at integrating intersection
types and and substructural/dependent types in our POPL 2015
paper "Integrating Linear and Dependent Types".

It turns out that intersection function work rather like
a type-theoretic analogue of "logical variables" from Hoare
logic. Paul-Andre Mellies and Noam Zeilberger give a
categorical account of this fact in their POPL 2015 paper
"Functors are Type Refinement Systems".

Best,
Neel

PS -- Slightly farther afield, Alexandre Miquel gave a denotational
model of the implicit calculus of constructions in terms of
coherence spaces and stable functions,  which can be thought of
as a way of presenting state machines and simulation relations
(see Uday Reddy's "Global State Considered Unnecessary"). As a
result it seems plausible to me that there are some deep
connections between intersection types and protocol-based
reasoning about state.


From gc at pps.univ-paris-diderot.fr  Thu Jun 18 08:24:42 2015
From: gc at pps.univ-paris-diderot.fr (Giuseppe Castagna)
Date: Thu, 18 Jun 2015 14:24:42 +0200
Subject: [TYPES] I'm searching for a survey on type system feature
	combinations
In-Reply-To: <44181.179.218.44.118.1434337730.squirrel@webmail.inf.puc-rio.br>
References: <44181.179.218.44.118.1434337730.squirrel@webmail.inf.puc-rio.br>
Message-ID: <5582B88A.5020802@pps.univ-paris-diderot.fr>

On 15/06/15 05:08, hgualandi at inf.puc-rio.br wrote:
> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

> I was wondering if there exists a comprehensive survey somewhere that
> covers how different type system features interact with each other. The
> only one I know of is Barendregt's Lambda Cube -- each axis of the cube is
> a different "feature" and each vertex corresponds to a different
> combination of features. However, the Lambda Cube doesn't cover things
> like subtyping, mutable references, intersection/union types, etc. Is
> there something out there that does?
>



It is not a survey but if you want an actual language that uses
subtyping, mutable references, union/intersection/negation types, then
you can try CDuce (http://www.cduce.org) that is included in all major
Linux distributions. The reference paper for the language was presented
at ICFP 2003.

Actually you can also try it with parametric polymorphism (reference
papers in POPL 2014 and POPL 2015 : Polymorphic functions with
set-theoretic types) but since polymorphism is not included in the
distribution, yet, you have to compile the alpha version available at
https://www.cduce.org/redmine/projects/cduce

Cheers

Beppe


P.S.
If you wonder about the advantages of using union and intersection types
with polymorphism here you are Okasaki' s implementation of red-black
trees balance and insert: thanks to intersection types you can
statically enforce that red-nodes have only black children (AFAIK you
need GADTs to do it in ML).

(* RedBlack tree *)
type RBtree('a) = Btree('a) | Rtree('a)

(* Black rooted RB tree: a leaf or a black node *)
type Btree('a) = [] | <black elem='a>[ RBtree('a) RBtree('a) ]

(* Red rooted RB tree: only black childs *)
type Rtree('a) = <red elem='a>[ Btree('a) Btree('a) ]

(* Wrongtree : a red tree with a red child *)
type Wrongtree('a) =    <red elem='a>( [ Rtree('a) Btree('a) ]
                                      | [ Btree('a) Rtree('a) ])

(* Unbalanced : a black node with a wrong tree child *)
type Unbalanced('a) = <black elem='a>( [ Wrongtree('a) RBtree('a) ]
                                      | [ RBtree('a) Wrongtree('a) ])
;;


(* Balance is a function that when applied to a unbalanced tree *)
(* it returns a red tree and when applied to something that is  *)
(* not unbalanced, it returns a result of the same type.           *)
(* balance : (Unbalanced('a) -> Rtree('a)) /\                   *)
(*           ('b\Unbalanced(Any) -> 'b\Unbalanced(Any))         *)

let balance ( Unbalanced('a) -> Rtree('a) ; 'b\Unbalanced(Any) -> 
'b\Unbalanced(Any) )
   | (<black (z)>[ <red (y)>[ <red (x)>[ a b ] c ] d ]
   | <black (z)>[ <red (x)>[ a <red (y)>[ b c ] ] d ]
   | <black (x)>[ a <red (z)>[ <red (y)>[ b c ] d ] ]
   | <black (x)>[ a <red (y)>[ b <red (z)>[ c d ] ] ]) & Unbalanced(Any) ->
         <red (y)>[ <black (x)>[ a b ] <black (z)>[ c d ] ]
   | x -> x
;;


(* insert: 'a -> Btree('a) -> Btree('a)\[]                      *)
(* it preserves the type and returns a non empty tree           *)

let insert (x : 'a) (t : Btree('a)) : Btree('a)\[] =
   let ins_aux ( [] -> Rtree('a);
                 Btree('a)\[] -> RBtree('a)\[];
                 Rtree('a) -> Rtree('a)|Wrongtree('a) )
     | [] -> <red elem=x>[ [] [] ]
     | (<(color) elem=y>[ a b ]) & z ->
            if x << y then balance <(color) elem=y>[ (ins_aux a) b ]
        else if x >> y then balance <(color) elem=y>[ a (ins_aux b) ]
        else z

(* if ins_aux is applied to a leaf it returns a red tree, to a  *)
(* black node it returns a non-empty RBtree, a red node it      *)
(* returns either a red tree of a wrongtree to be balanced.     *)

From uuomul at yahoo.com  Sat Jun 27 08:08:24 2015
From: uuomul at yahoo.com (Andrei Popescu)
Date: Sat, 27 Jun 2015 12:08:24 +0000 (UTC)
Subject: [TYPES] statistics about information-flow programming errors?
Message-ID: <590283973.815269.1435406904568.JavaMail.yahoo@mail.yahoo.com>

Dear TYPES forum, 


I am searching for studies about the size and impact of programming errors that lead to unintended information flow. I know of some famous leaks that made it to the news. However, I am more interested in statistics about everyday leaks from everyday programs. (I thought this list might be a good place for my question, given the traditional connection between information flow and type systems.) 
Many thanks in advance, 
 Andrei 

From davidfstr at gmail.com  Thu Sep 10 00:53:58 2015
From: davidfstr at gmail.com (David Foster)
Date: Wed, 09 Sep 2015 21:53:58 -0700
Subject: [TYPES] RFC: ARF - An interprocedural flow-based type checker
Message-ID: <55F10CE6.8020601@gmail.com>

I've written a small untyped language calculus (ARF) and an 
interprocedural flow-based type checker to explore techniques for 
efficiently inferring all types in the presence of recursive function 
calls, with no prior type declarations or annotations required in the 
original program.

* https://github.com/davidfstr/arf#assign-recurse-flow-arf

The type system I have is a flow-based type system, similar to that used 
by David Pearce's Whiley language[^1]. I have extended his approach with 
interprocedural analysis and full inference for all types, since I 
didn't want to require the programmer to insert any annotations in the 
original source code, which would be required by Pearce's original 
formulation.

The reason I developed ARF was to learn type checking techniques for my 
ultimate application: writing an optional static type checker for 
Python[^2] that can be superimposed over Python's runtime type system, 
which is more similar in flavor to flow-based type systems than other 
kinds of type systems such as Hindley-Milner. However it occurs to me 
that the ARF calculus and type checker may be interesting in its own right.

In particular ARF has very good type checking performance: O(m^2) time 
in the worst case and O(m) time in the average case, where m is the 
number of functions in the program. (These bounds are derived from 
informal reasoning and empirical timings from ARF's automated test suite.)

On the other hand, I may have just reinvented a type system that already 
exists somewhere in the academic literature, since I am not familiar 
enough with type-related terminology to effectively search the literature.

So I have two main questions for this list:

(1) Is it likely that the ARF calculus or type checking algorithm is 
novel in one or more respects, based on my descriptions of its 
properties and performance?

(2) Are there other related calculi or type checking algorithms from the 
literature?

Thank you for taking the time to read this.

-- 
David Foster
http://dafoster.net/about/

[^1]: David J Pearce. "Calculus for Constraint-Based Flow Typing". June 
2012.
[^2]: David L Foster. "Plint: An optional static type checker for 
Python". In development. <https://github.com/davidfstr/plint>

From gabriel.scherer at gmail.com  Thu Sep 10 04:48:33 2015
From: gabriel.scherer at gmail.com (Gabriel Scherer)
Date: Thu, 10 Sep 2015 10:48:33 +0200
Subject: [TYPES] RFC: ARF - An interprocedural flow-based type checker
In-Reply-To: <55F10CE6.8020601@gmail.com>
References: <55F10CE6.8020601@gmail.com>
Message-ID: <CAPFanBFnPsEO=-NDaVODp7SYUa2QmXkw2HOEF7MF+f98jUFdSQ@mail.gmail.com>

The assumption made in your note [^max-refinements-in-loop], namely
that there is a bounded number of types refining each other and that
you can thus always compute the fixpoint in finite time, will not hold
in richer type systems, if you have higher-order functions for example
(consider a recursive function that consumes infinitely many
arguments). Ultimately you may run into the well-known problem that
polymorphic recursion is not inferrable in absence of type
annotations.

I was not entirely satisfied with the complexity argument you provide.
You describe several different corner cases and their complexity
analysis, and assume that any program (can be decomposed in
subprograms that) will behave in a way similar to one of these corner
cases -- that they are effectively the worst cases in a formal sense.
However, this assumption that the corner cases cover all possible
programs is not clear to me.

I am far from an expert on this corner of the literature, but I think
you may be interested in the work on Flow Analysis that happened
approximately at the same time as the detailed study of polymorphic
recursion (in the nineties). In particular, the work of Christian
Mossin on flow analysis seems relevant. It was done in a typed setting
but, in "Higher-Order Value Flow Graphs" (1997) a dynamic type is
considered; it could be interesting to translate your language to his
system to compare your analyses.
(His formalism, in terms of a flow graph built out of programs, allows
for rigorous proofs of complexity in terms of the size characteristics
of the constructed graph.)

On Thu, Sep 10, 2015 at 6:53 AM, David Foster <davidfstr at gmail.com> wrote:
> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
>
> I've written a small untyped language calculus (ARF) and an interprocedural
> flow-based type checker to explore techniques for efficiently inferring all
> types in the presence of recursive function calls, with no prior type
> declarations or annotations required in the original program.
>
> * https://github.com/davidfstr/arf#assign-recurse-flow-arf
>
> The type system I have is a flow-based type system, similar to that used by
> David Pearce's Whiley language[^1]. I have extended his approach with
> interprocedural analysis and full inference for all types, since I didn't
> want to require the programmer to insert any annotations in the original
> source code, which would be required by Pearce's original formulation.
>
> The reason I developed ARF was to learn type checking techniques for my
> ultimate application: writing an optional static type checker for Python[^2]
> that can be superimposed over Python's runtime type system, which is more
> similar in flavor to flow-based type systems than other kinds of type
> systems such as Hindley-Milner. However it occurs to me that the ARF
> calculus and type checker may be interesting in its own right.
>
> In particular ARF has very good type checking performance: O(m^2) time in
> the worst case and O(m) time in the average case, where m is the number of
> functions in the program. (These bounds are derived from informal reasoning
> and empirical timings from ARF's automated test suite.)
>
> On the other hand, I may have just reinvented a type system that already
> exists somewhere in the academic literature, since I am not familiar enough
> with type-related terminology to effectively search the literature.
>
> So I have two main questions for this list:
>
> (1) Is it likely that the ARF calculus or type checking algorithm is novel
> in one or more respects, based on my descriptions of its properties and
> performance?
>
> (2) Are there other related calculi or type checking algorithms from the
> literature?
>
> Thank you for taking the time to read this.
>
> --
> David Foster
> http://dafoster.net/about/
>
> [^1]: David J Pearce. "Calculus for Constraint-Based Flow Typing". June
> 2012.
> [^2]: David L Foster. "Plint: An optional static type checker for Python".
> In development. <https://github.com/davidfstr/plint>

From Francois.Pottier at inria.fr  Thu Sep 10 06:52:15 2015
From: Francois.Pottier at inria.fr (Francois Pottier)
Date: Thu, 10 Sep 2015 12:52:15 +0200
Subject: [TYPES] RFC: ARF - An interprocedural flow-based type checker
In-Reply-To: <CAPFanBFnPsEO=-NDaVODp7SYUa2QmXkw2HOEF7MF+f98jUFdSQ@mail.gmail.com>
References: <55F10CE6.8020601@gmail.com>
 <CAPFanBFnPsEO=-NDaVODp7SYUa2QmXkw2HOEF7MF+f98jUFdSQ@mail.gmail.com>
Message-ID: <20150910105215.GA23293@yquem.inria.fr>


Hello,

On Thu, Sep 10, 2015 at 10:48:33AM +0200, Gabriel Scherer wrote:
> In particular, the work of Christian Mossin on flow analysis seems
> relevant. It was done in a typed setting but, in "Higher-Order Value Flow
> Graphs" (1997) a dynamic type is considered; it could be interesting to
> translate your language to his system to compare your analyses.

It may be worth noting that the paper "Constraint Abstractions" by
J. Gustavsson and J. Svenningsson offers a pleasant, constraint-based view of
flow analysis and a significant improvement in complexity compared with
Mossin's algorithm.

  http://www.cse.chalmers.se/~josefs/publications/ca.pdf

-- 
Fran?ois Pottier
Francois.Pottier at inria.fr
http://gallium.inria.fr/~fpottier/

From hgualandi at inf.puc-rio.br  Thu Sep 10 11:41:12 2015
From: hgualandi at inf.puc-rio.br (hgualandi at inf.puc-rio.br)
Date: Thu, 10 Sep 2015 12:41:12 -0300 (BRT)
Subject: [TYPES] RFC: ARF - An interprocedural flow-based type checker
In-Reply-To: <55F10CE6.8020601@gmail.com>
References: <55F10CE6.8020601@gmail.com>
Message-ID: <40780.189.122.122.184.1441899672.squirrel@webmail.inf.puc-rio.br>

> On the other hand, I may have just reinvented a type system that already
> exists somewhere in the academic literature, since I am not familiar
> enough with type-related terminology to effectively search the literature.

I am not familiar with the Whiley language and with the references that
Gabriel and Fran?ois provided but I am familiar with some of the
literature on type inference for dynamically typed languages. So here
comes a bit of a brain dump of things from my masters...


On a cursory glance, the types you infer for Python are unions of base
types. This reminds me of the Soft Typing work for Scheme, from the 90s.
Soft typing systems are based on global type inference (the user doesn't
add any type annotations) and use the result of the type inference is a
classification of the primitive operations in the program based on how
safe they are at runtime. For example, in an addition `x + y` if it can
deduce that x and y are numbers, then the addition is certainly safe. If x
and y are always None, then the addition is certainly unsafe and if x and
y can be either a number or None, then the safety of the addition is
uncertain and can only be checked at runtime. One of the interesting
features of soft typing systems is that by classifying operations this way
the output in case of a type error is more informative than just saying "I
failed to typecheck your program because some types didn't match".

The first Soft Typing systems for scheme [1][2][3] were based on HM type
inference with row-polymorphism. Later systems, like MrSpidey for PLT
Scheme [4][5] moved to flow-based analysis, which is more accurate. The
cost is that flow-analysis has to look at the whole program while HM
inference can check modules separately. Inferring
parametrically-polymorphic types using flow analysis is also trickier to
do efficiently[7].

Anyway, it might be interesting for you to dig up an old version of
DrScheme that comes bundled with MrSpidey so you can play a bit with it.

(disconnected brain dump: [3] has a very comprehensive section on the
downsides of using HM inference for typechecking. [6] frames flow analysis
as a more traditional type system and [7] is a very deep survey on
flow-analysis.)

One thing that  you should be aware of is that global type inference is
very brittle, which is partly a reason why people have been moving on to
Optional Typing and Gradual Typing for dynamic languages lately [8]. My
impression is that the niche for global type inference has been automated
program analysis that does not expect any interaction from the programmer.
You see these sometimes inside compilers for dynamic languages (which use
the inference to omit tag checks and things like that) but one notable
example of a global type inference system that is programmer facing is the
Dialyzer tool for Erlang.

Dialyzer is a soft type system that silences warnings for "potentially
unsafe" operations and only complains about things that it is 100% sure
that are wrong. The authors call this a  "success type system" [9], which
instead of focusing on proving that some programs don't go wrong, focuses
on proving that some programs do go wrong. As a result of this more lax
typechecking, Dialyzer can have more efficient inference (if one of its
inferred types ever grows too big it can "give up" and infer the "any"
type instead) and the error messages it reports are almost certainly going
to be bugs (and not just some imprecision in the type checker), which is
nice for their use case of running a linter mature code bases with
thousands of lines of code.

Summing up, I hopefully what I wrote has to do with what you are looking for.

Hugo

----------


[1]
Cartwright, R. & Fagan, M.
Soft Typing Proceedings of the ACM SIGPLAN 1991 Conference on Programming
Language Design and Implementation, ACM, 1991

[2]
Fagan, M.
Soft Typing: an approach to type checking for dynamically typed languages
Rice University, 1991
www.ccs.neu.edu/scheme/pubs/thesis-fagan.ps.gz

[3]
Wright, A. K. & Cartwright, R. A Practical Soft Type System for Scheme
Transactions on Programming Languages and Systems, ACM, 1997

[4]
Flanagan, C.; Flatt, M.; Krishnamurthi, S.; Weirich, S. & Felleisen, M.
Catching bugs in the web of program invariants Proceedings of the ACM
SIGPLAN 1996 Conference on Programming Language Design and Implementation,
Association for Computing Machinery (ACM), 1996
http://cs.brown.edu/~sk/Publications/Papers/Published/ffkwf-mrspidey/

[5]
Flanagan, Cormac
Effective Static Debugging via Componential Set-Based Analysis Rice
University, 1997
https://users.soe.ucsc.edu/~cormac/papers/thesis.pdf

[6]
Palsberg, J. & Schwartzbach, M. I.
Safety Analysis Versus Type Inference for Partial Types Information
Processing Letters, Elsevier North-Holland, Inc., 1992
http://www.cs.ucla.edu/~palsberg/paper/ipl92.pdf

[7]
Midtgaard, J. Control-Flow Analysis of Functional Programs University of
Aarhus, 2007
http://www.brics.dk/RS/07/18/index.html

[8]
Felleisen, M. From Soft Scheme to Typed Scheme: Experiences from 20 Years
of Script Evolution, and Some Ideas on What Works 2009
http://www.ccs.neu.edu/home/matthias/Presentations/stop.html

[9]
Lindahl, T. & Sagonas, K.
Practical type inference based on success typings Proceedings of the 8th
ACM SIGPLAN International Conference on Principles and Practice of
Declarative Programming, Association for Computing Machinery (ACM), 2006
http://it.uu.se/research/group/hipe/papers/succ_types.pdf

From davidfstr at gmail.com  Fri Sep 11 00:55:53 2015
From: davidfstr at gmail.com (David Foster)
Date: Thu, 10 Sep 2015 21:55:53 -0700
Subject: [TYPES] RFC: ARF - An interprocedural flow-based type checker
In-Reply-To: <40780.189.122.122.184.1441899672.squirrel@webmail.inf.puc-rio.br>
References: <55F10CE6.8020601@gmail.com>
 <40780.189.122.122.184.1441899672.squirrel@webmail.inf.puc-rio.br>
Message-ID: <55F25ED9.70306@gmail.com>

On 9/10/15, 1:48 AM, Gabriel Scherer wrote:
 > I was not entirely satisfied with the complexity argument you provide.
 > [...]
 > However, this assumption that the corner cases cover all possible
 > programs is not clear to me.

Indeed. This initial analysis is just a first approximation.

 > In particular, the work of Christian Mossin on flow analysis seems 
relevant.

Thanks! I will take a look.


On 9/10/15, 3:52 AM, Francois Pottier wrote:
 > It may be worth noting that the paper "Constraint Abstractions" by
 > J. Gustavsson and J. Svenningsson offers a pleasant, constraint-based 
view of
 > flow analysis and a significant improvement in complexity compared with
 > Mossin's algorithm.

Thanks! I will also take a look.


On 9/10/15, 8:41 AM, hgualandi at inf.puc-rio.br wrote:
> I am not familiar with the Whiley language and with the references that
> Gabriel and Fran?ois provided but I am familiar with some of the
> literature on type inference for dynamically typed languages. So here
> comes a bit of a brain dump of things from my masters...

Thank you Hugo. These references are extremely useful.

 > On a cursory glance, the types you infer for Python are unions of base
 > types. This reminds me of the Soft Typing work for Scheme, from the 90s.

Indeed: If you have "if { x = <int> } else { x = <bool> }; return x;", 
the return type will be inferred as int|bool.

 > One of the interesting
 > features of soft typing systems is that by classifying operations 
this way
 > the output in case of a type error is more informative than just 
saying "I
 > failed to typecheck your program because some types didn't match".

That is encouraging to hear. Having extremely clear error messages from 
the type checker is a very high priority for the larger type checker I'm 
designing. (It's item #3 in the mission statement.)

 > One thing that  you should be aware of is that global type inference is
 > very brittle, which is partly a reason why people have been moving on to
 > Optional Typing and Gradual Typing for dynamic languages lately [8].

By brittle do you mean that small changes in the program source text can 
easily cause large parts of the program to type differently? Or some 
other property?

From simone.martini at unibo.it  Wed Oct 14 05:26:31 2015
From: simone.martini at unibo.it (Simone Martini)
Date: Wed, 14 Oct 2015 09:26:31 +0000
Subject: [TYPES] When types appeared in programming languages
Message-ID: <60E836D1-4632-4B29-A565-CCDB93280F0F@unibo.it>

Last year, there has been a thread on this mailing list on the role (and concept) of types in programming languages, started by this msg of Vladimir Voevodsky:
	http://lists.seas.upenn.edu/pipermail/types-list/2014/001745.html

Stimulated from that thread (which showed that there was little consensus on when types appeared, and with which meaning), I wrote a little essay, suggesting that the emergence of the concept of type in computer science is relatively independent from the logical tradition, until the Curry-Howard isomorphism will make an explicit bridge between them.

I presented the paper last week at History and Philosophy of Computing 2015, in Pisa. 

	http://arxiv.org/abs/1510.03726

Comments, remarks, and especially critiques would be much welcomed from the members of this list.

Best,
-s.
---------------------------------------------------
Simone Martini                          
Universita' di Bologna                 
Dip. di Informatica - Scienza e Ingegneria
Italy

www.cs.unibo.it/~martini

From patrick.browne at dit.ie  Fri Oct 16 07:48:16 2015
From: patrick.browne at dit.ie (PATRICK BROWNE)
Date: Fri, 16 Oct 2015 12:48:16 +0100
Subject: [TYPES] Fwd:  When types appeared in programming languages
In-Reply-To: <CAGFLrKdG7=pbmrzAdTy0AHs0Cab_HuiD0RmCjx-jCvSsHQe55w@mail.gmail.com>
References: <60E836D1-4632-4B29-A565-CCDB93280F0F@unibo.it>
 <CAGFLrKdG7=pbmrzAdTy0AHs0Cab_HuiD0RmCjx-jCvSsHQe55w@mail.gmail.com>
Message-ID: <CAGFLrKeivs=kScDRTw+Q-PpQ4Z-d5rpFLN1UfrHfLT9kkBdwTA@mail.gmail.com>

Simone,
I enjoyed your review of types. Have you looked at Joseph Goguen's paper
Type as Theories[1].
He presents three descriptions of types: 1)as sets, 2)as algebras, 3)as
theories.
I believe that algebraic languages like CafeOBJ and Maude support all three
approach to types.
Types as sets: Using *sorts*, which can be arrange in a lattice of sorts.
Types as algebras: Tight modules with carrier set, and concrete operations
using initial semantics
Types as theories: Loose modules representing theories with axioms stating
properties e.g. partial order, monoid.
                   Types are logical theories, presented by axioms, whose
properties can be explored by logical deduction.
Regards,
Pat
[1]
http://www.google.ie/url?sa=t&rct=j&q=&esrc=s&source=web&cd=4&cad=rja&uact=8&ved=0CDQQFjADahUKEwib3eGM1MbIAhXC6xQKHcsLA4A&url=http%3A%2F%2Fciteseerx.ist.psu.edu%2Fviewdoc%2Fdownload%3Fdoi%3D10.1.1.16.2241%26rep%3Drep1%26type%3Dps&usg=AFQjCNGjxJGhAumTd7mV0iNovz3eKUco3g&bvm=bv.105039540,d.d24

On 14 October 2015 at 10:26, Simone Martini <simone.martini at unibo.it> wrote:

> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list
> ]
>
> Last year, there has been a thread on this mailing list on the role (and
> concept) of types in programming languages, started by this msg of Vladimir
> Voevodsky:
>         http://lists.seas.upenn.edu/pipermail/types-list/2014/001745.html
>
> Stimulated from that thread (which showed that there was little consensus
> on when types appeared, and with which meaning), I wrote a little essay,
> suggesting that the emergence of the concept of type in computer science is
> relatively independent from the logical tradition, until the Curry-Howard
> isomorphism will make an explicit bridge between them.
>
> I presented the paper last week at History and Philosophy of Computing
> 2015, in Pisa.
>
>         http://arxiv.org/abs/1510.03726
>
> Comments, remarks, and especially critiques would be much welcomed from
> the members of this list.
>
> Best,
> -s.
> ---------------------------------------------------
> Simone Martini
> Universita' di Bologna
> Dip. di Informatica - Scienza e Ingegneria
> Italy
>
> www.cs.unibo.it/~martini
>

-- 


This email originated from DIT. If you received this email in error, please 
delete it from your system. Please note that if you are not the named 
addressee, disclosing, copying, distributing or taking any action based on 
the contents of this email or attachments is prohibited. www.dit.ie

Is ? ITB?C a th?inig an r?omhphost seo. M? fuair t? an r?omhphost seo tr? 
earr?id, scrios de do ch?ras ? le do thoil. Tabhair ar aird, mura t? an 
seola? ainmnithe, go bhfuil dianchosc ar aon nochtadh, aon ch?ipe?il, aon 
d?ileadh n? ar aon ghn?omh a dh?anfar bunaithe ar an ?bhar at? sa 
r?omhphost n? sna hiat?in seo. www.dit.ie

T? ITB?C ag aistri? go Gr?inseach Ghorm?in ? DIT is on the move to 
Grangegorman <http://www.dit.ie/grangegorman>

From simone.martini at unibo.it  Sun Oct 18 06:39:40 2015
From: simone.martini at unibo.it (Simone Martini)
Date: Sun, 18 Oct 2015 10:39:40 +0000
Subject: [TYPES] When types appeared in programming languages
In-Reply-To: <CAGFLrKeivs=kScDRTw+Q-PpQ4Z-d5rpFLN1UfrHfLT9kkBdwTA@mail.gmail.com>
References: <60E836D1-4632-4B29-A565-CCDB93280F0F@unibo.it>
 <CAGFLrKdG7=pbmrzAdTy0AHs0Cab_HuiD0RmCjx-jCvSsHQe55w@mail.gmail.com>
 <CAGFLrKeivs=kScDRTw+Q-PpQ4Z-d5rpFLN1UfrHfLT9kkBdwTA@mail.gmail.com>
Message-ID: <304BEB76-487A-4C77-9917-0163A710D6B5@unibo.it>

Dear Patrick,

Joe Goguen?s paper is a fine piece of work, which observes and classifies the use (and role) of types in PL from a semantical perspective (types as ?sets?, as ?algebras? and ?theories?).

Once could be tempted to say that these three ?types? correspond to what I call the "technical concept?, the "general abstraction mechanism? and the types from mathematical logic. 
But I believe this would be a post festam reconstruction. 
Until the turn from the ?60s to the ?70s (and thus papers by Goguen, Hoare, and of course Liskov) there are no real ?types as algebras? around. 

Of course, the ?types as theories? are the ?types of logic? (at least one particular way to understand them), independent from the Curry-Howard isomorphism, but they arrive on the scene in the 80s? 

Best regards and thank you for sharing with us your observations.

-s.




> On 16 Oct 2015, at 13:48, PATRICK BROWNE <patrick.browne at dit.ie> wrote:
> 
> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
> 
> Simone,
> I enjoyed your review of types. Have you looked at Joseph Goguen's paper
> Type as Theories[1].
> He presents three descriptions of types: 1)as sets, 2)as algebras, 3)as
> theories.
> I believe that algebraic languages like CafeOBJ and Maude support all three
> approach to types.
> Types as sets: Using *sorts*, which can be arrange in a lattice of sorts.
> Types as algebras: Tight modules with carrier set, and concrete operations
> using initial semantics
> Types as theories: Loose modules representing theories with axioms stating
> properties e.g. partial order, monoid.
>                   Types are logical theories, presented by axioms, whose
> properties can be explored by logical deduction.
> Regards,
> Pat
> [1]
> http://www.google.ie/url?sa=t&rct=j&q=&esrc=s&source=web&cd=4&cad=rja&uact=8&ved=0CDQQFjADahUKEwib3eGM1MbIAhXC6xQKHcsLA4A&url=http%3A%2F%2Fciteseerx.ist.psu.edu%2Fviewdoc%2Fdownload%3Fdoi%3D10.1.1.16.2241%26rep%3Drep1%26type%3Dps&usg=AFQjCNGjxJGhAumTd7mV0iNovz3eKUco3g&bvm=bv.105039540,d.d24
> 
> On 14 October 2015 at 10:26, Simone Martini <simone.martini at unibo.it> wrote:
> 
>> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list
>> ]
>> 
>> Last year, there has been a thread on this mailing list on the role (and
>> concept) of types in programming languages, started by this msg of Vladimir
>> Voevodsky:
>>        http://lists.seas.upenn.edu/pipermail/types-list/2014/001745.html
>> 
>> Stimulated from that thread (which showed that there was little consensus
>> on when types appeared, and with which meaning), I wrote a little essay,
>> suggesting that the emergence of the concept of type in computer science is
>> relatively independent from the logical tradition, until the Curry-Howard
>> isomorphism will make an explicit bridge between them.
>> 
>> I presented the paper last week at History and Philosophy of Computing
>> 2015, in Pisa.
>> 
>>        http://arxiv.org/abs/1510.03726
>> 
>> Comments, remarks, and especially critiques would be much welcomed from
>> the members of this list.
>> 
>> Best,
>> -s.
>> ---------------------------------------------------
>> Simone Martini
>> Universita' di Bologna
>> Dip. di Informatica - Scienza e Ingegneria
>> Italy
>> 
>> www.cs.unibo.it/~martini
>> 
> 
> -- 
> 
> 
> This email originated from DIT. If you received this email in error, please 
> delete it from your system. Please note that if you are not the named 
> addressee, disclosing, copying, distributing or taking any action based on 
> the contents of this email or attachments is prohibited. www.dit.ie
> 
> Is ? ITB?C a th?inig an r?omhphost seo. M? fuair t? an r?omhphost seo tr? 
> earr?id, scrios de do ch?ras ? le do thoil. Tabhair ar aird, mura t? an 
> seola? ainmnithe, go bhfuil dianchosc ar aon nochtadh, aon ch?ipe?il, aon 
> d?ileadh n? ar aon ghn?omh a dh?anfar bunaithe ar an ?bhar at? sa 
> r?omhphost n? sna hiat?in seo. www.dit.ie
> 
> T? ITB?C ag aistri? go Gr?inseach Ghorm?in ? DIT is on the move to 
> Grangegorman <http://www.dit.ie/grangegorman>


From a.g.setzer at swansea.ac.uk  Fri Dec 18 20:57:21 2015
From: a.g.setzer at swansea.ac.uk (Anton Setzer)
Date: Sat, 19 Dec 2015 01:57:21 +0000
Subject: [TYPES] Postdoc positions and lectureships in Swansea (suitable for
 type theoretists; deadlines 22/12/15 and 5/1/16)
Message-ID: <5674B981.4060604@swansea.ac.uk>

Dear type theoretists,

In Swansea we have 2 lectureships (closing date very soon: 22/12/15) and 
10 three year postdoc
positions available (deadline for expression of interest 5/1/16)
I would be very keen on getting people related to my research area which 
includes type theory.


Details are as follows:

* Up to 2 permanent Lectureships in Computer Security. While the 
lectureships aim at Computer Security in general,
this might be an opportunity for researchers working on applications of 
Logic in Computer Security.

http://www.swansea.ac.uk/personnel/jobs/details.php?nPostingID=2756&nPostingTargetID=4869&option=52&sort=DESC&respnr=1&ID=QHUFK026203F3VBQB7VLO8NXD&JOBADLG=UK&Resultsperpage=20&lg=UK&mask=suext 


http://www.swansea.ac.uk/compsci/


* 10 three-years postdoctoral fellowships across a wide range of science 
and technology disciplines. The Theoretical Computer Science Group 
offers projects in Computability, Specification, Proof Theory, 
Complexity and Verification. See our research portfolio at

http://www.swansea.ac.uk/compsci/researchandimpact/researchgroups/theory/

important restrictions on candidates for the postdoc positions (full 
details are below)

* 3 - 5 years post PhD
* not been resident in the UK for more than 12 months in last three years
* Fellowships will normally be 3 years in length
* can involve collaboration with a relevant commercial partner.
* 
http://expertisewales.com/marie-sk%C5%82odowska-curie-actions-cofund-fellowship-scheme 


Please contact members of our group directly if you are interest in a 
particular topic.

Deadline for Expression of Interest: 5 January 2016
Full Application: 1 March 2016

Further details about the fellowships, including eligibility criteria, 
are below.

SWANSEA UNIVERSITY EXCITING FELLOWSHIP OPPORTUNITIES

Strengthening International Research Capacity in Wales (SIRCIW) 
Fellowships hosted by Swansea University Swansea University?s, College 
of Science, is delighted to announce 10 SIRCIW postdoctoral fellowships 
across a wide range of science and technology disciplines to the highest 
calibre candidates.

The SIRCIW fellowship scheme, part of the Chief Scientific Adviser for 
Wales? strategy to increase research capacity in Wales, will enable 
talented ?rising star? researchers, with a minimum 3 to 5 years 
post-doctoral research experience, to:-

  * Work with leading international scholars in Swansea?s, College of 
Science;
  * Receive excellent research supervision;
  * Have access to the latest facilities and resources, and involvement 
in world-leading joint research projects;
  * Collaborate with commercial partner where appropriate;
  * Spend time as an academic in Wales, linking up with extensive 
international networks and collaborations.

These prestigious 3 year fellowships are jointly funded by Swansea 
University, the European Commission - H2020, Marie Sklodowska Curie 
Action COFUND award and the Welsh Government.

Through SIRCIW, Swansea is seeking to attract talented experienced 
researchers with the potential to be research leaders of the future.  It 
is anticipated fellowships will start in autumn 2016.

FELLOW ELIGIBILITY CRITERIA

  * Researchers may be of Any Nationality
  * Cannot have been resident in the UK for more than 12 months in the 
last three years
  * Submit a Science and/ or Technology relevant joint fellowship 
application with Swansea University to the Chief Scientific Adviser for 
Wales Office.

APPLICATION PROCESS

2 stage process, to be completed in English:

1. Expression of Interest, EoI, submitted to the Deapartment of Computer 
Science, Swansea University by Tuesday 5th January
2. Full Application (supervisor form, ethics form, and CV) submitted to 
CSAW office by Tuesday 1st March 2016.

Interested applicants are encouraged to make early contact with a 
potential Department of Computer Science Supervisor.  To initiate 
informal discussions please forward:-

  * Recent successful research proposal
  * Current C.V. & Research/ career history
  * Proposed Research Topic Area
  * Likely Impact
  * Referee Details

FURTHER INFORMATION:

Department of Computer Science, Swansea University
http://www.swansea.ac.uk/compsci/
College of Science, Swansea University
http://www.swansea.ac.uk/science/
SIRCIW fellowship scheme can be found at
http://expertisewales.com/support-and-funding-researchers