Skip to content

Instantly share code, notes, and snippets.

@decorator-factory
Created March 14, 2023 21:20
Show Gist options
  • Save decorator-factory/23b775c458e233f294deeaab241cfc58 to your computer and use it in GitHub Desktop.
Save decorator-factory/23b775c458e233f294deeaab241cfc58 to your computer and use it in GitHub Desktop.
Lambda calculus interlude
-- Lazy System F (lazy as in -- I am too lazy to specify all the boring bits)
--- boolean (this is a popular implementation in lambda calculus)
Bool = ∀x. x -> x -> x
true : Bool
true = λt f. t
false : Bool
false = λt f. f
--- color channel
RgbChannel = ∀x. x -> x -> x -> x
red : RgbChannel
red = λr g b. r
green : RgbChannel
green = λr g b. g
blue : RgbChannel
blue = λr g b. b
--- maybe (now we need a type parameter)
Maybe = ∀a. ∀x. x -> (a -> x) -> x
nothing : ∀a. Maybe a
nothing = λn j. n
just : ∀a. a -> Maybe a
just = λa. λn j. j a
--- lists (now we need self-reference!)
List = ∀a. ∀x. x -> (a -> x -> x) -> x
nil : ∀a. List a
nil = λinit step. n
cons : ∀a. a -> List a -> List a
cons = λhead tail. λinit step. step head (tail init step)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment