"Back to Direct Style: Typed and Tight" Discussions

[b-studios]

👋 Welcome!

We’re using Discussions as a place to connect with other members of our community. We hope that you:

• Ask questions you’re wondering about.
• Share ideas.
• Engage with other community members.
• Welcome others and are open-minded. Remember that this is a community we
  build together 💪.

To get started, comment below with an introduction of yourself and tell us about what you do with this community.

[ju-sh]

What does the Sub type for structural rules for contexts mean?

Is it like subtypes? As in:

  -- xs :> xs
  Keep : Sub xs xs

  -- xs :> (y::xs)
  Weak : Sub xs (y :: xs)

  -- xs :> ys → (x::xs) :> (y::ys)
  Lift : Sub xs ys -> Sub (x :: xs) (x :: ys)

  -- xs :> ys → ys :> zs → xs :> zs
  Comp : Sub xs ys -> Sub ys zs -> Sub xs zs

  -- x::y::zs :> y::x::zs
  Swap : Sub (x :: y :: zs) (y :: x :: zs)

  -- x::x::xs :> x::xs
  Copy : Sub (x :: x :: xs) (x :: xs)

I'm new to this kind of things as was trying to learn..

[b-studios]

Hey, thanks for your question. Sub is not related to subtyping, it is short for "substitution".
Keep is the noop substitution that does not change anything. Weak means "weakening", that is, an additional binder is available in the context that needs to be ignored by existing variables.

The meaning of Sub can best be seen in the definition of rename.

rename : Sub xs ys -> Name xs x -> Name ys x
rename Keep x = x
rename Weak x = S x
rename (Lift a) Z = Z
rename (Lift a) (S x) = S (rename a x)
rename (Comp a b) x = rename b (rename a x)
rename Swap Z = S Z
rename Swap (S Z) = Z
rename Swap (S (S x)) = S (S x)
rename Copy Z = Z
rename Copy (S y) = y

Variables are de-bruijn, so we need to rename them, when we introduce a binder, etc.