This paper: http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.26.957 Induction is Not Derivable in Second Order Dependent Type Theory, shows, well, that you can't encode naturals with a strong induction principle in said theory. At all, no matter what tricks you try. However, A Logic for Parametric Polymorphism, http://www.era.lib.ed.ac.uk/bitstream/1842/205/1/Par_Poly.pdf Indicates that in a type theory incorporating relational parametricity of its own types, the induction principle for the ordinary Church-like encoding of natural numbers can be derived. I've done some work here: http://code.haskell.org/~dolio/agda-share/html/ParamInduction.html for some simpler types (although, I've been informed that sigma was novel, it not being a Simple Type), but haven't figured out natural numbers yet (I haven't actually studied the second paper above, which I was pointed to recently). -- Dan On Tue, Sep 18, 2012 at 5:41 PM, Ryan Ingram wrote:

Oleg, do you have any references for the extension of lambda-encoding of data into dependently typed systems?

In particular, consider Nat:

nat_elim :: forall P:(Nat -> *). P 0 -> (forall n:Nat. P n -> P (succ n)) -> (n:Nat) -> P n

The naive lambda-encoding of 'nat' in the untyped lambda-calculus has exactly the correct form for passing to nat_elim:

nat_elim pZero pSucc n = n pZero pSucc

with

zero :: Nat zero pZero pSucc = pZero

succ :: Nat -> Nat succ n pZero pSucc = pSucc (n pZero pSucc)

But trying to encode the numerals this way leads to "Nat" referring to its value in its type!

type Nat = forall P:(Nat -> *). P 0 -> (forall n:Nat. P n -> P (succ n)) -> P ???

Is there a way out of this quagmire? Or are we stuck defining actual datatypes if we want dependent types?

-- ryan

On Tue, Sep 18, 2012 at 1:27 AM, wrote:

...

There has been a recent discussion of ``Church encoding'' of lists and the comparison with Scott encoding.

I'd like to point out that what is often called Church encoding is actually Boehm-Berarducci encoding. That is, often seen

...

newtype ChurchList a = CL { cataCL :: forall r. (a -> r -> r) -> r -> r }

(in http://community.haskell.org/%7Ewren/list-extras/Data/List/Church.hs )

is _not_ Church encoding. First of all, Church encoding is not typed and it is not tight. The following article explains the other difference between the encodings

http://okmij.org/ftp/tagless-final/course/Boehm-Berarducci.html

Boehm-Berarducci encoding is very insightful and influential. The authors truly deserve credit.

P.S. It is actually possible to write zip function using Boehm-Berarducci encoding: http://okmij.org/ftp/ftp/Algorithms.html#zip-folds

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

On Tue, Sep 18, 2012 at 11:19 PM, Ryan Ingram wrote:

Fascinating!

But it looks like you still 'cheat' in your induction principles...

×-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)

Can you somehow define

x-induction {A} {B} {P} f p = p (P p) f

No, or at least I don't know how. The point is that with parametricity, I can prove that if p : A × B, then p = (fst p , snd p). Then when I need to prove P p, I change the obligation to P (fst p , snd p). But i have (forall x y. P (x , y)) given. I don't know why you think that's cheating. If you thought it was going to be a straight-forward application of the Church (or some other) encoding, that was the point of the first paper (that's impossible). But parametricity can be used to prove statements _about_ the encodings that imply the induction principle.

On Tue, Sep 18, 2012 at 4:09 PM, Dan Doel wrote:

...

This paper:

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

Induction is Not Derivable in Second Order Dependent Type Theory, shows, well, that you can't encode naturals with a strong induction principle in said theory. At all, no matter what tricks you try.

However, A Logic for Parametric Polymorphism,

http://www.era.lib.ed.ac.uk/bitstream/1842/205/1/Par_Poly.pdf

Indicates that in a type theory incorporating relational parametricity of its own types, the induction principle for the ordinary Church-like encoding of natural numbers can be derived. I've done some work here:

http://code.haskell.org/~dolio/agda-share/html/ParamInduction.html

for some simpler types (although, I've been informed that sigma was novel, it not being a Simple Type), but haven't figured out natural numbers yet (I haven't actually studied the second paper above, which I was pointed to recently).

-- Dan

On Tue, Sep 18, 2012 at 5:41 PM, Ryan Ingram wrote:

...

Oleg, do you have any references for the extension of lambda-encoding of data into dependently typed systems?

In particular, consider Nat:

nat_elim :: forall P:(Nat -> *). P 0 -> (forall n:Nat. P n -> P (succ n)) -> (n:Nat) -> P n

The naive lambda-encoding of 'nat' in the untyped lambda-calculus has exactly the correct form for passing to nat_elim:

nat_elim pZero pSucc n = n pZero pSucc

with

zero :: Nat zero pZero pSucc = pZero

succ :: Nat -> Nat succ n pZero pSucc = pSucc (n pZero pSucc)

But trying to encode the numerals this way leads to "Nat" referring to its value in its type!

type Nat = forall P:(Nat -> *). P 0 -> (forall n:Nat. P n -> P (succ n)) -> P ???

Is there a way out of this quagmire? Or are we stuck defining actual datatypes if we want dependent types?

-- ryan

On Tue, Sep 18, 2012 at 1:27 AM, wrote:

...

There has been a recent discussion of ``Church encoding'' of lists and the comparison with Scott encoding.

I'd like to point out that what is often called Church encoding is actually Boehm-Berarducci encoding. That is, often seen

...

newtype ChurchList a = CL { cataCL :: forall r. (a -> r -> r) -> r -> r }

(in http://community.haskell.org/%7Ewren/list-extras/Data/List/Church.hs )

is _not_ Church encoding. First of all, Church encoding is not typed and it is not tight. The following article explains the other difference between the encodings

http://okmij.org/ftp/tagless-final/course/Boehm-Berarducci.html

Boehm-Berarducci encoding is very insightful and influential. The authors truly deserve credit.

P.S. It is actually possible to write zip function using Boehm-Berarducci encoding: http://okmij.org/ftp/ftp/Algorithms.html#zip-folds

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

do you have any references for the extension of lambda-encoding of data into dependently typed systems?

Is there a way out of this quagmire? Or are we stuck defining actual datatypes if we want dependent types?

Although not directly answering your question, the following paper Inductive Data Types: Well-ordering Types Revisited Healfdene Goguen Zhaohui Luo http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.17.8970&rep=rep1&type=pdf might still be relevant. Sec 2 reviews the major approaches to inductive data types in Type Theory.

On Wed, Sep 19, 2012 at 8:36 PM, wren ng thornton wrote:

...

P.S. It is actually possible to write zip function using Boehm-Berarducci encoding: http://okmij.org/ftp/ftp/Algorithms.html#zip-folds

Of course it is; I just never got around to doing it :)

If you do, you might want to consider not using the above method, as I seem to recall it doing an undesirable amount of extra work (repeated O(n) tail). One can do better with some controversial types (this is not my idea originally; ski (don't know his real name) on freenode's #haskell showed it to me a long time ago): ---- snip ---- {-# LANGUAGE PolymorphicComponents #-} module ABC where newtype L a = L { unL :: forall r. (a -> r -> r) -> r -> r } nil :: L a nil = L $ \_ z -> z cons :: a -> L a -> L a cons x (L xs) = L $ \f -> f x . xs f newtype A a c = Roll { unroll :: (a -> A a c -> L c) -> L c } type B a c = a -> A a c -> L c zipWith :: (a -> b -> c) -> L a -> L b -> L c zipWith f (L as) (L bs) = unroll (as consA nilA) (bs consB nilB) where -- nilA :: A a c nilA = Roll $ const nil -- consA :: a -> A a c -> A a c consA x xs = Roll $ \k -> k x xs -- nilB :: B a c nilB _ _ = nil -- consB :: b -> B a c -> B a c consB y ys x xs = f x y `cons` unroll xs ys ---- snip ---- This traverses each list only once. -- Dan