3 ms·

Yeah to me that description sounds like "static type checking". "First-class types" on the other hand means that types are expressions that can be manipulated

by chubot 5y ago

Yeah to me that description sounds like "static type checking". "First-class types" on the other hand means that types are expressions that can be manipulated at runtime, or by compile-time metaprogramming stage. I think Julia is very much like this: types are very complex expressions and they're expressed with the same machinery as arithmetic expressions (femtolisp).

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 ago
  What 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 ago
    Type 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.

by chubot 5y ago

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 ago
What 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 ago
  Type 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.