3 ms·
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 sou
by 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 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.