Implement a simpler singleton type

Author: brendanzab

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

@@ -188,13 +188,13 @@ simple_glyph =
         x => ?todo4
 
       -- repeat' : Bits8
-      -- repeat' with (MkSing flag)
-      --   repeat' | MkSing 0 {prf} = rewrite sym prf in repeat
-      --   repeat' | MkSing x {prf} = ?todo4
+      -- repeat' with (MkSingEq flag)
+      --   repeat' | MkSingEq 0 {prf} = rewrite sym prf in repeat
+      --   repeat' | MkSingEq x {prf} = ?todo4
 
       -- repeat' : Bits8
-      -- repeat' = case MkSing flag of
-      --   MkSing 0 {prf} => ?todo3
-      --   MkSing x {prf} => ?todo4
+      -- repeat' = case MkSingEq flag of
+      --   MkSingEq 0 {prf} => ?todo3
+      --   MkSingEq x {prf} => ?todo4
     in
       Pure (repeat' + 1))

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

@@ -1,23 +1,61 @@
 module Fathom.Data.Sing
 
 
-||| A singleton type, constrained to be a single value
+||| A type constrained to 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).
+||| The underlying value is erased at runtime, as it can be converted back to
+||| the index by reconstructing the value as required.
 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}
+data Sing : {0 A : Type} -> (x : A) -> Type where
+  MkSing : {0 A : Type} -> (0 x : A) -> Sing x
 
 
-||| Convert a singleton back to its underlying value restoring it with a value
-||| constructed runtime
+||| Reconstruct a singleton with a runtime value.
 public export
 val : {0 A : Type} -> {x : A} -> Sing x -> A
 val (MkSing _) = x
+
+
+||| Update the value contained in a singleton with a function.
+export
+map : {0 A, B : Type} -> {0 x : A} -> (f : A -> B) -> Sing x -> Sing (f x)
+map f (MkSing y) = MkSing (f y)
+
+
+
+namespace SingEq
+  -- NOTE: Unsure if this representation is actually needed?
+
+  ||| A type constrained to be a single value, with an associated equality proof.
+  |||
+  ||| 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 SingEq {0 A : Type} (x : A) where
+    constructor MkSingEq
+    ||| 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} -> SingEq x -> A
+  val (MkSingEq _) = x
+
+
+  ||| Update the value contained in a singleton with a function.
+  export
+  map : {0 A, B : Type} -> {0 x : A} -> (f : A -> B) -> SingEq x -> SingEq (f x)
+  map f (MkSingEq y {prf}) = MkSingEq (f y) {prf = cong f prf}
+
+
+withEq : {0 A : Type} -> {0 x : A} -> Sing x -> SingEq x
+withEq (MkSing x) = MkSingEq x
+
+withoutEq : {0 A : Type} -> {0 x : A} -> SingEq x -> Sing x
+withoutEq {x} (MkSingEq _) = MkSing x