Parametrickery: Subtyping & Monotonicity

Sub.hs

{-# LANGUAGE DataKinds #-}

module Sub where


data Sub = S Sub

data Three (s :: Sub) a b c where
  One   :: a -> Three  s        a b c
  Two   :: b -> Three (S  s   ) a b c
  Three :: c -> Three (S (S s)) a b c

type LtEqOne   a b c = forall s. Three  s        a b c
type LtEqTwo   a b c = forall s. Three (S  s   ) a b c
type LtEqThree a b c = forall s. Three (S (S s)) a b c


-- Note that, similar to MonoMaybe, functions parametric in s:
--
--   forall s. Three s a b c -> Three s d e f
--
-- are monotonically decreasing.
--
-- Further, we obtain the subtyping relation:
--
--   LtEqOne a b c <: LtEqTwo a b c <: LtEqThree a b c
--
-- as evidenced below.

oneLtTwo :: LtEqOne a b c -> LtEqTwo a b c
oneLtTwo x = x

twoLtThree :: LtEqTwo a b c -> LtEqThree a b c
twoLtThree x = x