Documentation of `PartialRenaming`

[hirrolot]

In 03-holes/Main.hs, we have the following lines of code:

-- partial renaming from Γ to Δ
data PartialRenaming = PRen {
    dom :: Lvl                -- size of Γ
  , cod :: Lvl                -- size of Δ
  , ren :: IM.IntMap Lvl }    -- mapping from Δ vars to Γ vars

I don't get why the first comment says that the renaming is from "Γ to Δ", while the last comment says that it's from "Δ vars to Γ vars". Is this a typo?

[AndrasKovacs]

It's not a typo. A renaming from Gamma to Delta can be represented as a function from Delta vars to Gamma vars. This flipping is a fairly common thing in type theory literature.

For an illustration, assume Gamma = (a : A, b : B) and Delta = (c : C, d : D). Then, in many semantics of a type theory, Gamma and Delta are interpreted as some kind of record/sigma types, and a renaming from Gamma to Delta is a function of the form \(a, b) -> (t1, t2) where t1 and t2 must be variables. However, every such function is determined by a mapping (c |-> t1, d |-> t2) where t1 and t2 are variables. So, a renaming in the forward direction, from Gamma to Delta, is also representable as a function from variables to variables in the backwards direction.

[hirrolot]

Why \(a, b, c) -> (t1, t2) and not \(a, b) -> (t1, t2)?

[AndrasKovacs]

Well, that was a typo, thanks! Edited.

[hirrolot]

Okay, so PartialRenaming represents a function of the form \(a, b) -> (t1, t2) in the example you've suggested, but is implemented (by the ren field) in the backwards direction (c |-> t1, d |-> t2)?

[AndrasKovacs]

Yes.

It's only "morally" a function \(a, b) -> (t1, t2), not literally. The point is, the direction of the arrow in "renaming from Gamma to Delta" is more useful than the other way around, because it's much more common in semantics that way.

[hirrolot]

Sweet, thank you for your explanation.

[hirrolot]

I also have a few questions about the function invert that generates PartialRenaming.

First, I see this comment:

--  invert : (Γ : Cxt) → (spine : Sub Δ Γ) → PRen Γ Δ

But 1) the first parameter is of type Lvl, not Cxt, 2) I don't see Sub Δ Γ defined anywhere in the file, not sure what that means, and 3) spine is not one of the function parameters, invert actually accepts sp.

Next, in the implementation of invert, we construct pure $ PRen dom gamma ren, where dom is the length of the spine, and gamma is the first parameter of invert. But, looking at the docs:

-- partial renaming from Γ to Δ
data PartialRenaming = PRen {
    dom :: Lvl                -- size of Γ
  , cod :: Lvl                -- size of Δ
  , ren :: IM.IntMap Lvl }    -- mapping from Δ vars to Γ vars

dom is actually the "size of Γ" and cod is the "size of Δ", so I am a bit confused why PRen is constructed the other way round in invert.

The definition of `invert`

```haskell -- invert : (Γ : Cxt) → (spine : Sub Δ Γ) → PRen Γ Δ invert :: Lvl -> Spine -> IO PartialRenaming invert gamma sp = do let go :: Spine -> IO (Lvl, IM.IntMap Lvl) go [] = pure (0, mempty) go (sp :> t) = do (dom, ren) <- go sp case force t of VVar (Lvl x) | IM.notMember x ren -> pure (dom + 1, IM.insert x dom ren) _ -> throwIO UnifyError (dom, ren) <- go sp pure $ PRen dom gamma ren ```

[AndrasKovacs]

A Sub Gamma Delta is a parallel substitution. A renaming is a special case of a substitution which maps vars to vars. A substitution maps vars to arbitrary values.

Here (spine : Sub Gamma Delta) means that spine is a sequence of values, one value for each variables in Delta, such that each value can depend on variables from Gamma. A spine here is just a list of arguments that a meta is applied to, so it happens to be the same thing as a Sub (both are lists of values). sp is the abbreviation of spine.

Gamma and Delta in PRen Gamma Delta and Sub Gamma Delta are just arbitrary variable names. I can alpha-rename abstracted variables however I like.

In a formalization, we'd write Gamma for a context, but in the implementation the only computationally relevant information is just the length of the context. So in the Haskell code a context becomes a Lvl. If instead of De Bruijn levels and indices, we used non-shadowing names, we would need to pass a list of names instead of a Lvl. But this is mostly an implementation detail, the main idea is to pass enough information about a typing context, to be able to do some operations. Usually the only relevant operation is to create a variable which is fresh in a context. There are some more advanced unification algorithms where actual lists of types may be needed.

[hirrolot]

Maybe you meant Sub Delta Gamma instead of Sub Gamma Delta? Because the code says Sub Δ Γ.

Also, I don't understand why we do IM.insert x dom ren, i.e., associating a gamma-variable x with a delta-variable dom, while PartialRenaming says that ren maps delta-variables to gamma-variables.

[AndrasKovacs]

The choice of gamma and delta is completely arbitrary and you can consistently rename them in any context. When I talk about functions from A to B the names "A" and "B" have no importance at all. Same with "gamma" and "delta".

[hirrolot]

Interesting. I think I've understood the Haskell implementation itself, but the comments introduce so much confusion to me. Perhaps they'd be more clear considering the formalism...

Anyhow, thank you for the help!