InitialHEADmaster

1 files changed, 85 insertions, 0 deletions

diff --git a/ch15_15.5-i.hs b/ch15_15.5-i.hs
new file mode 100644
index 0000000..ac52df4
--- /dev/null
+++ b/ch15_15.5-i.hs
@@ -0,0 +1,85 @@
+{-# LANGUAGE ImportQualifiedPost #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+import Data.Constraint (Dict (Dict))
+import Data.Kind (Type)
+import Data.Singletons (Demote, Sing, SingI, SingKind, fromSing, sing)
+import Data.Singletons.Decide qualified as D
+
+data Sigma (f :: k -> Type) where
+  Sigma :: Sing a -> f a -> Sigma f
+
+withSigma :: (forall (a :: k). Sing a -> f a -> r) -> Sigma f -> r
+withSigma c (Sigma s f) = c s f
+
+toSigma :: SingI a => f a -> Sigma f
+toSigma = Sigma sing
+
+fromSigma
+  :: forall k (a :: k) (f :: k -> Type)
+   . (SingI a, D.SDecide k)
+  => Sigma f
+  -> Maybe (f a)
+fromSigma (Sigma s f) =
+  case s D.%~ sing @a of
+    D.Proved D.Refl -> Just f
+    D.Disproved _ -> Nothing
+
+class Dict1 c (f :: k -> Type) where
+  dict1 :: Sing (a :: k) -> Dict (c (f a))
+
+instance
+  ( Dict1 Eq (f :: k -> Type)
+  , D.SDecide k
+  )
+  => Eq (Sigma f)
+  where
+  Sigma sa fa == Sigma sb fb =
+    case sa D.%~ sb of
+      D.Proved D.Refl ->
+        case dict1 @_ @Eq @f sa of
+          Dict -> fa == fb
+      D.Disproved _ -> False
+
+-- Exercise 15.5-i
+-- Provide an instance of `Ord` for `Sigma` by comparing the `fs` if the
+-- singletons are equal, comparing the singletons at the term-level otherwise.
+instance
+  ( Dict1 Eq (f :: k -> Type)
+  , Dict1 Ord (f :: k -> Type)
+  , D.SDecide k
+  , Ord (Demote k)
+  , SingKind k
+  )
+  => Ord (Sigma f)
+  where
+  compare (Sigma sa fa) (Sigma sb fb) =
+    case sa D.%~ sb of
+      D.Proved D.Refl ->
+        -- Sandy passes `@Ord` as the first type application, however that
+        -- failed to compile on my PC. I had to do `@_ @Ord` instead (same
+        -- with `@Eq` above and `@Show` below). I wonder if newer versions of
+        -- GHC treat the order of type variables differently when used against
+        -- `class` functions, like `dict1` above.
+        case dict1 @_ @Ord @f sa of
+          Dict -> compare fa fb
+      D.Disproved _ -> compare (fromSing sa) (fromSing sb)
+
+instance
+  ( Dict1 Show (f :: k -> Type)
+  , Show (Demote k)
+  , SingKind k
+  )
+  => Show (Sigma f)
+  where
+  show (Sigma sa fa) =
+    case dict1 @_ @Show @f sa of
+      Dict ->
+        mconcat
+          [ "Sigma "
+          , show $ fromSing sa
+          , " ("
+          , show fa
+          , ")"
+          ]