Both are excellent points, thank you.
Your mention of general recursion prompts the following: in 1995, ten years
after publication of Boehm-Berarducci, Launchbury and Sheard investigated
transformation of programs written in general recursive form into
build-foldr form, with an eye towards the no
On Wed, Sep 26, 2012 at 12:41 AM, wrote:
> First of all, the Boehm-Berarducci encoding is inefficient only when
> doing an operation that is not easily representable as a fold. Quite
> many problems can be efficiently tackled by a fold.
Indeed. Some operations are even more efficient than usuall
> Wouldn't you say then that "Church encoding" is still the more appropriate
> reference given that Boehm-Berarducci's algorithm is rarely used?
>
> When I need to encode pattern matching it's goodbye Church and hello Scott.
> Aside from your projects, where else is the B-B procedure used?
First
On Thu, Sep 20, 2012 at 3:15 PM, wrote:
> Incidentally, there is more than one way to build a predecessor of Church
> numerals. Kleene's solution is not the only one.
Wouldn't you say then that "Church encoding" is still the more appropriate
reference given that Boehm-Berarducci's algorithm is r
> 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
Inducti
On Thu, 20 Sep 2012, Jay Sulzberger wrote:
On Thu, 20 Sep 2012, o...@okmij.org wrote:
Dan Doel wrote:
P.S. It is actually possible to write zip function using
Boehm-Berarducci
encoding:
http://okmij.org/ftp/Algorithms.html#zip-folds
If you do, you might want to consider not us
On Thu, 20 Sep 2012, o...@okmij.org wrote:
Dan Doel wrote:
P.S. It is actually possible to write zip function using Boehm-Berarducci
encoding:
http://okmij.org/ftp/Algorithms.html#zip-folds
If you do, you might want to consider not using the above method, as I
seem to recall it doi
Dan Doel wrote:
> >> P.S. It is actually possible to write zip function using Boehm-Berarducci
> >> encoding:
> >> http://okmij.org/ftp/Algorithms.html#zip-folds
>
> If you do, you might want to consider not using the above method, as I
> seem to recall it doing an undesirable amount of ex
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
On 9/18/12 4:27 AM, o...@okmij.org 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 =
On Tue, Sep 18, 2012 at 8:39 PM, Dan Doel wrote:
> 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))
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 rew
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-indu
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 f
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-calc
Oleg,
Let me try to understand what you're saying here:
(1) Church encoding was discovered and investigated in an untyped setting.
I understand your tightness criterion to mean surjectivity, the absence of
which means having to deal with junk.
(2) Church didn't give an encoding for pattern-match
On 18 September 2012 18:27, 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 ChurchL
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 ->
18 matches
Mail list logo
