Intrinsically typed DTLC?

Stream: general

[Sofia]

Hello world. I want to create an intrinsically typed DTLC implementation. a la https://repository.tudelft.nl/islandora/object/uuid:f0312839-3444-41ee-9313-b07b21b59c11

I currently have the following code describing STLC, and want to extend it to DTLC. My issue is specifically in upgrading the custom inductive Ty to Lean's Sort _ family, for all universes. Is there any way I can do this or have I hit the limits of Lean's expressiveness?

I'm using Lean 4 btw.

inductive Ty
| unit
| nat
| bool
| func (a b : Ty)

namespace Ty
    abbrev type : Ty -> Type
    | unit => Unit
    | nat => Nat
    | bool => Bool
    | func a b => a.type -> b.type
end Ty

inductive Cover : (x y z : List α) -> Prop
| done  : Cover [] [] []
| left  : Cover x y z -> Cover (t :: x) y (t :: z)
| right : Cover x y z -> Cover x (t :: y) (t :: z)
| both  : Cover x y z -> Cover (t :: x) (t :: y) (t :: z)

inductive Exp : Ty -> List Ty -> Type
| lift (x : t.type) : Exp t []
| var : Exp t [t]
| lam : Exp u (t :: Γ) -> Exp (Ty.func t u) Γ
| app : Exp (Ty.func t u) Γ₁ -> Exp t Γ₂ -> Cover Γ₁ Γ₂ Γ₃ -> Exp u Γ₃

[Sofia]

If I let my type be a Prop, which isn't quite helpful here... I can get at least the first few.

universe u

inductive Exp2 : Sort u -> List (Sort u) -> Prop
| lift (x : t) : Exp2 t []
| var : Exp2 t [t]
| lam : Exp2 u (t :: Γ) -> Exp2 (t -> u) Γ
--| app : Exp2 (t -> u) Γ₁ -> Exp2 t Γ₂ -> Cover Γ₁ Γ₂ Γ₃ -> Exp2 u Γ₃

With the last failing because each Γ needs to be the same type, due to the definition of Cover.

[Jannis Limperg]

Sofia said:

I want to create an intrinsically typed DTLC implementation.

This is considered very hard and personally, I don't see the point. Intrinsic STLC is nice because everything just falls into place. Intrinsic DTT very much doesn't fall into place, and any reduction in lines of code you might get will be paid for with many hours of bashing your head against a wall of mutual definitions (which Lean doesn't support well; Agda would be a better choice here). So if you can go extrinsic, do that.

Specifically for this universe issue, I don't quite understand what you're trying to do. If your language has universes, you should model them with a corresponding inductive, not with Lean universes. Prop is certainly not the way to go since your expressions should be computationally relevant. Also note that in Exp2, you give your expressions Lean types rather than types from your language.

[Sofia]

The objective of Exp2 is exactly "Can I inherit Lean's types instead of creating my own?"

[Jannis Limperg]

Okay, then I think the answer is no. This universe issue is one problem; a more fundamental one is that types do not have useful structure (or even equality). E.g. if you want to type a dependently-typed function, you need to substitute a value into the type of the body, but how do you substitute in a Lean type?

[Sofia]

Apply against a Pi?

[Sofia]

A friend linked me to https://pages.lip6.fr/Pierre-Evariste.Dagand/stuffs/thesis-2011-phd/thesis.pdf for implementing the type myself.

Could you link to research demonstrating an intrinsically typed DTLC is "considered very hard"?

[Jannis Limperg]

I just tried to write down a type for the lam constructor that concludes Exp (forall a, P a) Gamma and I don't even see what that would sensibly look like. I'm not familiar enough with the ornaments stuff to say definitively whether that is a relevant reference, but I suspect it won't help.

The issues with intrinsic DTT are folklore, so no specific references. Here's an example from my MSc thesis if that helps. This is a very mildly dependently-typed language: no universes and only specific constructs where dependencies can occur, so the intrinsic style still kinda works. But for example the type of fix contains substitutions, which made everything afterwards a little painful, and it took me a number of attempts to arrive at a formulation that worked. I'm sure the extrinsic style would have been much more straightforward, if also slightly more boilerplatey.

[Sofia]

The ornaments paper specifies its own inductive type family, among other more interesting things.

Thanks for the information. I'll still try for an intrinsic DTLC, but recognize I may just yield and use an extrinsic approach instead. If I get it working either way, I'll share the result.

[Kevin Buzzard]

In my experience, trying something which is believed to be hard is a really good way of getting a deeper understanding of the difficulties. It might not turn into a paper, but it makes you a wiser person.

[Sofia]

This is the idea. :)

[Jannis Limperg]

Good luck! If you do succeed, I'll be very interested in the results.