lude

commit 487c87633a11a97a8c3bf015051cd5f1e8e495d3
parent 3094cae6e65c32030842fef2c4ec768f8e9f0012
Author: Robert Russell <robert@rr3.xyz>
Date:   Thu, 24 Sep 2026 21:16:29 -0700

Todo: add idea related to Repr-generic types

Diffstat:
A
Todo/ReprGenericMaybe.hs.txt
 | 
30
++++++++++++++++++++++++++++++

1 file changed, 30 insertions(+), 0 deletions(-)
diff --git a/Todo/ReprGenericMaybe.hs.txt b/Todo/ReprGenericMaybe.hs.txt
@@ -0,0 +1,30 @@
+--------------------------------------------------------------------------------
+
+type TypeB :: Repr.EvalOrder -> Kind
+type TypeB eo = Type# (Repr.Box eo)
+
+type TypeL :: Kind
+type TypeL = TypeB Repr.Lazy
+
+type TypeE :: Kind
+type TypeE = TypeB Repr.Eager
+
+--------------------------------------------------------------------------------
+
+type MaybeB :: forall (eo :: Repr.EvalOrder) -> forall (r :: Repr). Type# r -> TypeB eo
+data family MaybeB
+data instance MaybeB Repr.Lazy @Repr.BoxL a = NothingLL | JustLL a
+data instance MaybeB Repr.Eager @Repr.BoxL a = NothingEL | JustEL a
+data instance MaybeB Repr.Lazy @Repr.BoxE a = NothingLE | JustLE a
+data instance MaybeB Repr.Eager @Repr.BoxE a = NothingEE | JustEE a
+
+type IsMaybe :: forall {r :: Repr} {s :: Repr}. (Type# r -> Type# s) -> Constraint
+class IsMaybe (maybe :: Type# r -> Type# s) where
+    nothing :: forall (a :: Type# r). Lev (maybe a)
+    just :: forall (a :: Type# r). a -> maybe a
+    elimMaybe :: forall {t :: Repr} (b :: Type# t) (a :: Type# r). Lev b -> (a -> b) -> (maybe a -> b)
+
+instance IsMaybe (MaybeB Repr.Lazy @Repr.BoxL) where nothing = NothingLL; just = JustLL; elimMaybe n j = \case NothingLL -> n; JustLL a -> j a
+instance IsMaybe (MaybeB Repr.Eager @Repr.BoxL) where nothing = NothingEL; just = JustEL; elimMaybe n j = \case NothingEL -> n; JustEL a -> j a
+instance IsMaybe (MaybeB Repr.Lazy @Repr.BoxE) where nothing = NothingLE; just = JustLE; elimMaybe n j = \case NothingLE -> n; JustLE a -> j a
+instance IsMaybe (MaybeB Repr.Eager @Repr.BoxE) where nothing = NothingEE; just = JustEE; elimMaybe n j = \case NothingEE -> n; JustEE a -> j a