search

Gabriella439 / Haskell-Morte-Library

A bare-bones calculus-of-constructions
BSD 3-Clause "New" or "Revised" License
372 stars 25 forks source link

How do you encode isZero and pred in Morte? #71

Closed montokapro closed 6 years ago

montokapro commented 6 years ago

I've looked around and haven't noticed an example that transforms one type (ie Nat) to another type (ie Bool). Would anyone be interested in explaining how to write the isZero function for natural numbers?

Similarly, I'm having a hard time understanding how to write the predecessor function. In untyped lambda calculus, this takes nested lambda functions (http://jwodder.freeshell.org/lambda.html). I can find the source code for CC via Coq, but I'd be interested to see how that code differs from CoC and Morte.

Gabriella439 commented 6 years ago

I'll use Dhall notation since it will shorten the examples.

isZero would be:

λ(n : Natural) → Natural/fold n Bool (λ(_ : Bool) → False) True

Predecessor is inefficient (i.e. O(N)), but still possible:

  λ(n : Natural)
→ Natural/fold
  n
  (Optional Natural)
  (   λ(o : Optional Natural)
    → Optional/fold
      Natural
      o
      (Optional Natural)
      (λ(n : Natural) → [ n + +1 ] : Optional Natural)
      ([ +0 ] : Optional Natural)
  )
  ([] : Optional Natural)
montokapro commented 6 years ago

Phew! It took me longer than I'd like to admit, but I wrote your example in pure Morte and have a better understanding for it. I'll post the code tomorrow for other's reference. Thank you!

Regarding Dhall, I'm super excited to see CoC being used for package management and configuration... it seems perfectly suited :) Thank you for your hard work!

Gabriella439 commented 6 years ago

You're welcome! :)