[TYPES] Representing inductive types with W-types

[roconnor at theorem.ca]

Does this mean that containers are "the same" as strictly positive 
functors?

Because all strictly postive functors are isomorphic to some container, 
and every container is a strictly positive functor?

On Thu, 17 Nov 2011, Altenkirch Thorsten wrote:

> Hi Russell,
>
> I think our work on containers is relevant here. You can show that any
> strictly positive functor can be represented as a container, I.e. A
> functor of the form
> F X = Sigma s:S. P s -> X where S : Set, P : S -> Set, I.e. the signature
> of a W-type.
> Actually for your example you need n-ary containers to handle nested types.
>
> The relevant results are in our '05 Journal paper
> http://www.cs.nott.ac.uk/~txa/publ/cont-tcs.pdf
> And in Michael Abbot's PhD.
>
> Recently (with Peter Morris) we extended this to dependent types, this
> appeared in LICS 2009 http://www.cs.nott.ac.uk/~txa/publ/ICont.pdf
>
> Cheers,
> Thorsten
>
> On 17/11/2011 20:57, "roconnor at theorem.ca" <roconnor at theorem.ca> wrote:
>
>> [ The Types Forum,
>> http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
>>
>> Does anyone have a reference on how to encode (non-mutually recursive)
>> inductive data type declarations of a language similar to CiC using
>> W-Types?
>>
>> I was playing around with this by hand, and I can make ad-hoc encodings
>> for the types I've tried; but I haven't quite figured out what the
>> systematic translation is.  For example, I find
>>
>> Inductive Tree (A:Type) : Type :=
>> node : A -> list (Tree A) -> Tree A
>>
>> quite difficult to translate.  I can only manage because I happen to know
>> that list X ~ Sigma n:nat. Fin n -> X
>>
>> where Fin
>>
>> Fin 0 = Void
>> Fin (S n) = Unit + Fin n
>>
>> By my ad hoc method I get
>>
>> nat ~ W : Bool. if b then Void else Unit
>> list A ~ W x : Unit + A. [const Void | const Unit] x
>> Tree A ~ W (a,n):A*nat. Fin n
>>
>> But of course nat and Fin do not directly appear in the Inductive
>> definition of Tree, so I'm not entirely sure how to deduce them (or
>> something isomorphic) systematically.
>>
>> --
>> Russell O'Connor                                      <http://r6.ca/>
>> ``All talk about `theft,''' the general counsel of the American
>> Graphophone
>> Company wrote, ``is the merest claptrap, for there exists no property in
>> ideas musical, literary or artistic, except as defined by statute.''
>
> 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.

-- 
Russell O'Connor                                      <http://r6.ca/>
``All talk about `theft,''' the general counsel of the American Graphophone
Company wrote, ``is the merest claptrap, for there exists no property in
ideas musical, literary or artistic, except as defined by statute.''