headers
Stefan Holdermans | 7 Nov 2008 09:24
Picon

Minimal type reconstruction

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

Hi all,

One way to look at type inference in Hindley-Milner-like disciplines  
is not just as the problem of finding a principal type scheme for a  
term in a given type environment, but as the problem of reconstructing  
an explicitly typed term in the style of System F that corresponds to  
such a principal type scheme. As an obvious example, consider the  
"completion" of the implicitly typed polymorphic identity function

	λx. x ,

resulting in the explicitly typed

	Λα. λx : α. x .

Typically, type inference for Hindley-Milner-like systems proceeds by  
assigning each let-bound variable its principal type. For example,  
completion of

	let id = λx. x in  id 2 + id 3 ni

yields

	let id = Λα. λx : α. x in id [ℕ] 2 + id [ℕ] 3 ni .

However, in this particular example the type abstraction in the  
definition of id and, hence, the type applications in the body of the  
local definition are unnecessary; another perfectly valid completion
(Continue reading)

Permalink | Reply | 4 comments |
headers
Josef Svenningsson | 7 Nov 2008 16:06
Picon
Picon

Re: Minimal type reconstruction

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

See:
 Minimal typing derivations
Nikolaj Skallerud Bjørner
http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.31.9102

Josef

On Fri, Nov 7, 2008 at 9:24 AM, Stefan Holdermans <stefan <at> cs.uu.nl> wrote:
> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
>
> Hi all,
>
> One way to look at type inference in Hindley-Milner-like disciplines
> is not just as the problem of finding a principal type scheme for a
> term in a given type environment, but as the problem of reconstructing
> an explicitly typed term in the style of System F that corresponds to
> such a principal type scheme. As an obvious example, consider the
> "completion" of the implicitly typed polymorphic identity function
>
>        λx. x ,
>
> resulting in the explicitly typed
>
>        Λα. λx : α. x .
>
> Typically, type inference for Hindley-Milner-like systems proceeds by
> assigning each let-bound variable its principal type. For example,
> completion of
(Continue reading)

Permalink | Reply | 0 comments |
headers
Andrew Kennedy | 7 Nov 2008 16:06
Picon
Favicon

Re: Minimal type reconstruction

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

Hi Stefan

I think that

"Minimal Typing Derivations", N Bjorner, ACM Workshop on ML and its Applications, 1994

is probably what you're after. (Should be on citeseer but I don't seem to get access right now).

Cheers
Andrew.

-----Original Message-----
From: types-list-bounces <at> lists.seas.upenn.edu
[mailto:types-list-bounces <at> lists.seas.upenn.edu] On Behalf Of Stefan Holdermans
Sent: 07 November 2008 08:24
To: types-list <at> lists.seas.upenn.edu
Subject: [TYPES] Minimal type reconstruction

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

Hi all,

One way to look at type inference in Hindley-Milner-like disciplines
is not just as the problem of finding a principal type scheme for a
term in a given type environment, but as the problem of reconstructing
an explicitly typed term in the style of System F that corresponds to
such a principal type scheme. As an obvious example, consider the
"completion" of the implicitly typed polymorphic identity function
(Continue reading)

Permalink | Reply | 1 comment |
headers
Didier Remy | 7 Nov 2008 16:30
Picon
Picon
Favicon

Re: Minimal type reconstruction

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

> That is, if a let-bound variable is not used polymorphically, we may  
> just as well infer a monomorphic type for it. In some specific  
> situations, such a "minimal" completion may even be preferable over a  
> fully polymorphic one. (Looking through a Curry-Howard lens, we are  
> after the "simplest" proofs.) Although I'm quite sure it has been  
> considered before, I have not found any discussion in literature of  
> the problem of finding minimal completions. Can anyone on this list  
> provide me with pointers to such discussions?

Dear Stefan,

I think that this is exactly the problem studied by Nikolaj Bjorner in the
case of ML in his paper "Minimal Typing Deriviations" presented at the ML
workshop in 1994 [http://theory.stanford.edu/people/nikolaj/ml-work94.ps]

Best wishes,

         Didier
Permalink | Reply | 0 comments |
headers
Gavin Bierman | 7 Nov 2008 16:35
Picon
Favicon

Re: Minimal type reconstruction

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

http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.31.9102


Gavin

-----Original Message-----
From: types-list-bounces <at> lists.seas.upenn.edu
[mailto:types-list-bounces <at> lists.seas.upenn.edu] On Behalf Of Andrew Kennedy
Sent: 07 November 2008 15:07
To: 'Stefan Holdermans'; types-list <at> lists.seas.upenn.edu
Subject: Re: [TYPES] Minimal type reconstruction

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

Hi Stefan

I think that

"Minimal Typing Derivations", N Bjorner, ACM Workshop on ML and its Applications, 1994

is probably what you're after. (Should be on citeseer but I don't seem to get access right now).

Cheers
Andrew.

-----Original Message-----
From: types-list-bounces <at> lists.seas.upenn.edu
[mailto:types-list-bounces <at> lists.seas.upenn.edu] On Behalf Of Stefan Holdermans
Sent: 07 November 2008 08:24
(Continue reading)

Permalink | Reply | 0 comments |
headers
Stefano Berardi | 12 Nov 2008 12:07
Picon
Favicon

[TYPES/announce] WORKSHOP "STRUCTURAL PROOF THEORY" November 19-21 2008 PARIS

[ The Types Forum (announcements only), 
     http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

   WORKSHOP "STRUCTURAL PROOF THEORY"
           November 19-21 2008
   175, rue Chevaleret, 75013 PARIS, France

  This workshop is devoted to structural proof theory questions, from
  the design of deduction systems for various logics (classical,
  intuitionistic, modal, etc.), to the computational interpretations of
  proofs through cut-elimination, proof-search, proof complexity. There
  will be 4 invited talks and the rest of the program will consist of
  contributed talks and discussions.

  The workshop is open to everyone interested. All proposals of
  contributed talks are welcome, including works in progress and
  discussions of open problems.

  If you intend to give a talk or simply participate, please let us know
  by sending an email to parigot [at] pps [dot] jussieu [dot] fr.

  For more informations see http://www.pps.jussieu.fr/~parigot/SPT-2008.html

  The previous workshop of this kind was a small workshop of the research
  project Types, many topics of the workshop are related to Type Theory 
and many
  participant are members of Types.
Permalink | Reply | 0 comments |
headers
Stefan Holdermans | 8 Nov 2008 09:47
Picon

Re: Minimal type reconstruction

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

Josef, Andrew, Didier, Gavin, and Christian,

I asked:

> I have not found any discussion in literature of  the problem of  
> finding minimal completions. Can anyone on this list  provide me  
> with pointers to such discussions?

Thank you so much for your very helpful answers; I will look into the  
papers you mentioned.

Cheers,

   Stefan
Permalink | Reply | 0 comments |
headers
Andrei Popescu | 12 Nov 2008 20:26
Picon
Favicon

HOAS versus meta reasoning

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

Dear Type Theorists and Practioners, 

I would like to know what is the state of the art in taming the interaction between HOAS (higher order
abstract syntax) and meta-reasoning/inductive reasoning/recursive definitions.  (I am aware of some
of the work, but very probably I am not aware of the latest progress.)  

Thank you in advance, 
   Andrei Popescu
Permalink | Reply | 7 comments |
headers
Andrew Gacek | 12 Nov 2008 22:36
Picon
Gravatar

Re: HOAS versus meta reasoning

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

Hi Andrei,

There has been research on this topic for over a decade, begun by Dale
Miller and Ray McDowell (who picked up on earlier work by Peter
Schroeder-Heister and Girard), continued by Alwen Tiu and Dale Miller
and now including several others like David Baelde, Gopalan Nadathur
and myself. There is also a system called Abella
(http://abella.cs.umn.edu) that incorporates this style of reasoning.
Some of the highlights of this research are:

 * Reasoning with higher-order abstract syntax in a logical framework,
by Raymond McDowell and Dale Miller (ToCL 2002). In this paper
McDowell and Miller present a logic with HOAS, recursive definitions,
and natural number induction. Using this logic they are able to prove
various theorems such as subject reduction for the lambda calculus,
but in each theorem when they use the inductive hypothesis, they do so
on closed HOAS terms. The reason is that they have trouble encoding
the free variables in a logical way.

* A proof theory for generic judgments, by Dale Miller and Alwen Tiu
(LICS 2005), and A logical framework for reasoning about logical
specifications, by Alwen Tiu (PhD 2004). In the first paper Miller and
Tiu introduce a new logical quantifier called nabla which allows them
to overcome the previous issue with encoding free variables. In
particular, they are able to elegantly encode many notions from the
pi-calculus. The second work is Tiu's PhD thesis in which he adds a
notion of induction and coinduction on recursive definitions to the
logic.
(Continue reading)

Permalink | Reply | 0 comments |
headers
Karl Crary | 12 Nov 2008 23:43
Picon
Favicon

Re: HOAS versus meta reasoning

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

The Twelf wiki (twelf.plparty.org) has a lot of material on how to do 
things with higher-order representations.  What specifically are you 
looking to tame? 

    -- Karl Crary

Andrei Popescu wrote:
> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
>
> Dear Type Theorists and Practioners, 
>
> I would like to know what is the state of the art in taming the interaction between HOAS (higher order
abstract syntax) and meta-reasoning/inductive reasoning/recursive definitions.  (I am aware of some
of the work, but very probably I am not aware of the latest progress.)  
>
> Thank you in advance, 
>    Andrei Popescu  
>
>  
>
>
>       
>
>
Permalink | Reply | 0 comments |

Gmane