The Coq mailing list

[Andreas Abel <andreas.abel AT ifi.lmu.de>]

Hi Thorsten,

sorry I did not see your answer right away...

On 11/24/11 4:42 PM, Altenkirch Thorsten wrote:
> In a predicative setting:
> Uniform datatypes can be reduced to W-types (in an extensional setting).
>
> However, it is not clear wether we can do this for non-uniform datatypes.
> (Actually I think we can't).
>
> If this is true then do non-uniform datatypes extend the strength of the
> system?

I think so.

In my paper

  Semi-continuous Sized Types and Termination
  Logical Methods in Computer Science, Volume 4, Issue 2, Paper 3. 
CSL'06 special issue.

  http://www2.tcs.ifi.lmu.de/~abel/publications.html#lmcs07

in Example 3.1 I explain how to encode an infinite sequence of number 
classes into one non-uniform data type:

  NCn = µ Fn          , where
  F0 X   = 1              and
  Fn+1 X = Fn X + (µFn → X ).

So basically, the n+1st number class is a tree branching over the nth 
number class.

You can turn that into one nested data type:

  µλY λF. 1 + (µF → Y (λX. F X + (µF → X ))).

Herein,

  F : * -> *
  Y : (* -> *) -> *

Does this make sense?

Cheers,
Andreas

> And is there a universal type like W covering non-uniform operators?
>
> Thorsten
>
> On 24/11/2011 08:55, "Andreas 
> Abel"<andreas.abel AT ifi.lmu.de>
>   wrote:
>
> > If you want some literature on this, I can advertise the paper by Ralph
> > and myself:
> >
> > Fixed Points of Type Constructors and Primitive Recursion
> > Andreas Abel and Ralph Matthes
> > Computer Science Logic, 18th International Workshop, CSL 2004, 13th
> > Annual Conference of the EACSL
> > Karpacz, Poland, September 2004. LNCS 3210,  Springer.
> >
> > http://www2.tcs.ifi.lmu.de/~abel/publications.html#csl04
> >
> > It is about Fomega, no dependencies, but the principles stay the same
> > for CC.
> >
> > Cheers,
> > Andreas
> >
> > On 21.11.11 2:36 AM, Peter LeFanu Lumsdaine wrote:
> > > > > On Wed, 16 Nov 2011, Bruno Barras wrote:
> > > > >
> > > > > > Putting what Matthieu already said with my own words:
> > > > > > non-uniform parameters behave
> > > > > > (1) like normal indices w.r.t. recursive schemes
> > > > > > (2) like parameters w.r.t. dependent pattern-matching (check out
> > > > > > list'_case)
> > >
> > > Many thanks to those who replied both on- and off-list; this makes a
> > > lot of sense now.
> > >
> > > Best,
> > > Peter.
> >
> > --
> > Andreas Abel<><       Du bist der geliebte Mensch.
> >
> > Theoretical Computer Science, University of Munich
> > Oettingenstr. 67, D-80538 Munich, GERMANY
> >
> > andreas.abel AT ifi.lmu.de
> > http://www2.tcs.ifi.lmu.de/~abel/
>
>
> This message and any attachment are intended solely for the addressee and may 
> contain confidential information. If you have received this message in error, 
> please send it back to me, and immediately delete it.   Please do not use, 
> copy or disclose the information contained in this message or in any 
> attachment.  Any views or opinions expressed by the author of this email do 
> not necessarily reflect the views of the University of Nottingham.
>
> This message has been checked for viruses but the contents of an attachment
> may still contain software viruses which could damage your computer system:
> you are advised to perform your own checks. Email communications with the
> University of Nottingham may be monitored as permitted by UK legislation.

--
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel AT ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/