Add idris code of strictly sorted list

Author: ngeiswei

idris/StrictlySorted.idr

@@ -0,0 +1,105 @@
+module StrictlySorted
+
+------------------------------------------------------------------
+-- Attempts to define a strictly sorted list data type (as a set
+-- implementation).
+------------------------------------------------------------------
+
+--------------------------------------------------------------------
+-- StrictlySorted using (Maybe a) as type argument to capture the
+-- first element of the list.
+--------------------------------------------------------------------
+
+data StrictlySorted : (a : Type) -> Maybe a -> Type where
+  Empty : StrictlySorted a Nothing
+  Singleton : (x : a) -> StrictlySorted a (Just x)
+  Prepend : Ord a => (x : a)
+                  -> (s : StrictlySorted a (Just y))
+                  -> (prf : (x < y) === True)
+                  -> StrictlySorted a (Just x)
+
+-- Test
+empty_ssl : StrictlySorted Int Nothing
+empty_ssl = Empty
+
+singleton_ssl : StrictlySorted Int (Just 10)
+singleton_ssl = Singleton 10
+
+pair_ssl : StrictlySorted Int (Just 5)
+pair_ssl = Prepend 5 (Singleton 10) Refl
+
+-- Fails due to 42 not being less than 10
+-- ill_ssl : StrictlySorted Int (Just 42)
+-- ill_ssl = Prepend 42 (Singleton 10) Refl
+
+------------------------------------------------------------------------
+-- Alternative implementation of StrictlySorted not using (Maybe a) in
+-- the type declaration.  Not as elegant to define, but easier to use.
+-- Note that (Maybe a) is still used in ssh (short for strictly sorted
+-- head).  It works because (Just x) < Nothing is evaluated to False.
+------------------------------------------------------------------------
+
+-- Pre-declaration to avoid circular dependencies
+data StrictlySorted' : Type -> Type
+0 ssh : StrictlySorted' a -> Maybe a
+
+data StrictlySorted' : (a : Type) -> Type where
+  Empty' : StrictlySorted' a
+  Singleton' : (x : a) -> StrictlySorted' a
+  Prepend' : Ord a => (x : a)
+                   -> (s : StrictlySorted' a)
+                   -> (prf : ((Just x) < ssh s) === True)
+                   -> StrictlySorted' a
+
+-- Post-implementation of ssh to avoid circular dependencies
+ssh Empty' = Nothing
+ssh (Singleton' x) = Just x
+ssh (Prepend' x _ _) = Just x
+
+-- Test
+empty_ssl' : StrictlySorted' Int
+empty_ssl' = Empty'
+
+singleton_ssl' : StrictlySorted' Int
+singleton_ssl' = Singleton' 10
+
+pair_ssl' : StrictlySorted' Int
+pair_ssl' = Prepend' 5 (Singleton' 10) Refl
+
+-- Fails due to 42 not being less than 10
+-- ill_ssl' : StrictlySorted Int (Just 42)
+-- ill_ssl' = Prepend 42 (Singleton 10) Refl
+
+--------------------------------------
+-- Alternatives from Micheal Messer
+--------------------------------------
+
+-- data StrictlySorted : Ord a -> List a -> Type where
+--     Empty : StrictlySorted o []
+--     Singleton : StrictlySorted o [x]
+--     Prepend : (v : a) -> StrictlySorted o (x :: xs) -> ((<) @{o} v x = True) -> StrictlySorted o (v :: x :: xs)
+
+-- g : Ord a => (xs : List a) -> {auto prf : StrictlySorted %search xs} -> ()
+
+-- t : ()
+-- t = g [1,2,3]
+
+---------------------------------------------
+-- Another alternative from Micheal Messer
+---------------------------------------------
+
+-- data StrictlySorted : (a : Type) -> Ord a -> Type
+-- 0 helper : a -> StrictlySorted a o -> Type
+
+-- public export
+-- data StrictlySorted : (a : Type) -> Ord a -> Type where
+--     Nil : StrictlySorted a o
+--     (::) : (v : a) -> (ls : StrictlySorted a o) -> {auto 0 prf : helper v ls} -> StrictlySorted a o
+
+-- helper v [] = ()
+-- helper v (x :: xs) = (<) @{o} v x = True
+
+-- g : Ord a => StrictlySorted a %search -> ()
+
+-- t : ()
+-- t = g [1,2,3]