Fascinating!<br><br>But it looks like you still 'cheat' in your induction principles...<br><pre><a name="3768">
</a>×-induction : ∀{A B} {P : A × B → Set}
→ ((x : A) → (y : B) → P (x , y))
→ (p : A × B) → P p
×-induction {A} {B} {P} f p rewrite sym (×-η p) = f (fst p) (snd p)</pre>Can you somehow define<br><br>x-induction {A} {B} {P} f p = p (P p) f<br><br><br><div class="gmail_quote">On Tue, Sep 18, 2012 at 4:09 PM, Dan Doel <span dir="ltr"><<a href="mailto:dan.doel@gmail.com" target="_blank">dan.doel@gmail.com</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">This paper:<br>
<br>
<a href="http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.26.957" target="_blank">http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.26.957</a><br>
<br>
Induction is Not Derivable in Second Order Dependent Type Theory,<br>
shows, well, that you can't encode naturals with a strong induction<br>
principle in said theory. At all, no matter what tricks you try.<br>
<br>
However, A Logic for Parametric Polymorphism,<br>
<br>
<a href="http://www.era.lib.ed.ac.uk/bitstream/1842/205/1/Par_Poly.pdf" target="_blank">http://www.era.lib.ed.ac.uk/bitstream/1842/205/1/Par_Poly.pdf</a><br>
<br>
Indicates that in a type theory incorporating relational parametricity<br>
of its own types, the induction principle for the ordinary<br>
Church-like encoding of natural numbers can be derived. I've done some<br>
work here:<br>
<br>
<a href="http://code.haskell.org/~dolio/agda-share/html/ParamInduction.html" target="_blank">http://code.haskell.org/~dolio/agda-share/html/ParamInduction.html</a><br>
<br>
for some simpler types (although, I've been informed that sigma was<br>
novel, it not being a Simple Type), but haven't figured out natural<br>
numbers yet (I haven't actually studied the second paper above, which<br>
I was pointed to recently).<br>
<span class="HOEnZb"><font color="#888888"><br>
-- Dan<br>
</font></span><div class="HOEnZb"><div class="h5"><br>
On Tue, Sep 18, 2012 at 5:41 PM, Ryan Ingram <<a href="mailto:ryani.spam@gmail.com">ryani.spam@gmail.com</a>> wrote:<br>
> Oleg, do you have any references for the extension of lambda-encoding of<br>
> data into dependently typed systems?<br>
><br>
> In particular, consider Nat:<br>
><br>
> nat_elim :: forall P:(Nat -> *). P 0 -> (forall n:Nat. P n -> P (succ<br>
> n)) -> (n:Nat) -> P n<br>
><br>
> The naive lambda-encoding of 'nat' in the untyped lambda-calculus has<br>
> exactly the correct form for passing to nat_elim:<br>
><br>
> nat_elim pZero pSucc n = n pZero pSucc<br>
><br>
> with<br>
><br>
> zero :: Nat<br>
> zero pZero pSucc = pZero<br>
><br>
> succ :: Nat -> Nat<br>
> succ n pZero pSucc = pSucc (n pZero pSucc)<br>
><br>
> But trying to encode the numerals this way leads to "Nat" referring to its<br>
> value in its type!<br>
><br>
> type Nat = forall P:(Nat -> *). P 0 -> (forall n:Nat. P n -> P (succ n))<br>
> -> P ???<br>
><br>
> Is there a way out of this quagmire? Or are we stuck defining actual<br>
> datatypes if we want dependent types?<br>
><br>
> -- ryan<br>
><br>
><br>
><br>
> On Tue, Sep 18, 2012 at 1:27 AM, <<a href="mailto:oleg@okmij.org">oleg@okmij.org</a>> wrote:<br>
>><br>
>><br>
>> There has been a recent discussion of ``Church encoding'' of lists and<br>
>> the comparison with Scott encoding.<br>
>><br>
>> I'd like to point out that what is often called Church encoding is<br>
>> actually Boehm-Berarducci encoding. That is, often seen<br>
>><br>
>> > newtype ChurchList a =<br>
>> > CL { cataCL :: forall r. (a -> r -> r) -> r -> r }<br>
>><br>
>> (in <a href="http://community.haskell.org/%7Ewren/list-extras/Data/List/Church.hs" target="_blank">http://community.haskell.org/%7Ewren/list-extras/Data/List/Church.hs</a> )<br>
>><br>
>> is _not_ Church encoding. First of all, Church encoding is not typed<br>
>> and it is not tight. The following article explains the other<br>
>> difference between the encodings<br>
>><br>
>> <a href="http://okmij.org/ftp/tagless-final/course/Boehm-Berarducci.html" target="_blank">http://okmij.org/ftp/tagless-final/course/Boehm-Berarducci.html</a><br>
>><br>
>> Boehm-Berarducci encoding is very insightful and influential. The<br>
>> authors truly deserve credit.<br>
>><br>
>> P.S. It is actually possible to write zip function using Boehm-Berarducci<br>
>> encoding:<br>
>> <a href="http://okmij.org/ftp/ftp/Algorithms.html#zip-folds" target="_blank">http://okmij.org/ftp/ftp/Algorithms.html#zip-folds</a><br>
>><br>
>><br>
>><br>
>><br>
>> _______________________________________________<br>
>> Haskell-Cafe mailing list<br>
>> <a href="mailto:Haskell-Cafe@haskell.org">Haskell-Cafe@haskell.org</a><br>
>> <a href="http://www.haskell.org/mailman/listinfo/haskell-cafe" target="_blank">http://www.haskell.org/mailman/listinfo/haskell-cafe</a><br>
><br>
><br>
><br>
> _______________________________________________<br>
> Haskell-Cafe mailing list<br>
> <a href="mailto:Haskell-Cafe@haskell.org">Haskell-Cafe@haskell.org</a><br>
> <a href="http://www.haskell.org/mailman/listinfo/haskell-cafe" target="_blank">http://www.haskell.org/mailman/listinfo/haskell-cafe</a><br>
><br>
</div></div></blockquote></div><br>