Singleton scope types

[fizruk]

It is currently necessary to pass down Scope n as an extra parameter in many functions, and then extend it manually via extendScope or extendScopePattern. However, it appears that the scopes can be extracted from the type directly via an approach a la singleton package or type level literals in GHC. In particular, the idea is that we could introduce the following typeclass

class Distinct n => KnownScope n where
  theScope :: Scope n
  
class (KnownScope n, Ext n l) => KnownExt n l
instance (KnownScope n, Ext n l) => KnownExt n l

Of course, the empty scope is known:

instance KnownScope VoidS where
  theScope = emptyScope

The tricky part is to make extended scopes known in functions like withFresh:

withFresh :: KnownScope n => Scope n -> (forall (l :: S). KnownExt n l => NameBinder n l -> r) -> r

One way to achieve this would be to extend data kind S:

data S = VoidS | ExtS (i :: Nat) S

instance (KnownScope scope, KnownNat i, Fresh i scope) => KnownScope (ExtS i scope) where
  theScope = UnsafeScope (IntSet.insert i scope)
    where UnsafeScope scope = theScope @scope

The Fresh constraint should ensure that i is indeed fresh in scope. I think, an alternative to adding this constraint is to hide ExtS from the user.

The definition of Fresh could follow something like this:

class Fresh (i :: Nat) (scope :: S)

instance Fresh i VoidS

instance (Fresh i s, Not (i == j)) => Fresh i (ExtS j s)

However, I'm not sure the Not (i == j) part is possible to express properly in haskell, since type equality can yield False for polymorphic types and KnownNat is not enough to force i and j to be known statically.

It might be worth looking into permissive nominal terms¹, as I have a strong suspicion that the foil is at least related to that.

Footnotes

1. Gilles Dowek, Murdoch J. Gabbay, Dominic P. Mulligan, Permissive nominal terms and their unification: an infinite, co-infinite approach to nominal techniques, Logic Journal of the IGPL, Volume 18, Issue 6, December 2010, Pages 769–822, https://doi.org/10.1093/jigpal/jzq006 ↩