4 ms·
> types are very complex expressions and they're expressed with the same machinery as arithmetic expressions (femtolisp). This is how it works in Yatima. Since
by jcburnham 5y ago
> types are very complex expressions and they're expressed with the same machinery as arithmetic expressions (femtolisp).
This is how it works in Yatima. Since we use self-types and lambda-encodings for our datatypes, all type expressions are built up via some combination of self types, pi types and a few type-level constants (like primitives).
For example, the type of booleans can be expressed as:
def Bool : Type =
@self ∀
(0 P : ∀ (Bool) -> Type)
(& true : P (data λ P t f => t))
(& false : P (data λ P t f => f))
-> P self
def true : Bool = data λ P t f => t
def false : Bool = data λ P t f => f
from https://github.com/yatima-inc/introit/blob/main/Pure/Bool.ya https://github.com/yatima-inc/introit/blob/main/Pure/Bool.ya
- skulk 5y agoWhat is 'Type'? Is it a Type as well? In a toy dependent type system I'm building I just declared the top type as an instance of itself without caring about soundness. I'm curious what the approach is here.
- jcburnham 5y agoType is a builtin currently, with `Type : Type`, which makes the type system unsound. There are a couple ways of addressing that that we've explored, like the standard universe polymorphism hierarchy of `Type 0 : Type 1 : Type 2 ...`, but we've also looked at more exotic solutions like whether there's actually a self-type lambda encoding of `Type` itself (which would allow for `case` matching on `Type`). Haven't quite figured it out though, so for the moment `Type : Type` is an acceptable shim while we work on getting everything else working.