Skip to content

Instantly share code, notes, and snippets.

@CodaFi
Last active September 24, 2021 19:46
Show Gist options
  • Save CodaFi/7bb3bd00f04a9b26fd71 to your computer and use it in GitHub Desktop.
Save CodaFi/7bb3bd00f04a9b26fd71 to your computer and use it in GitHub Desktop.
// Playground - noun: a place where people can play
protocol ℕ {
static func construct() -> Self
static var value : UInt { get }
}
struct Zero : ℕ {
static func construct() -> Zero {
return Zero()
}
static var value : UInt {
return 0
}
}
struct Suc<N : ℕ> : ℕ {
static func construct() -> Suc<N> {
return Suc()
}
static var value : UInt {
return 1 + N.value
}
}
struct Ident<N : ℕ> : ℕ {
static func construct() -> Ident<N> {
return Ident()
}
static var value : UInt {
return N.value
}
}
struct Plus<N : ℕ , M : ℕ> : ℕ {
static func construct() -> Plus<N, M> {
return Plus()
}
static var value : UInt {
return N.value + M.value
}
}
struct Mult<N : ℕ , M : ℕ> : ℕ {
static func construct() -> Mult<N, M> {
return Mult()
}
static var value : UInt {
return N.value * M.value
}
}
func refl<N : ℕ>(n : N) -> N {
return n
}
func succ<N : ℕ>(n : N) -> Suc<N> {
return Suc<N>()
}
func +<N : ℕ>(n : N, _ : Zero) -> Plus<N, Zero> {
return Plus<N, Zero>()
}
func +<N : ℕ>(_ : Zero, n : N) -> Plus<Zero, N> {
return Plus<Zero, N>()
}
func +<N : ℕ, M : ℕ>(n : N, m : M) -> Plus<N, M> {
return Plus<N, M>()
}
func *<N : ℕ>(n : N, _ : Zero) -> Zero {
return Zero()
}
func *<N : ℕ>(_ : Zero, n : N) -> Zero {
return Zero()
}
func *<N : ℕ, M : ℕ>(n: N, m : M) -> Mult<N, M> {
return Mult<N, M>()
}
typealias _2 = Suc<Suc<Zero>>;
typealias _3 = Suc<Suc<Zero>>;
typealias _4 = Plus<Suc<Suc<Zero>>, Suc<Suc<Zero>>>
typealias _6 = Plus<Suc<Suc<Zero>>, Plus<Suc<Suc<Zero>>, Suc<Suc<Zero>>>>
typealias _8 = Mult<_4, _2>
let _15 = _2() + _3() + _4() + _6()
let _30 = _15 * _2()
let _22 = _15 + succ(_6())
let mix = _30 + _2() * _3() + _15 + _22
// Playground - noun: a place where people can play
// We're in ℤ country now
protocol ℤ {
static func construct() -> Self
static var value : Int { get }
}
struct Zero : ℤ {
static func construct() -> Zero {
return Zero()
}
static var value : Int {
return 0
}
}
struct Suc<N : ℤ> : ℤ {
static func construct() -> Suc<N> {
return Suc()
}
static var value : Int {
return 1 + N.value
}
}
struct Rec<N : ℤ> : ℤ {
static func construct() -> Rec<N> {
return Rec()
}
static var value : Int {
return N.value - 1
}
}
struct Ident<N : ℤ> : ℤ {
static func construct() -> Ident<N> {
return Ident()
}
static var value : Int {
return N.value
}
}
struct Plus<N : ℤ , M : ℤ> : ℤ {
static func construct() -> Plus<N, M> {
return Plus()
}
static var value : Int {
return N.value + M.value
}
}
struct Sub<N : ℤ , M : ℤ> : ℤ {
static func construct() -> Sub<N, M> {
return Sub()
}
static var value : Int {
return N.value - M.value
}
}
struct Mult<N : ℤ , M : ℤ> : ℤ {
static func construct() -> Mult<N, M> {
return Mult()
}
static var value : Int {
return N.value * M.value
}
}
func refl<N : ℤ>(n : N) -> N {
return n
}
func succ<N : ℤ>(n : N) -> Suc<N> {
return Suc<N>()
}
func recc<N : ℤ>(n : N) -> Rec<N> {
return Rec<N>()
}
func +<N : ℤ>(n : N, _ : Zero) -> Plus<N, Zero> {
return Plus<N, Zero>()
}
func +<N : ℤ>(_ : Zero, n : N) -> Plus<Zero, N> {
return Plus<Zero, N>()
}
func +<N : ℤ, M : ℤ>(n : N, m : M) -> Plus<N, M> {
return Plus<N, M>()
}
func -<N : ℤ>(n : N, _ : Zero) -> Sub<N, Zero> {
return Sub<N, Zero>()
}
func -<N : ℤ>(_ : Zero, n : N) -> Sub<Zero, N> {
return Sub<Zero, N>()
}
func -<N : ℤ, M : ℤ>(n : N, m : M) -> Sub<N, M> {
return Sub<N, M>()
}
func *<N : ℤ>(n : N, _ : Zero) -> Zero {
return Zero()
}
func *<N : ℤ>(_ : Zero, n : N) -> Zero {
return Zero()
}
func *<N : ℤ, M : ℤ>(n : N, m : M) -> Mult<N, M> {
return Mult<N, M>()
}
typealias _2 = Suc<Suc<Zero>>;
typealias _3 = Suc<Suc<Zero>>;
typealias _4 = Plus<Suc<Suc<Zero>>, Suc<Suc<Zero>>>
typealias _6 = Plus<Suc<Suc<Zero>>, Plus<Suc<Suc<Zero>>, Suc<Suc<Zero>>>>
typealias _8 = Mult<_4, _2>
let _15 = _2() + _3() + _4() + _6()
let _30 = _15 * _2()
let _22 = _30 - _8()
let mix = _30 + _2() * _3() + _15 - _22
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment