Skip to content

Instantly share code, notes, and snippets.

@mxswd
Last active December 12, 2016 19:24
Show Gist options
  • Save mxswd/9fc8d19f6cc235c23158 to your computer and use it in GitHub Desktop.
Save mxswd/9fc8d19f6cc235c23158 to your computer and use it in GitHub Desktop.
Thanks @robrix and CodaFi_ for the discussion :D
// this is a playground
protocol Nat {
class func construct() -> Self
class func value() -> Int
}
struct Z : Nat {
static func construct() -> Z {
return Z()
}
static func value() -> Int {
return 0
}
}
struct S<N: Nat> : Nat {
static func construct() -> S<N> {
return S()
}
static func value() -> Int {
return 1 + N.value()
}
}
// how about type level bools
protocol BOOL {
class func value() -> Bool
}
struct TRUE : BOOL {
static func value() -> Bool {
return true
}
}
struct FALSE : BOOL {
static func value() -> Bool {
return false
}
}
// you saw identity before
func refl<N: Nat>(n: N) -> N {
return n
}
let twoEqualsTwo: S<S<Z>> = refl(S<S<Z>>())
// now succ, given X, give me S<X>
func succ<N: Nat>(n: N) -> S<N> {
return S<N>()
}
let twoSuccThree: S<S<S<Z>>> = succ(S<S<Z>>())
// cool, what about less than or equal?
func sub1<N: Nat, X: Nat>(proof: N -> S<X>)(n: N) -> X {
return X.construct()
}
// try to type it another way. you can't
let twoSubOne: S<Z> = sub1(refl)(n: S<S<Z>>())
twoSubOne // not a lie
// x less than y, needs some more type constraints... but compiler bugs exist.
// im cheating here a little.
func lessThan<N: Nat, M: Nat>(proof: M -> N)(n: N)(m: M) -> TRUE {
return TRUE()
}
// is 2 less than 1?
let onelessthantwo = lessThan(sub1(refl))(n: S<Z>())(m: S<S<Z>>())
let zerolessthantwo = lessThan(sub1(sub1(refl)))(n: Z())(m: S<S<Z>>())
// now something useful
struct MVec<A, L: Nat> {
let vec: Array<A>
func index<I: Nat>(i: I, n: S<I> -> L -> TRUE) -> A {
return vec[I.value()]
}
}
// you must provide a proof that an index is inside the bounds of the array
let v1: MVec<String, S<S<S<Z>>>> = MVec(vec: ["hello", "rob", "rix"])
v1.index(Z(), lessThan(sub1(sub1(refl))))
v1.index(S<Z>(), lessThan(sub1(refl)))
v1.index(S<S<Z>>(), lessThan(refl))
//v1.index(S<S<S<Z>>>(), lessThan(refl)) // type error, 3 > 2
@jbrennan
Copy link

What is a Nat? What is a Z?

@jbrennan
Copy link

Oh they’re numbers I get it.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment