[ new ] Data.OpenUnion (#1050)

libs/contrib/Control/Monad/Syntax.idr

@@ -1,20 +0,0 @@
-module Control.Monad.Syntax
-
-%default total
-
-infixr 1 =<<, <=<, >=>
-
-||| Left-to-right Kleisli composition of monads.
-public export
-(>=>) : Monad m => (a -> m b) -> (b -> m c) -> (a -> m c)
-(>=>) f g = \x => f x >>= g
-
-public export
-||| Right-to-left Kleisli composition of monads, flipped version of `>=>`.
-(<=<) : Monad m => (b -> m c) -> (a -> m b) -> (a -> m c)
-(<=<) = flip (>=>)
-
-public export
-||| Right-to-left monadic bind, flipped version of `>>=`.
-(=<<) : Monad m => (a -> m b) -> m a -> m b
-(=<<) = flip (>>=)

libs/contrib/Control/Validation.idr

@@ -11,7 +11,6 @@ module Control.Validation
 -- failing early with a nice error message if it isn't.
 
 import Control.Monad.Identity
-import Control.Monad.Syntax
 import Control.Monad.Error.Either
 import Data.Nat
 import Data.Strings

libs/contrib/Data/List/AtIndex.idr

@@ -0,0 +1,109 @@
+module Data.List.AtIndex
+
+import Data.DPair
+import Data.List.HasLength
+import Data.Nat
+import Decidable.Equality
+
+%default total
+
+||| @AtIndex witnesses the fact that a natural number encodes a membership proof.
+||| It is meant to be used as a runtime-irrelevant gadget to guarantee that the
+||| natural number is indeed a valid index.
+public export
+data AtIndex : a -> List a -> Nat -> Type where
+  Z : AtIndex a (a :: as) Z
+  S : AtIndex a as n -> AtIndex a (b :: as) (S n)
+
+||| Inversion principle for Z constructor
+export
+inverseZ : AtIndex x (y :: xs) Z -> x === y
+inverseZ Z = Refl
+
+||| inversion principle for S constructor
+export
+inverseS : AtIndex x (y :: xs) (S n) -> AtIndex x xs n
+inverseS (S p) = p
+
+||| An empty list cannot possibly have members
+export
+Uninhabited (AtIndex a [] n) where
+  uninhabited Z impossible
+  uninhabited (S _) impossible
+
+||| For a given list and a given index, there is only one possible value
+||| stored at that index in that list
+export
+atIndexUnique : AtIndex a as n -> AtIndex b as n -> a === b
+atIndexUnique Z Z = Refl
+atIndexUnique (S p) (S q) = atIndexUnique p q
+
+||| Provided that equality is decidable, we can look for the first occurence
+||| of a value inside of a list
+public export
+find : DecEq a => (x : a) -> (xs : List a) -> Dec (Subset Nat (AtIndex x xs))
+find x [] = No (\ p => void (absurd (snd p)))
+find x (y :: xs) with (decEq x y)
+  find x (x :: xs) | Yes Refl = Yes (Element Z Z)
+  find x (y :: xs) | No neqxy = case find x xs of
+      Yes (Element n prf) => Yes (Element (S n) (S prf))
+      No notInxs => No \case
+        (Element Z p) => void (neqxy (inverseZ p))
+        (Element (S n) prf) => absurd (notInxs (Element n (inverseS prf)))
+
+||| If the equality is not decidable, we may instead rely on interface resolution
+public export
+interface FindElement (0 t : a) (0 ts : List a) where
+  findElement : Subset Nat (AtIndex t ts)
+
+FindElement t (t :: ts) where
+  findElement = Element 0 Z
+
+FindElement t ts => FindElement t (u :: ts) where
+  findElement = let (Element n prf) = findElement in
+                Element (S n) (S prf)
+
+||| Given an index, we can decide whether there is a value corresponding to it
+public export
+lookup : (n : Nat) -> (xs : List a) -> Dec (Subset a (\ x => AtIndex x xs n))
+lookup n [] = No (\ p => void (absurd (snd p)))
+lookup Z (x :: xs) = Yes (Element x Z)
+lookup (S n) (x :: xs) = case lookup n xs of
+  Yes (Element x p) => Yes (Element x (S p))
+  No notInxs => No (\ (Element x p) => void (notInxs (Element x (inverseS p))))
+
+||| An AtIndex proof implies that n is less than the length of the list indexed into
+public export
+inRange : (n : Nat) -> (xs : List a) -> (0 _ : AtIndex x xs n) -> LTE n (length xs)
+inRange n [] p = void (absurd p)
+inRange Z (x :: xs) p = LTEZero
+inRange (S n) (x :: xs) p = LTESucc (inRange n xs (inverseS p))
+
+|||
+export
+weakenR : AtIndex x xs n -> AtIndex x (xs ++ ys) n
+weakenR Z = Z
+weakenR (S p) = S (weakenR p)
+
+export
+weakenL : (p : Subset Nat (HasLength ws)) -> AtIndex x xs n -> AtIndex x (ws ++ xs) (fst p + n)
+weakenL m p = case view m of
+  Z     => p
+  (S m) => S (weakenL m p)
+
+export
+strengthenL : (p : Subset Nat (HasLength xs)) ->
+              lt n (fst p) === True ->
+              AtIndex x (xs ++ ys) n -> AtIndex x xs n
+strengthenL m lt idx = case view m of
+  S m => case idx of
+    Z => Z
+    S idx => S (strengthenL m lt idx)
+
+export
+strengthenR : (p : Subset Nat (HasLength ws)) ->
+              lte (fst p) n === True ->
+              AtIndex x (ws ++ xs) n -> AtIndex x xs (minus n (fst p))
+strengthenR m lt idx = case view m of
+  Z => rewrite minusZeroRight n in idx
+  S m => case idx of S idx => strengthenR m lt idx

libs/contrib/Data/List/HasLength.idr

@@ -0,0 +1,138 @@
+||| This module implements a relation between a natural number and a list.
+||| The relation witnesses the fact the number is the length of the list.
+|||
+||| It is meant to be used in a runtime-irrelevant fashion in computations
+||| manipulating data indexed over lists where the computation actually only
+||| depends on the length of said lists.
+|||
+||| Instead of writing:
+||| ```
+||| f0 : (xs : List a) -> P xs
+||| ```
+|||
+||| We would write either of:
+||| ```
+||| f1 : (n : Nat) -> (0 _ : HasLength xs n) -> P xs
+||| f2 : (n : Subset n (HasLength xs)) -> P xs
+||| ```
+|||
+||| See `sucR` for an example where the update to the runtime-relevant Nat is O(1)
+||| but the udpate to the list (were we to keep it around) an O(n) traversal.
+
+module Data.List.HasLength
+
+import Data.DPair
+import Data.List
+
+%default total
+
+------------------------------------------------------------------------
+-- Type
+
+||| Ensure that the list's length is the provided natural number
+public export
+data HasLength : List a -> Nat -> Type where
+  Z : HasLength [] Z
+  S : HasLength xs n -> HasLength (x :: xs) (S n)
+
+------------------------------------------------------------------------
+-- Properties
+
+||| The length is unique
+export
+hasLengthUnique : HasLength xs m -> HasLength xs n -> m === n
+hasLengthUnique Z Z = Refl
+hasLengthUnique (S p) (S q) = cong S (hasLengthUnique p q)
+
+||| This specification corresponds to the length function
+export
+hasLength : (xs : List a) -> HasLength xs (length xs)
+hasLength [] = Z
+hasLength (_ :: xs) = S (hasLength xs)
+
+export
+map : (f : a -> b) -> HasLength xs n -> HasLength (map f xs) n
+map f Z = Z
+map f (S n) = S (map f n)
+
+||| @sucR demonstrates that snoc only increases the lenght by one
+||| So performing this operation while carrying the list around would cost O(n)
+||| but relying on n together with an erased HasLength proof instead is O(1)
+export
+sucR : HasLength xs n -> HasLength (snoc xs x) (S n)
+sucR Z = S Z
+sucR (S n) = S (sucR n)
+
+------------------------------------------------------------------------
+-- Views
+
+namespace SubsetView
+
+  ||| We provide this view as a convenient way to perform nested pattern-matching
+  ||| on values of type `Subset Nat (HasLength xs)`. Functions using this view will
+  ||| be seen as terminating as long as the index list `xs` is left untouched.
+  ||| See e.g. listTerminating below for such a function.
+  public export
+  data View : (xs : List a) -> Subset Nat (HasLength xs) -> Type where
+    Z : View [] (Element Z Z)
+    S : (p : Subset Nat (HasLength xs)) -> View (x :: xs) (Element (S (fst p)) (S (snd p)))
+
+  ||| This auxiliary function gets around the limitation of the check ensuring that
+  ||| we do not match on runtime-irrelevant data to produce runtime-relevant data.
+  viewZ : (0 p : HasLength xs Z) -> View xs (Element Z p)
+  viewZ Z = Z
+
+  ||| This auxiliary function gets around the limitation of the check ensuring that
+  ||| we do not match on runtime-irrelevant data to produce runtime-relevant data.
+  viewS : (n : Nat) -> (0 p : HasLength xs (S n)) -> View xs (Element (S n) p)
+  viewS n (S p) = S (Element n p)
+
+  ||| Proof that the view covers all possible cases.
+  export
+  view : (p : Subset Nat (HasLength xs)) -> View xs p
+  view (Element Z p) = viewZ p
+  view (Element (S n) p) = viewS n p
+
+namespace CurriedView
+
+  ||| We provide this view as a convenient way to perform nested pattern-matching
+  ||| on pairs of values of type `n : Nat` and `HasLength xs n`. If transformations
+  ||| to the list between recursive calls (e.g. mapping over the list) that prevent
+  ||| it from being a valid termination metric, it is best to take the Nat argument
+  ||| separately from the HasLength proof and the Subset view is not as useful anymore.
+  ||| See e.g. natTerminating below for (a contrived example of) such a function.
+  public export
+  data View : (xs : List a) -> (n : Nat) -> HasLength xs n -> Type where
+    Z : View [] Z Z
+    S : (n : Nat) -> (0 p : HasLength xs n) -> View (x :: xs) (S n) (S p)
+
+  ||| Proof that the view covers all possible cases.
+  export
+  view : (n : Nat) -> (0 p : HasLength xs n) -> View xs n p
+  view Z Z = Z
+  view (S n) (S p) = S n p
+
+------------------------------------------------------------------------
+-- Examples
+
+-- /!\ Do NOT re-export these examples
+
+listTerminating : (p : Subset Nat (HasLength xs)) -> HasLength (xs ++ [x]) (S (fst p))
+listTerminating p = case view p of
+  Z => S Z
+  S p => S (listTerminating p)
+
+data P : List Nat -> Type where
+  PNil : P []
+  PCon : P (map id xs) -> P (x :: xs)
+
+covering
+notListTerminating : (p : Subset Nat (HasLength xs)) -> P xs
+notListTerminating p = case view p of
+  Z => PNil
+  S p => PCon (notListTerminating {xs = map id (tail xs)} (record { snd $= map id } p))
+
+natTerminating : (n : Nat) -> (0 p : HasLength xs n) -> P xs
+natTerminating n p = case view n p of
+  Z => PNil
+  S n p => PCon (natTerminating n (map id p))

libs/contrib/Data/Nat/Order/Properties.idr

@@ -25,11 +25,20 @@ lteReflection 0 b = RTrue LTEZero
 lteReflection (S k) 0 = RFalse \sk_lte_z => absurd sk_lte_z
 lteReflection (S a) (S b) = LTESuccInjectiveMonotone a b (lteReflection a b)
 
+export
+ltReflection : (a, b : Nat) -> Reflects (a `LT` b) (a `lt` b)
+ltReflection a = lteReflection (S a)
+
 -- For example:
 export
 lteIsLTE : (a, b : Nat) -> a `lte` b = True -> a `LTE` b
 lteIsLTE  a b prf = invert (replace {p = Reflects (a `LTE` b)} prf (lteReflection a b))
 
+export
+notlteIsNotLTE : (a, b : Nat) -> a `lte` b = False -> Not (a `LTE` b)
+notlteIsNotLTE a b prf = invert (replace {p = Reflects (a `LTE` b)} prf (lteReflection a b))
+
+
 export
 notlteIsLT : (a, b : Nat) -> a `lte` b = False -> b `LT` a
 notlteIsLT a b prf = notLTImpliesGTE
@@ -37,6 +46,10 @@ notlteIsLT a b prf = notLTImpliesGTE
                          (invert $ replace {p = Reflects (S a `LTE` S b)} prf
                                  $ lteReflection (S a) (S b)) prf'
 
+export
+notltIsGTE : (a, b : Nat) -> (a `lt` b) === False -> a `GTE` b
+notltIsGTE a b p = notLTImpliesGTE (notlteIsNotLTE (S a) b p)
+
 
 -- The converse to lteIsLTE:
 export

libs/contrib/Data/OpenUnion.idr

@@ -0,0 +1,90 @@
+||| This module is inspired by the open union used in the paper
+||| Freer Monads, More Extensible Effects
+||| by Oleg Kiselyov and Hiromi Ishii
+|||
+||| By using an AtIndex proof, we are able to get rid of all of the unsafe
+||| coercions in the original module.
+
+module Data.OpenUnion
+
+import Data.DPair
+import Data.List.AtIndex
+import Data.List.HasLength
+import Data.Nat
+import Data.Nat.Order.Properties
+import Decidable.Equality
+import Syntax.WithProof
+
+%default total
+
+||| An open union of families is an index picking a family out together with
+||| a value in the family thus picked.
+public export
+data Union : (ts : List (a -> Type)) -> a -> Type where
+  Element : (k : Nat) -> (0 _ : AtIndex t ts k) -> t v -> Union ts v
+
+||| An empty open union of families is empty
+public export
+Uninhabited (Union [] v) where uninhabited (Element _ p _) = void (uninhabited p)
+
+
+||| Injecting a value into an open union, provided we know the index of
+||| the appropriate type family.
+inj' : (k : Nat) -> (0 _ : AtIndex t ts k) -> t v -> Union ts v
+inj' = Element
+
+||| Projecting out of an open union, provided we know the index of the
+||| appropriate type family. This may obviously fail if the value stored
+||| actually corresponds to another family.
+prj' : (k : Nat) -> (0 _ : AtIndex t ts k) -> Union ts v -> Maybe (t v)
+prj' k p (Element k' q t) with (decEq k  k')
+  prj' k p (Element k q t) | Yes Refl = rewrite atIndexUnique p q in Just t
+  prj' k p (Element k' q t) | No neq = Nothing
+
+||| Given that equality of type families is not decidable, we have to rely on
+||| the interface `FindElement` to automatically find the index of a given family.
+public export
+interface FindElement t ts => Member (0 t : a -> Type) (0 ts : List (a -> Type)) where
+
+  inj : t v -> Union ts v
+  inj = let (Element n p) = findElement in inj' n p
+
+  prj : Union ts v -> Maybe (t v)
+  prj = let (Element n p) = findElement in prj' n p
+
+||| By doing a bit of arithmetic we can figure out whether the union's value came from
+||| the left or the right list used in the index.
+public export
+split : Subset Nat (HasLength ss) -> Union (ss ++ ts) v -> Either (Union ss v) (Union ts v)
+split m (Element n p t) with (@@ lt n (fst m))
+  split m (Element n p t) | (True ** lt) = Left (Element n (strengthenL m lt p) t)
+  split m (Element n p t) | (False ** notlt) =
+     let 0 lte : lte (fst m) n === True = LteIslte (fst m) n (notltIsGTE n (fst m) notlt)
+     in Right (Element (minus n (fst m)) (strengthenR m lte p) t)
+
+||| We can inspect an open union over a non-empty list of families to check
+||| whether the value it contains belongs either to the first family or any
+||| other in the tail.
+public export
+decomp : Union (t :: ts) v -> Either (Union ts v) (t v)
+decomp (Element 0     (Z)   t) = Right t
+decomp (Element (S n) (S p) t) = Left (Element n p t)
+
+||| An open union over a singleton list is just a wrapper over values of that family
+public export
+decomp0 : Union [t] v -> t v
+decomp0 elt = case decomp elt of
+  Left t => absurd t
+  Right t => t
+
+||| Inserting new families at the end of the list leaves the index unchanged.
+public export
+weakenR : Union ts v -> Union (ts ++ us) v
+weakenR (Element n p t) = Element n (weakenR p) t
+
+||| If we introduce them at the beginning however, we need to shift the index by
+||| the number of families we have introduced. Note that this number is the only
+||| thing we need to keep around at runtime.
+public export
+weakenL : Subset Nat (HasLength ss) -> Union ts v -> Union (ss ++ ts) v
+weakenL m (Element n p t) = Element (fst m + n) (weakenL m p) t

libs/contrib/contrib.ipkg

@@ -9,7 +9,6 @@ modules = Control.ANSI,
           Control.Linear.LIO,
 
           Control.Monad.Algebra,
-          Control.Monad.Syntax,
 
           Control.Algebra,
           Control.Algebra.Laws,
@@ -44,6 +43,8 @@ modules = Control.ANSI,
           Data.List.Lazy,
           Data.List.Views.Extra,
           Data.List.Palindrome,
+          Data.List.HasLength,
+          Data.List.AtIndex,
 
           Data.Logic.Propositional,
 
@@ -60,6 +61,8 @@ modules = Control.ANSI,
           Data.Nat.Order.Properties,
           Data.Nat.Properties,
 
+          Data.OpenUnion,
+
           Data.Recursion.Free,
 
           Data.SortedMap,

libs/prelude/Prelude/Interfaces.idr

@@ -176,10 +176,26 @@ interface Applicative m => Monad m where
 
 %allow_overloads (>>=)
 
+||| Right-to-left monadic bind, flipped version of `>>=`.
+public export
+(=<<) : Monad m => (a -> m b) -> m a -> m b
+(=<<) = flip (>>=)
+
+||| Sequencing of effectful composition
 public export
 (>>) : (Monad m) => m a -> m b -> m b
 a >> b = a >>= \_ => b
 
+||| Left-to-right Kleisli composition of monads.
+public export
+(>=>) : Monad m => (a -> m b) -> (b -> m c) -> (a -> m c)
+(>=>) f g = \x => f x >>= g
+
+||| Right-to-left Kleisli composition of monads, flipped version of `>=>`.
+public export
+(<=<) : Monad m => (b -> m c) -> (a -> m b) -> (a -> m c)
+(<=<) = flip (>=>)
+
 ||| `guard a` is `pure ()` if `a` is `True` and `empty` if `a` is `False`.
 public export
 guard : Alternative f => Bool -> f ()

libs/prelude/Prelude/Ops.idr

@@ -14,7 +14,7 @@ infixr 4 ||
 infixr 7 ::, ++
 
 -- Functor/Applicative/Monad/Algebra operators
-infixl 1 >>=, >>
+infixl 1 >>=, =<<, >>, >=>, <=<
 infixr 2 <|>
 infixl 3 <*>, *>, <*
 infixr 4 <$>, $>, <$