Typelevelisation

more_types!.swift

import Foundation



func fix <A>(_ f : (A) -> A) -> A { f (fix (f)) }

// _ = fix { _ in }

indirect enum N {
    case s(N), z
}

// let odd : (N) -> Bool = fix { f in { v -> Bool in
//     switch v {
//     case let N.s(.s(a)) : return f (a)
//     case .z : return true
//     default : return false } }
// }
// print (odd (N.s(.s(.s(.z)))))

struct Box<T> { let value: T }

// func make <T>() -> Box<T> {
//     func rec <K>() -> K {
//         if Bool.random() {
//             return Box.init(value: rec())
//         } else { return "!" }
//     }
//     return rec()
// }


protocol TList {
    associatedtype L
    associatedtype R : TList
}
protocol ConsKind {
    associatedtype A
    associatedtype B
}
enum Cons <A, B : TList> : TList, ConsKind {
    typealias L = A
    typealias R = B
}
enum End : TList {
    typealias L = End
    typealias R = End
}

indirect enum HList<T : TList> {
    case cons(T.L, HList<T.R>), end
}

precedencegroup ListConstructor {
    associativity: right
}
infix operator |- : ListConstructor
func |- <A,B>(l: A, b: HList<B>) -> HList<Cons<A,B>> {
    .cons(l, b)
}
func |- <A>(l: A, b: HList<End>) -> HList<Cons<A, End>> {
    .cons(l, .end)
}

extension TList where R == End {
    typealias _Last = L
}
extension TList {
    typealias Rec<T : TList> = T._Last
    typealias Last = Rec<Self>
}

print (type(of: Cons<Int, Cons<String, End>>.Last.self)) // weird one!

let k = 1 |- "2" |- 0.3 |- .end
print(type(of: k))


extension TList where Self : ConsKind {
    typealias NonEmpty = Yes
}

// func last <T>(_ v: HList<T>) -> T.Last where T.NonEmpty == Yes {
//     switch v {
//         case let .cons(a, .end) : return a
//         case let .cons(_, tail) : return last (tail)
//         default : fatalError("IF YOU SEE ME, THEN YOUR REALITY IS FUCKING BROKEN ! ! !")
//     }
// }
enum Yes {}
enum None {}

extension TList where L == R.L, L == None {
    typealias Equivalent2Nat = Yes
}
indirect enum CountedArray<Elem, Size: TList> where Size.Equivalent2Nat == Yes {
    case cons(Elem, CountedArray<Elem, Size.R>), end
}
func |- <A, S>(l: A, r: CountedArray<A, S>) -> CountedArray<A, Cons<End, S>> {
    .cons (l, r)
}
func |- <A>(l: A, r: CountedArray<A, End>) -> CountedArray<A, Cons<End, End>> {
    .cons (l, .end)
}

let _2elemthing : CountedArray = 1 |- 2 |- .end
//print (type(of: _2elemthing))

func safeHead <A,S>(of arr: CountedArray<A, Cons<End, S>>) -> A {
    switch arr {
    case let .cons (a, _): return a
    default : fatalError("IF YOU SEE ME, THEN YOUR REALITY IS FUCKING BROKEN ! ! !")
    }
    
}
print (safeHead(of: _2elemthing))

let emptyarr : CountedArray<Int, End> = .end
//print (safeHead(of:emptyarr)) -- fails :thumb_up: