Move refinement and singleton types into modules

Author: brendanzab

experiments/idris/fathom.ipkg

@@ -15,6 +15,8 @@ package fathom
 -- modules to install
 modules = Fathom
         , Fathom.Base
+        , Fathom.Data.Sing
+        , Fathom.Data.Refine
         , Fathom.Closed.IndexedInductive
         , Fathom.Closed.InductiveRecursive
         , Fathom.Closed.InductiveRecursiveCustom

experiments/idris/src/Fathom/Base.idr

@@ -5,50 +5,6 @@ import Data.Colist
 import Data.List
 
 
-------------------
--- USEFUL TYPES --
-------------------
-
-
-||| A value that is refined by a proposition.
-|||
-||| This is a bit like `(x : A ** B)`, but with the second element erased.
-public export
-record Refine (0 A : Type) (0 P : A -> Type) where
-  constructor MkRefine
-  ||| The wrapped value
-  value : A
-  ||| The proof of the proposition
-  {auto 0 prf : P value}
-
-||| Refine a value with a proposition
-public export
-refine : {0 A : Type} -> {0 P : A -> Type} -> (value : A) -> {auto 0 prf : P value} -> Refine A P
-refine value = MkRefine { value }
-
-
-||| Singleton types
-|||
-||| Inspired by [this type](https://agda.readthedocs.io/en/v2.5.4.1/language/with-abstraction.html#the-inspect-idiom)
-||| from the Agda docs.
-public export
-record Sing {0 A : Type} (x : A) where
-  constructor MkSing
-  0 value : A
-  {auto 0 prf : x = value}
-
-
-||| Convert a singleton back to its underlying value
-public export
-sing : {0 A : Type} -> {0 x : A} -> (0 value : A) -> {auto 0 prf : x = value} -> Sing x
-sing value = MkSing { value }
-
-||| Convert a singleton back to its underlying value
-public export
-value : {0 Val : Type} -> {x : Val} -> Sing x -> Val
-value (MkSing _) = x
-
-
 ---------------------------
 -- ENCODER/DECODER PAIRS --
 ---------------------------

experiments/idris/src/Fathom/Closed/IndexedInductive.idr

@@ -8,6 +8,7 @@ import Data.Colist
 import Data.Vect
 
 import Fathom.Base
+import Fathom.Data.Sing
 
 
 -------------------------
@@ -37,7 +38,7 @@ decode End [] = Just ((), [])
 decode End (_::_) = Nothing
 decode Fail _ = Nothing
 decode (Pure x) buffer =
-  Just (sing x, buffer)
+  Just (MkSing x, buffer)
 decode (Skip f _) buffer = do
   (x, buffer') <- decode f buffer
   Just ((), buffer')

experiments/idris/src/Fathom/Closed/InductiveRecursive.idr

@@ -26,6 +26,8 @@ import Data.Colist
 import Data.Vect
 
 import Fathom.Base
+import Fathom.Data.Sing
+import Fathom.Data.Refine
 
 -- import Fathom.Open.Record
 
@@ -87,7 +89,7 @@ decode End [] = Just ((), [])
 decode End (_::_) = Nothing
 decode Fail _ = Nothing
 decode (Pure x) buffer =
-  Just (sing x, buffer)
+  Just (MkSing x, buffer)
 decode (Skip f _) buffer = do
   (x, buffer') <- decode f buffer
   Just ((), buffer')
@@ -150,25 +152,25 @@ FormatOf rep = Refine Format (\f => Rep f = rep)
 
 
 toFormatOf : (f : Format) -> FormatOf (Rep f)
-toFormatOf f = refine f
+toFormatOf f = MkRefine f
 
 
 export
 either : (cond : Bool) -> (f1 : Format) -> (f2 : Format) -> FormatOf (if cond then Rep f1 else Rep f2)
-either True f1 _ = refine f1
-either False _ f2 = refine f2
+either True f1 _ = MkRefine f1
+either False _ f2 = MkRefine f2
 
 
 export
 orPure : (cond : Bool) -> FormatOf a -> (def : a) -> FormatOf (if cond then a else Sing def)
 orPure True f _ = f
-orPure False _ def = refine (Pure def)
+orPure False _ def = MkRefine (Pure def)
 
 
 export
 orPure' : (cond : Bool) -> FormatOf a -> (def : a) -> FormatOf (if cond then a else Sing def)
 orPure' True f _ = f
-orPure' False _ def = refine (Pure def)
+orPure' False _ def = MkRefine (Pure def)
 
 
 foo : (cond : Bool) -> (f : Format) -> Rep f -> Format

experiments/idris/src/Fathom/Closed/InductiveRecursiveCustom.idr

@@ -8,6 +8,8 @@ import Data.Colist
 import Data.Vect
 
 import Fathom.Base
+import Fathom.Data.Sing
+import Fathom.Data.Refine
 
 
 -------------------------
@@ -64,7 +66,7 @@ decode End [] = Just ((), [])
 decode End (_::_) = Nothing
 decode Fail _ = Nothing
 decode (Pure x) buffer =
-  Just (sing x, buffer)
+  Just (MkSing x, buffer)
 decode (Skip f _) buffer = do
   (x, buffer') <- decode f buffer
   Just ((), buffer')
@@ -127,25 +129,25 @@ FormatOf rep = Refine Format (\f => Rep f = rep)
 
 
 toFormatOf : (f : Format) -> FormatOf (Rep f)
-toFormatOf f = refine f
+toFormatOf f = MkRefine f
 
 
 export
 either : (cond : Bool) -> (f1 : Format) -> (f2 : Format) -> FormatOf (if cond then Rep f1 else Rep f2)
-either True f1 _ = refine f1
-either False _ f2 = refine f2
+either True f1 _ = MkRefine f1
+either False _ f2 = MkRefine f2
 
 
 export
 orPure : (cond : Bool) -> FormatOf a -> (def : a) -> FormatOf (if cond then a else Sing def)
 orPure True f _ = f
-orPure False _ def = refine (Pure def)
+orPure False _ def = MkRefine (Pure def)
 
 
 export
 orPure' : (cond : Bool) -> FormatOf a -> (def : a) -> FormatOf (if cond then a else Sing def)
 orPure' True f _ = f
-orPure' False _ def = refine (Pure def)
+orPure' False _ def = MkRefine (Pure def)
 
 
 foo : (cond : Bool) -> (f : Format) -> Rep f -> Format

experiments/idris/src/Fathom/Data/Refine.idr

@@ -0,0 +1,15 @@
+module Fathom.Data.Refine
+
+
+||| A value that is refined by a proposition.
+|||
+||| The proof of the proposition is erased at runtime.
+|||
+||| This is a bit like `(x : A ** B)`, but with the second element erased.
+public export
+record Refine (0 A : Type) (0 P : A -> Type) where
+  constructor MkRefine
+  ||| The refined value
+  val : A
+  ||| The a proof that @val is refined by @P
+  {auto 0 prf : P val}

experiments/idris/src/Fathom/Data/Sing.idr

@@ -0,0 +1,23 @@
+module Fathom.Data.Sing
+
+
+||| A singleton type, constrained to be a single value
+|||
+||| The underlying value and the proof are both erased at runtime, as they can
+||| be converted back to the index by reconstructing the value as required.
+|||
+||| Inspired by the singleton type [found in Adga’s documentation](https://agda.readthedocs.io/en/v2.5.4.1/language/with-abstraction.html#the-inspect-idiom).
+public export
+record Sing {0 A : Type} (x : A) where
+  constructor MkSing
+  ||| The underlying value of the singleton (erased at run-time)
+  0 val : A
+  ||| A proof that @val is the same as the indexed value (erased at run-time)
+  {auto 0 prf : x = val}
+
+
+||| Convert a singleton back to its underlying value restoring it with a value
+||| constructed runtime
+public export
+val : {0 A : Type} -> {x : A} -> Sing x -> A
+val (MkSing _) = x

experiments/idris/src/Fathom/Open/Record.idr

@@ -15,6 +15,7 @@ import Data.Colist
 import Data.Vect
 
 import Fathom.Base
+import Fathom.Data.Sing
 
 
 public export
@@ -57,7 +58,7 @@ pure x = MkFormat { Rep, decode, encode } where
   Rep = Sing x
 
   decode : Decode Rep BitStream
-  decode buffer = Just (sing x, buffer)
+  decode buffer = Just (MkSing x, buffer)
 
   encode : Encode Rep BitStream
   encode (MkSing _) buffer = Just buffer

experiments/idris/src/Playground.idr

@@ -5,6 +5,7 @@ import Data.Colist
 import Data.Vect
 
 import Fathom.Base
+import Fathom.Data.Sing
 import Fathom.Closed.InductiveRecursive as IndRec
 import Fathom.Closed.IndexedInductive as Indexed
 import Fathom.Open.Record as Record