Compile-Time Dependent Types

27 points by polywolf

fanf

Syl has two mode axes: staticity and erasure.

A static value is knowable at compile time; a dynamic value may not be.

An unerased value is knowable at runtime; an erased value may not be.

I wonder why these are two axes, rather than three points on a single axis, i.e. dynamic <: const / static <: erased, i.e. when does it make sense for a dynamic value to be erased?

Also I wonder how this two-level type theory relates to the quantitative type theory used for similar purposes in Idris. The papers on the theories don’t compare either with the other.

jado
Dynamic + erased values will be erased / irrelevant for runtime computation and may be unknown at comptime, e.g. a function that takes the length of a Vec type as another param:
```
foo : {0 n : Nat} -> Vect n Int -> Int
```
Idris2's QTT models this with 0 / 1 / w: n is used 0 times at runtime and can be erased from the final program. Any usages of this within the runtime relevant parts of the program would be a compilation error, but usages within types are fine. We don't need to know the concrete value of n & we can erase all of the usages of it within those types.

Syl doesn't look like it's capable of type checking that with a dynamic n.

Here, erased also implies static, so f will be specialized on x. The if erased expression accepts a static erased condition and is guaranteed to resolve at compile time. Therefore, the body of f true is simply print_int 0, and likewise for f false.

Like Zig it's doing monomorphization on the comptime params. foo above need not be specialized for every value of n. In Syl, every distinct value of n passed to foo would need a specialized program in the final compilation unit. iiuc, the "second level" of 2LTT allows for the representation of the specialized functions, while QTT wouldn't require this specialization or a second layer representation (and can track linearity).
landon

The one i'm struggling with is static + erased. Known at compile time but not runtime?

pervognsen

I've experimented with simple designs in this space but not very recently. Anyway, regarding the theorem proving side of things that you lose because of...

"Although this type system would not be suitable for a theorem proving language, it does not rule out type safety or even useful proofs. It has two practical consequences:

Functions used in type-level computations may diverge, so typechecking is not decidable.
Functions don’t discharge universally quantified claims, so the compiler must evaluate all applications that produce proofs before relying on their results."

"Not suitable" seems to assume the type inhabitation approach to theorem proving, as in Rocq, Agda and Lean. But an alternative is some version of the HOL-family approach, as in HOL4, HOL Light and Isabelle/HOL. Then you can still use internal compile-time computation for proof automation. To be able to prove things about the code itself (and reflect it back to the compiler as trusted facts), you need a sound translation from code to logic or from logic to code. Code to logic is more ergonomic and therefore more attractive for the end-user, but it is trickier to get right with respect to soundness (which ties to the issue with divergence).

Another way to put it is that if you have a sufficiently expressive compile-time system then you can build a bridge to an external proof system (exposed as a set of opaque LCF-style primitives) and still have internal proof automation, internal syntactic abstraction and all the rest, as opposed to having a jarring transition between the internal and external worlds.

I haven't thought much about it in this context, so maybe you run into unresolvable issues. Hopefully experts can chime in.

amw-zero

I honestly know a fair bit of type theory, and this is confusing to me:

That is, Syl is dependently typed at compile time and simply typed at runtime.

For me, "typed at runtime" means dynamically typed. Is that the case here, or does that just mean that it has a "regular" type system after the staging layer?

pervognsen

does that just mean that it has a "regular" type system after the staging layer?

I think that's the only way the statement makes sense. E.g. if you look at section 2.4.1 of Staged Compilation with Two-Level Type Theory where monomorphization is discussed as an option, the residual language is simply typed.
- amw-zero
  
  Yea, the paper goes into it. I guess it's saying, these are the types that describe the values that actually execute during the program's runtime. Pretty suspect choice of terminology since everyone calls these static types already, and then the paper calls the macro / meta-level types "static types."
jado

This is probably referring to simply typed lambda calc, meaning the dependent bits are erased and there are no types depending on runtime values.

I made a similar toy lang that extracts out the runtime program by erasing runtime irrelevant parts (which here are explicitly marked with a . prefix). This extracted program is a typed IR and could be translated to LLVM IR or similar quite easily.

aziis98

I also wanted to try making a small language with these ideas!

I realized that Rust is the only popular language in the intersection of safe, sound and without a gc for memory management. I would like a language where the type system is very flexible and powerful like typescript or zig comptime but have the runtime language be completely safe and allow for manual memory management. I don't really care the type system/comptime system might be slow, that would be the user/library author problem to keep compile time code reasonable. And the language could also provide nice primitives for easily returning custom errors or linting rules (I think there were some experimental languages on this front but I don't remember the names)