lude

commit 08d30ad2a1f9b41f8194d2eb9d985066b203cf0c
parent e2aebea409d0682ea935e85df897fe7e79de926f
Author: Robert Russell <robert@rr3.xyz>
Date:   Wed, 14 Oct 2026 16:21:28 -0700

Maybe: add tentative Repr-generic Maybe# type

Diffstat:
M
TODO.md
 | 
2
++
M
Todo/ReprGenericMaybe.hs.txt
 | 
27
+++++++++++++++++++++++++++
M
src/Lude/Maybe.hs
 | 
64
+++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++---

3 files changed, 90 insertions(+), 3 deletions(-)
diff --git a/TODO.md b/TODO.md
@@ -1,3 +1,5 @@
+- Make a stable vs. unstable/tentative distinction for all modules
+
 - Torsors
 - Integer, Natural, Rational, {Int,Nat}{8,16,32,64}
 - Flt{32,64}
diff --git a/Todo/ReprGenericMaybe.hs.txt b/Todo/ReprGenericMaybe.hs.txt
@@ -28,3 +28,30 @@ instance IsMaybe (MaybeB Repr.Lazy @Repr.BoxL) where nothing = NothingLL; just =
 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
+
+--------------------------------------------------------------------------------
+
+type Maybe# :: forall (r :: Repr). Type# r -> Type
+newtype Maybe# a = MkMaybe# {unMaybe# :: forall (s :: Repr) (b :: Type# s). Lev b -> (a -> b) -> b}
+
+-- | Laws:
+-- - @elimMaybe n _ nothing@ = @n@
+-- - @elimMaybe _ j (just x)@ = @j x@
+-- - @elimMaybe nothing just@ = @id@
+type IsMaybe :: forall {r :: Repr}. (Type# r -> Type) -> Constraint
+class IsMaybe (maybe :: Type# r -> Type) where
+    nothing :: forall (a :: Type# r). maybe a
+    just :: forall (a :: Type# r). a -> maybe a
+    elimMaybe :: forall (a :: Type# r) {s :: Repr} (b :: Type# s). Lev b -> (a -> b) -> maybe a -> b
+
+instance IsMaybe Maybe where
+    nothing = Nothing
+    just = Just
+    elimMaybe n j = \case
+        Nothing -> n
+        Just x -> j x
+
+instance forall (r :: Repr). (Functional# r) => IsMaybe (Maybe# @r) where
+    nothing = MkMaybe# \n _ -> n
+    just = lam# \x -> MkMaybe# \_ j -> j $# x
+    elimMaybe n j m = unMaybe# m n j
diff --git a/src/Lude/Maybe.hs b/src/Lude/Maybe.hs
@@ -2,25 +2,83 @@ module Lude.Maybe (
     Maybe (..),
     isJust,
     isNothing,
-    unsafe_fromJust,
+    maybe,
     (??),
+    unsafe_fromJust,
+    --
+    Maybe#,
+    nothing#,
+    just#,
+    maybe#,
+    isNothing#,
+    isJust#,
+    (??#),
 ) where
 
 import Data.Maybe (Maybe (..), isJust, isNothing)
 import Data.Maybe qualified as Base
 
+import Lude.Bool
+import Lude.Function
 import Lude.Haskell
 
 -- TODO: Versions for other reprs? Look at Todo/Lude.hs.
 
 -- TODO: Defaulting operators
 
+-- TODO: Using a `unBox# -> x` view pattern in `maybe#` triggers a GHC 9.14.1 bug. Report it.
+{-
+<no location info>: error:
+    panic! (the 'impossible' happened)
+  GHC version 9.14.1:
+	typeLevity
+  a_a1Ri
+  Call stack:
+      CallStack (from HasCallStack):
+        pprPanic, called at compiler/GHC/Core/Type.hs:2353:32 in ghc-9.14.1-ade7:GHC.Core.Type
+
+Please report this as a GHC bug:  https://www.haskell.org/ghc/reportabug
+-}
+
 --------------------------------------------------------------------------------
 
-unsafe_fromJust :: forall (a :: Type). Maybe a -> a
-unsafe_fromJust = Base.fromJust
+maybe :: forall (a :: Type) {s :: Repr} (b :: Type# s). Lev b -> (a -> b) -> Maybe a -> b
+maybe nothing just = \case
+    Nothing -> nothing
+    Just x -> just x
 
 (??) :: forall (a :: Type). Maybe a -> a -> a
 Just x ?? _ = x
 Nothing ?? x = x
 infix 1 ??
+
+unsafe_fromJust :: forall (a :: Type). Maybe a -> a
+unsafe_fromJust = Base.fromJust
+
+--------------------------------------------------------------------------------
+
+type Maybe# :: forall (r :: Repr). Type# r -> Type
+type Maybe# a = Maybe (Box a)
+
+nothing# :: forall {r :: Repr} (a :: Type# r). (Functional# r) => Maybe# a
+nothing# = Nothing
+
+just# :: forall {r :: Repr} (a :: Type# r). (Functional# r) => a -> Maybe# a
+just# = Just .# mkBox#
+
+maybe# :: forall {r :: Repr} (a :: Type# r) {s :: Repr} (b :: Type# s). (Functional# r) => Lev b -> (a -> b) -> Maybe# a -> b
+maybe# nothing just = \case
+    Nothing -> nothing
+    Just b -> just $# unBox# b
+
+isNothing# :: forall {r :: Repr} (a :: Type# r). (Functional# r) => Maybe# a -> Bool
+isNothing# = maybe# True (const False)
+
+isJust# :: forall {r :: Repr} (a :: Type# r). (Functional# r) => Maybe# a -> Bool
+isJust# = maybe# False (const True)
+
+(??#) :: forall {r :: Repr} (a :: Type# r). (Functional# r) => Maybe# a -> a -> a
+(??#) m = lam# \d -> case m of
+    Nothing -> d
+    Just b -> unBox# b
+infix 1 ??#