Kind already supports recursive types. For example:
SNat : Type
SNat = (t: Type) -> (s: SNat -> t) -> (z: t) -> t
Works and type-checks. But actually trying to use it will be problematic. For example:
SNat.zero : SNat
SNat.zero = t => s => z => z
Checks, but:
SNat.succ (n: SNat) : SNat
SNat.succ n = t => s => z => (s n)
Doesn't; it will hang. That's because the equal function will be stuck in a loop (print it to get an idea). Ideally, Kind would deal with that seamlessly, but that's not the case yet. One way this could be done, as suggested by @tjjfvi and @FranchuFranchu:
Add a "Fix" constructor, with some syntax like fix x: T
On the equality, just transform fix x: (F x) == fix x: (G x) into (F (G x)) == (G (F x)) - that's enough
When translating to HVM, just translate fix x: T to (Fix @x T), where (Fix t) = (t (Fix t)).
Kind already supports recursive types. For example:
Works and type-checks. But actually trying to use it will be problematic. For example:
Checks, but:
Doesn't; it will hang. That's because the
equalfunction will be stuck in a loop (print it to get an idea). Ideally, Kind would deal with that seamlessly, but that's not the case yet. One way this could be done, as suggested by @tjjfvi and @FranchuFranchu:Add a "Fix" constructor, with some syntax like
fix x: TOn the equality, just transform
fix x: (F x) == fix x: (G x)into(F (G x)) == (G (F x))- that's enoughWhen translating to HVM, just translate
fix x: Tto(Fix @x T), where(Fix t) = (t (Fix t)).