Re #2805 refactor: added Quantity to Relevance to form Modality

After this refactoring, all `Quantity`s are infinity (no effect).
Quantity0 should be used for runtime irrelevance.

See McBride, I got plenty of nutting (Wadlerfest 2016)

src/full/Agda/Syntax/Common.hs

@@ -211,6 +211,161 @@ sameHiding x y =
     (Instance{}, Instance{}) -> True
     (hx, hy)                 -> hx == hy
 
+---------------------------------------------------------------------------
+-- * Modalities
+---------------------------------------------------------------------------
+
+-- | We have a tuple of modalities, which might not be fully orthogonal.
+--   For instance, irrelevant stuff is also run-time irrelevant.
+data Modality = Modality
+  { modRelevance :: Relevance
+      -- ^ Legacy irrelevance.
+      --   See Pfenning, LiCS 2001; Abel/Vezzosi/Winterhalter, ICFP 2017.
+  , modQuantity  :: Quantity
+      -- ^ Cardinality / runtime erasure.
+      --   See Conor McBride, I got plenty o' nutting, Wadlerfest 2016.
+  } deriving (Typeable, Data, Eq, Ord, Show, Generic)
+
+defaultModality :: Modality
+defaultModality = Modality defaultRelevance defaultQuantity
+
+-- | Pointwise composition.
+instance Semigroup Modality where
+  Modality r q <> Modality r' q' = Modality (r <> r') (q <> q')
+
+-- | Pointwise unit.
+instance Monoid Modality where
+  mempty = Modality mempty mempty
+  mappend = (<>)
+
+-- | Dominance ordering.
+instance PartialOrd Modality where
+  comparable (Modality r q) (Modality r' q') = comparable (r, q) (r', q')
+
+instance POSemigroup Modality where
+instance POMonoid Modality where
+
+-- boilerplate instances
+
+instance KillRange Modality where
+  killRange = id
+
+instance NFData Modality where
+
+class LensModality a where
+
+  getModality :: a -> Modality
+
+  setModality :: Modality -> a -> a
+  setModality = mapModality . const
+
+  mapModality :: (Modality -> Modality) -> a -> a
+  mapModality f a = setModality (f $ getModality a) a
+
+instance LensModality Modality where
+  getModality = id
+  setModality = const
+  mapModality = id
+
+instance LensRelevance Modality where
+  getRelevance = modRelevance
+  setRelevance h m = m { modRelevance = h }
+  mapRelevance f m = m { modRelevance = f (modRelevance m) }
+
+instance LensQuantity Modality where
+  getQuantity = modQuantity
+  setQuantity h m = m { modQuantity = h }
+  mapQuantity f m = m { modQuantity = f (modQuantity m) }
+
+-- default accessors for Relevance
+
+getRelevanceMod :: LensModality a => LensGet Relevance a
+getRelevanceMod = getRelevance . getModality
+
+setRelevanceMod :: LensModality a => LensSet Relevance a
+setRelevanceMod = mapModality . setRelevance
+
+mapRelevanceMod :: LensModality a => LensMap Relevance a
+mapRelevanceMod = mapModality . mapRelevance
+
+-- default accessors for Quantity
+
+getQuantityMod :: LensModality a => LensGet Quantity a
+getQuantityMod = getQuantity . getModality
+
+setQuantityMod :: LensModality a => LensSet Quantity a
+setQuantityMod = mapModality . setQuantity
+
+mapQuantityMod :: LensModality a => LensMap Quantity a
+mapQuantityMod = mapModality . mapQuantity
+
+---------------------------------------------------------------------------
+-- * Quantities
+---------------------------------------------------------------------------
+
+-- | Quantity for linearity.
+data Quantity
+  = Quantity0  -- ^ Zero uses, erased at runtime.
+  -- TODO: | Quantity1  -- ^ Linear use (could be updated destructively).
+  -- (needs postponable constraints between quantities to compute uses).
+  | Quantityω  -- ^ Unrestricted use.
+  deriving (Typeable, Data, Show, Generic, Eq, Enum, Bounded)
+
+defaultQuantity :: Quantity
+defaultQuantity = Quantityω
+
+-- | Composition of quantities (multiplication).
+--
+-- 'Quantity0' is dominant.
+instance Semigroup Quantity where
+  Quantity0 <> _ = Quantity0
+  _ <> Quantity0 = Quantity0
+  Quantityω <> _ = Quantityω
+  -- _ <> Quantityω = Quantityω  -- redundant
+
+-- | In the absense of finite quantities besides 0, ω is the unit.
+instance Monoid Quantity where
+  mempty = Quantityω
+  mappend = (<>)
+
+-- | Note that the order is @ω ≤ 0@, more relevant is smaller.
+instance Ord Quantity where
+  compare = curry $ \case
+    (Quantityω, Quantityω) -> EQ
+    (Quantityω, Quantity0) -> LT
+    (Quantity0, Quantityω) -> GT
+    (Quantity0, Quantity0) -> EQ
+
+instance PartialOrd Quantity where
+  comparable = comparableOrd
+
+instance POSemigroup Quantity where
+instance POMonoid Quantity where
+
+-- boilerplate instances
+
+class LensQuantity a where
+
+  getQuantity :: a -> Quantity
+
+  setQuantity :: Quantity -> a -> a
+  setQuantity = mapQuantity . const
+
+  mapQuantity :: (Quantity -> Quantity) -> a -> a
+  mapQuantity f a = setQuantity (f $ getQuantity a) a
+
+instance LensQuantity Quantity where
+  getQuantity = id
+  setQuantity = const
+  mapQuantity = id
+
+instance KillRange Quantity where
+  killRange = id
+
+instance NFData Quantity where
+  rnf Quantity0 = ()
+  rnf Quantityω = ()
+
 ---------------------------------------------------------------------------
 -- * Relevance
 ---------------------------------------------------------------------------
@@ -449,7 +604,7 @@ instance LensOrigin (WithOrigin a) where
 
 data ArgInfo = ArgInfo
   { argInfoHiding       :: Hiding
-  , argInfoRelevance    :: Relevance
+  , argInfoModality     :: Modality
   , argInfoOrigin       :: Origin
   } deriving (Typeable, Data, Eq, Ord, Show)
 
@@ -476,20 +631,35 @@ instance LensHiding ArgInfo where
   setHiding h ai = ai { argInfoHiding = h }
   mapHiding f ai = ai { argInfoHiding = f (argInfoHiding ai) }
 
-instance LensRelevance ArgInfo where
-  getRelevance = argInfoRelevance
-  setRelevance h ai = ai { argInfoRelevance = h }
-  mapRelevance f ai = ai { argInfoRelevance = f (argInfoRelevance ai) }
+instance LensModality ArgInfo where
+  getModality = argInfoModality
+  setModality m ai = ai { argInfoModality = m }
+  mapModality f ai = ai { argInfoModality = f (argInfoModality ai) }
 
 instance LensOrigin ArgInfo where
   getOrigin = argInfoOrigin
   setOrigin o ai = ai { argInfoOrigin = o }
   mapOrigin f ai = ai { argInfoOrigin = f (argInfoOrigin ai) }
 
+-- inherited instances
+
+instance LensRelevance ArgInfo where
+  getRelevance = getRelevanceMod
+  setRelevance = setRelevanceMod
+  mapRelevance = mapRelevanceMod
+
+instance LensQuantity ArgInfo where
+  getQuantity = getQuantityMod
+  setQuantity = setQuantityMod
+  mapQuantity = mapQuantityMod
+
 defaultArgInfo :: ArgInfo
-defaultArgInfo =  ArgInfo { argInfoHiding       = NotHidden
-                          , argInfoRelevance    = Relevant
-                          , argInfoOrigin       = UserWritten }
+defaultArgInfo =  ArgInfo
+  { argInfoHiding       = NotHidden
+  , argInfoModality     = defaultModality
+  , argInfoOrigin       = UserWritten
+  }
+
 -- Accessing through ArgInfo
 
 -- default accessors for Hiding
@@ -503,6 +673,17 @@ setHidingArgInfo = mapArgInfo . setHiding
 mapHidingArgInfo :: LensArgInfo a => LensMap Hiding a
 mapHidingArgInfo = mapArgInfo . mapHiding
 
+-- default accessors for Modality
+
+getModalityArgInfo :: LensArgInfo a => LensGet Modality a
+getModalityArgInfo = getModality . getArgInfo
+
+setModalityArgInfo :: LensArgInfo a => LensSet Modality a
+setModalityArgInfo = mapArgInfo . setModality
+
+mapModalityArgInfo :: LensArgInfo a => LensMap Modality a
+mapModalityArgInfo = mapArgInfo . mapModality
+
 -- default accessors for Origin
 
 getOriginArgInfo :: LensArgInfo a => LensGet Origin a
@@ -536,16 +717,19 @@ instance SetRange a => SetRange (Arg a) where
 instance KillRange a => KillRange (Arg a) where
   killRange (Arg info a) = killRange2 Arg info a
 
--- | Ignores 'Relevance' and 'Origin'.
+-- | Ignores 'Quantity', 'Relevance', and 'Origin'.
 --   Ignores content of argument if 'Irrelevant'.
 --
 instance Eq a => Eq (Arg a) where
-  Arg (ArgInfo h1 r1 _) x1 == Arg (ArgInfo h2 r2 _) x2 =
-    h1 == h2 && (r1 == Irrelevant || r2 == Irrelevant || x1 == x2)
+  Arg (ArgInfo h1 m1 _) x1 == Arg (ArgInfo h2 m2 _) x2 =
+    h1 == h2 && (isIrrelevant m1 || isIrrelevant m2 || x1 == x2)
     -- Andreas, 2017-10-04, issue #2775, ignore irrelevant arguments during with-abstraction.
+    -- This is a hack, we should not use '(==)' in with-abstraction
+    -- and more generally not use it on Syntax.
+    -- Andrea: except for caching.
 
 instance Show a => Show (Arg a) where
-    show (Arg (ArgInfo h r o) a) = showR r $ showO o $ showH h $ show a
+    show (Arg (ArgInfo h (Modality r q) o) a) = showQ q $ showR r $ showO o $ showH h $ show a
       where
         showH Hidden       s = "{" ++ s ++ "}"
         showH NotHidden    s = "(" ++ s ++ ")"
@@ -557,6 +741,9 @@ instance Show a => Show (Arg a) where
           NonStrict    -> "?" ++ s
           Forced       -> "!" ++ s
           Relevant     -> "r" ++ s -- Andreas: I want to see it explicitly
+        showQ q s = case q of
+          Quantity0   -> "0" ++ s
+          Quantityω   -> "ω" ++ s
         showO o s = case o of
           UserWritten -> "u" ++ s
           Inserted    -> "i" ++ s
@@ -578,15 +765,27 @@ instance LensHiding (Arg e) where
   setHiding = setHidingArgInfo
   mapHiding = mapHidingArgInfo
 
-instance LensRelevance (Arg e) where
-  getRelevance = getRelevance . argInfo
-  mapRelevance = mapArgInfo . mapRelevance
+instance LensModality (Arg e) where
+  getModality = getModalityArgInfo
+  setModality = setModalityArgInfo
+  mapModality = mapModalityArgInfo
 
 instance LensOrigin (Arg e) where
   getOrigin = getOriginArgInfo
   setOrigin = setOriginArgInfo
   mapOrigin = mapOriginArgInfo
 
+-- Since we have LensModality, we get relevance and quantity by default
+
+instance LensRelevance (Arg e) where
+  getRelevance = getRelevanceMod
+  setRelevance = setRelevanceMod
+  mapRelevance = mapRelevanceMod
+
+instance LensQuantity (Arg e) where
+  getQuantity = getQuantityMod
+  setQuantity = setQuantityMod
+  mapQuantity = mapQuantityMod
 
 defaultArg :: a -> Arg a
 defaultArg = Arg defaultArgInfo
@@ -648,9 +847,10 @@ instance HasRange a => HasRange (Dom a) where
 instance KillRange a => KillRange (Dom a) where
   killRange (Dom info a) = killRange2 Dom info a
 
+-- | Ignores 'Origin' and 'Forced'.
 instance Eq a => Eq (Dom a) where
-  Dom (ArgInfo h1 r1 _) x1 == Dom (ArgInfo h2 r2 _) x2 =
-    (h1, ignoreForced r1, x1) == (h2, ignoreForced r2, x2)
+  Dom (ArgInfo h1 m1 _) x1 == Dom (ArgInfo h2 m2 _) x2 =
+    (h1, mapRelevance ignoreForced m1, x1) == (h2, mapRelevance ignoreForced m2, x2)
 
 instance Show a => Show (Dom a) where
   show = show . argFromDom
@@ -660,21 +860,34 @@ instance LensArgInfo (Dom e) where
   setArgInfo ai dom = dom { domInfo = ai }
   mapArgInfo f  dom = dom { domInfo = f $ domInfo dom }
 
-instance LensRelevance (Dom e) where
-  getRelevance = getRelevance . domInfo
-  mapRelevance = mapArgInfo . mapRelevance
 -- The other lenses are defined through LensArgInfo
 
 instance LensHiding (Dom e) where
   getHiding = getHidingArgInfo
   setHiding = setHidingArgInfo
   mapHiding = mapHidingArgInfo
 
+instance LensModality (Dom e) where
+  getModality = getModalityArgInfo
+  setModality = setModalityArgInfo
+  mapModality = mapModalityArgInfo
+
 instance LensOrigin (Dom e) where
   getOrigin = getOriginArgInfo
   setOrigin = setOriginArgInfo
   mapOrigin = mapOriginArgInfo
 
+-- Since we have LensModality, we get relevance and quantity by default
+
+instance LensRelevance (Dom e) where
+  getRelevance = getRelevanceMod
+  setRelevance = setRelevanceMod
+  mapRelevance = mapRelevanceMod
+
+instance LensQuantity (Dom e) where
+  getQuantity = getQuantityMod
+  setQuantity = setQuantityMod
+  mapQuantity = mapQuantityMod
 
 argFromDom :: Dom a -> Arg a
 argFromDom (Dom i a) = Arg i a

src/full/Agda/TypeChecking/MetaVars.hs

@@ -1159,9 +1159,12 @@ inverseSubst args = map (mapFst unArg) <$> loop (zip args terms)
               | length fs == length vs -> do
                 let aux (Arg _ v) (Arg info' f) = (Arg ai v,) $ t `applyE` [Proj ProjSystem f] where
                      ai = ArgInfo
-                       { argInfoHiding       = min (getHiding info) (getHiding info')
-                       , argInfoRelevance    = max (getRelevance info) (getRelevance info')
-                       , argInfoOrigin       = min (getOrigin info) (getOrigin info')
+                       { argInfoHiding   = min (getHiding info) (getHiding info')
+                       , argInfoModality = Modality
+                         { modRelevance  = max (getRelevance info) (getRelevance info')
+                         , modQuantity   = max (getQuantity  info) (getQuantity  info')
+                         }
+                       , argInfoOrigin   = min (getOrigin info) (getOrigin info')
                        }
                 res <- loop $ zipWith aux vs fs
                 return $ res `append` vars

src/full/Agda/TypeChecking/Serialise/Instances/Common.hs

@@ -433,6 +433,21 @@ instance EmbPrj Hiding where
   value 3 = return (Instance YesOverlap)
   value _ = malformed
 
+instance EmbPrj Quantity where
+  icod_ Quantity0 = return 0
+  icod_ Quantityω = return 1
+
+  value 0 = return Quantity0
+  value 1 = return Quantityω
+  value _ = malformed
+
+instance EmbPrj Modality where
+  icod_ (Modality a b) = icodeN' Modality a b
+
+  value = vcase $ \case
+    [a, b] -> valuN Modality a b
+    _ -> malformed
+
 instance EmbPrj Relevance where
   icod_ Relevant       = return 0
   icod_ Irrelevant     = return 1