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 express Maybe in morte? #65

Closed AnthonyJacob closed 6 years ago

AnthonyJacob commented 6 years ago

Suppose I have the following line of code in Haskell

data Maybe = Just a | Nothing

How do I compile it to morte expression and then back to Haskell again?

puffnfresh commented 6 years ago

It's expressed via a Scott encoding:

https://github.com/Gabriel439/Haskell-Morte-Library/blob/master/Prelude/Maybe/Just

https://github.com/Gabriel439/Haskell-Morte-Library/blob/master/Prelude/Maybe/Nothing

Which looks like this in Haskell:

type Maybe' a
  = forall b. (a -> b) -> b -> b

just :: a -> Maybe' a
just a f _ = f a

nothing :: Maybe' a
nothing _ a = a
Gabriella439 commented 6 years ago

See also this library:

https://github.com/Gabriel439/Haskell-Annah-Library

... which automates Church encoding data types and this blog post which explains the process:

http://www.haskellforall.com/2016/04/data-is-code.html