Parametricity and data kinds

Question

I am wondering about the MonoMaybe type family from the monad-validation Haskell library written by Alexis King. Its definition is as follows (ignoring strictness):

{-# LANGUAGE GADTs, DataKinds #-}
data MonoMaybeS = SMaybe | SJust

data MonoMaybe (s :: MonoMaybeS) a where
  MNothing :: MonoMaybe 'SMaybe a
  MJust :: forall s a. a -> MonoMaybe s a

This is analogous to Maybe, but the type forall s. MonoMaybe s A -> MonoMaybe s B enforces the invariant that the function is "monotonically increasing", in that it can only output MNothing when given MNothing, by parametricity. However, usual parametricity allows one to reason about universal quantification on the universe, while here s has type MonoMaybeS (which in GHC Haskell is "promoted" to the type level by the DataKinds extension).

Questions: how can we analyse the above? Is there a type theory in which one can define an indexed type family like above and prove an equivalence between $\forall s. \text{MonoMaybe}\ s\ A \to \text{MonoMaybe}\ s\ B$ and the subtype of $\text{Maybe}\ A \to \text{Maybe}\ B$ on the monotonically increasing functions? Can e.g. parametric cubical type theory à la Cavallo & Harper do this?

I have the following geometric intuition for the total space of $\lambda s. \text{MonoMaybe}\ s\ A$:

The indexing type $\text{MonoMaybeS}$ behaves as a sort of abstract interval (in particular one is not able to case split on it) which seems like it might have to do with bridge types.

Answer 1

I'm not sure there's any ready made system for precisely this (at least, I haven't seen/understood it yet). There's lots of adjacent work, though.

Cavallo & Harper isn't it, because it's modelling something like the normal parametricity situation, where because you don't have type-case, $Π$ types over the universe have to be uniform with respect to discrete results. But the Haskell example is the sort of scenario where you have two different $Π$ types. One is the normal $Π$ (which yields Haskell functions) and the other is a parametric $Π$ (Haskell $∀$) that is parametric because of computational irrelevance, regardless of what you're quantifying over.

So, to model this situation, I think you need something more like Nuyts, Vezossi & Devriese, which has a separate parametric $Π$. However, I think the problem with this is that each type is equipped with a particular notion of bridge, and the ones for data types like MonoMaybeS are just discrete, so being 'parametric' in them is still not any different than the normal $Π$.

But, you could probably say that MonoMaybeS is different from similar types described in teh paper in that its bridges match what happens in Haskell. I think that means you want the type to be bridge indiscrete (all values are related). Or maybe just say that things like (small) data types are bridge indiscrete instead of discrete to model the Haskell situation.

There is also work on modelling reasons underlying this sort of parametricity. For instance, Nathan Mishra-Linger's thesis has a system with computational irrelevance (which is not quite the same as e.g. Agda's irrelevance), involving two varieties of $Π$. But I don't believe it includes the parametricity aspects induced by irrelevance (at the time internal parametricity was an open question, I think). The only extra theorems you get are the simple ones that result from erasing irrelevant things.

Perhaps Sterling and Harper's Logical Relations as Types can handle all this. I cannot tell.

Answer 2

If you just want to avoid having a case on MonoMaybeS, you should be able to parametrize over it and use any version of parametricity that handles dependent types. In Coq, the type I'm suggesting would be using the definition

Inductive MonoMaybe (MonoMaybeS : Type) (SMaybe : MonoMaybeS) (SJust : MonoMaybeS) : MonoMaybeS -> Type -> Type :=
| MNothing : forall a, MonoMaybe MonoMaybeS SMaybe SJust SMaybe a
| MJust : forall s a, a -> MonoMaybe MonoMaybeS SMaybe SJust s a
.

and the type forall MonoMaybeS SMaybe SJust a b s, MonoMaybe MonoMaybeS SMaybe SJust s a -> MonoMaybe MonoMaybeS SMaybe SJust s b