commit 849e1773bcc55fa5b6e8352915a4db241dfa2663
parent 1017e0f6af89727bcf2306be9c9f142fde81660d
Author: Robert Russell <robert@rr3.xyz>
Date: Sun, 9 Aug 2026 13:43:26 -0700
Enable NoListTuplePuns and clean up
Diffstat:
7 files changed, 72 insertions(+), 23 deletions(-)
diff --git a/package.yaml b/package.yaml
@@ -36,6 +36,7 @@ default-extensions:
- LiberalTypeSynonyms
- MagicHash
- NoImplicitPrelude
+ - NoListTuplePuns
- OverloadedLists
- OverloadedStrings
- PartialTypeSignatures
@@ -55,6 +56,7 @@ default-extensions:
dependencies:
- base
- containers
+ - ghc-experimental
library:
source-dirs: src
diff --git a/src/Lude/Constraint.hs b/src/Lude/Constraint.hs
@@ -4,9 +4,14 @@ module Lude.Constraint (
Evidence (..),
Evidence1 (..),
--
+ Witnesses (..),
+ (:=>),
+ because,
+ (\\),
+ --
Entailment (..),
(:-),
- because,
+ pattern Duh,
--
Always,
always,
@@ -22,7 +27,6 @@ module Lude.Constraint (
) where
import Lude.Kind
-import Lude.Proxy
--------------------------------------------------------------------------------
@@ -30,19 +34,40 @@ type Evidence :: Constraint -> Type
data Evidence a = (a) => Evidence
-- TODO: Delete?
-type Evidence1 :: forall i. Constraint1 i -> Type1 i
+type Evidence1 :: forall {i}. Constraint1 i -> Type1 i
data Evidence1 p a = (p a) => Evidence1
--------------------------------------------------------------------------------
+type Witnesses :: Type -> Constraint -> Constraint
+class Witnesses a b | a -> b where
+ witness :: a -> Evidence b
+
+type (:=>) = Witnesses
+infixr 9 :=>
+
+because, (\\) :: forall a b c. (a :=> c) => ((c) => b) -> a -> b
+b `because` a = case witness a of Evidence -> b
+(\\) = because
+infixl 4 \\
+
+instance forall a. Witnesses (Evidence a) a where
+ witness e = e
+
+--------------------------------------------------------------------------------
+
type Entailment :: Constraint -> Constraint -> Type
newtype Entailment a b = Entailment ((a) => Evidence b)
type (:-) = Entailment
infixr 9 :-
-because :: (a) => ((b) => c) -> (a :- b) -> c
-c `because` Entailment Evidence = c
+pattern Duh :: forall a b. (a) => (b) => a :- b
+pattern Duh = Entailment Evidence
+{-# COMPLETE Duh #-}
+
+instance forall a b. (a) => Witnesses (a :- b) b where
+ witness (Entailment b) = b
--------------------------------------------------------------------------------
@@ -50,30 +75,30 @@ type Always :: Constraint
class Always
instance Always
-always :: a :- Always
+always :: forall a. a :- Always
always = Entailment Evidence
--------------------------------------------------------------------------------
-type Always1 :: forall i. Constraint1 i
-class Always1 a
-instance Always1 a
+type Always1 :: forall {i}. Constraint1 i
+class Always1 x
+instance Always1 x
-always1 :: a :- Always1 b
+always1 :: forall a x. a :- Always1 x
always1 = Entailment Evidence
--------------------------------------------------------------------------------
type Never :: Constraint
-class Never where contradiction :: b
+class Never where contradiction :: a
-never :: Never :- b
+never :: forall a. Never :- a
never = Entailment contradiction
--------------------------------------------------------------------------------
-type Never1 :: forall i. Constraint1 i
-class Never1 a where contradiction1 :: Proxy a -> b
+type Never1 :: forall {i}. Constraint1 i
+class Never1 x where contradiction1 :: b
-never1 :: forall a b. Never1 a :- b
-never1 @a = Entailment (contradiction1 (Proxy :: Proxy a))
+never1 :: forall x a. Never1 x :- a
+never1 @x = Entailment (contradiction1 @x)
diff --git a/src/Lude/Kind.hs b/src/Lude/Kind.hs
@@ -16,8 +16,11 @@ module Lude.Kind (
Constraint1,
--
Lev,
+ Endo,
+ BiEndo,
) where
+import Data.Tuple.Experimental qualified as GHC
import Data.Type.Equality ((:~:) (..), (:~~:) (..), type (~), type (~~))
import GHC.Exts qualified as GHC
@@ -52,11 +55,19 @@ type Constraint1 @r i = i -> Constraint @r
--------------------------------------------------------------------------------
--- | Used to declare unlifted values at the top-level. For example, for any @r@,
--- @A :: Type r@, and @bar :: A@:
+-- | Transparently box a type of any representation
+--
+-- Use `Lev` to declare unlifted values at the top-level. For example, for any
+-- @r :: Repr@, @A :: Type r@, and @bar :: A@:
-- @
-- foo :: Lev A
-- foo = bar
-- @
-type Lev :: forall r. Type @r -> Type
-type Lev a = (() :: ConstraintL) => a
+type Lev :: forall {r :: Repr}. Type @r -> Type
+type Lev a = (GHC.CTuple0 :: ConstraintL) => a
+
+type Endo :: Kind -> Kind
+type Endo k = k -> k
+
+type BiEndo :: Kind -> Kind
+type BiEndo k = k -> k -> k
diff --git a/src/Lude/List.hs b/src/Lude/List.hs
@@ -0,0 +1,7 @@
+module Lude.List (
+ List,
+) where
+
+import Prelude.Experimental (List)
+
+--------------------------------------------------------------------------------
diff --git a/src/Lude/Proxy.hs b/src/Lude/Proxy.hs
@@ -3,3 +3,5 @@ module Lude.Proxy (
) where
import Data.Proxy
+
+--------------------------------------------------------------------------------
diff --git a/src/Lude/Repr.hs b/src/Lude/Repr.hs
@@ -25,6 +25,7 @@ import GHC.Exts (Levity (..))
import GHC.Exts qualified as GHC
-- TODO: SIMD
+
-- TODO: Export patterns? (Non-exhaustive until we add SIMD support.)
--------------------------------------------------------------------------------
diff --git a/src/Lude/Void.hs b/src/Lude/Void.hs
@@ -3,13 +3,14 @@ module Lude.Void (
absurd,
) where
+import Data.Void (Void)
+
import Lude.Kind
+import Lude.Repr
-- TODO: Instances
--------------------------------------------------------------------------------
-data Void
-
-absurd :: forall r (a :: Type @r). Void -> a
+absurd :: forall (r :: Repr) (a :: Type @r). Void -> a
absurd = \case {}
