commit 37ebb0a47f875b1bbd792aaca9dd0becff683c00
parent 1149fa76f683442b27d12b822661b1043fe8317b
Author: Robert Russell <robert@rr3.xyz>
Date: Sun, 1 Jun 2025 21:19:16 -0700
Add stuff from experiments
Uhhgggg! I think I'm giving up on this project for now. The scope
has grown to creating a Haskell base alternative that puts laziness
and strictness on an equal footing, but that is not possible in an
ergonomic way without something like 2LTT.
Diffstat:
| M | package.yaml | | | 52 | +++++++++++++++++++++++++++++----------------------- |
| M | src/Lude.hs | | | 436 | ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++------- |
2 files changed, 430 insertions(+), 58 deletions(-)
diff --git a/package.yaml b/package.yaml
@@ -4,32 +4,38 @@ author: "Robert Russell"
license: ISC
ghc-options:
- - -Wall
- - -Wno-name-shadowing
- - -Wno-missing-signatures
+ - -Wall
+ - -Wno-name-shadowing
+ - -Wno-missing-signatures
+ - -Wno-unused-top-binds
+ - -fprint-explicit-foralls
+ - -fprint-explicit-kinds
+ - -fprint-explicit-runtime-reps
+
+language: GHC2021
default-extensions:
- - NoImplicitPrelude
- - BangPatterns
- - TypeFamilies
- - TypeOperators
-#- DuplicateRecordFields
-#- NoFieldSelectors
-#- OverloadedRecordDot
-#- BlockArguments
-#- LambdaCase
-#- MultiWayIf
-#- OverloadedStrings
-#- ScopedTypeVariables
-#- FlexibleInstances
-#- MultiParamTypeClasses
-#- UndecidableInstances
+ - BlockArguments
+ - DataKinds
+ - DefaultSignatures
+ - FunctionalDependencies
+ - GADTs
+ - LambdaCase
+ - MagicHash
+ - NoImplicitPrelude
+ - PatternSynonyms
+ - TypeData
+ - TypeFamilies
+ - UnboxedTuples
+ - UnicodeSyntax
+ - UnliftedNewtypes
+ - UnliftedDatatypes
dependencies:
- - base
- - bytestring
- - text
- - mtl
+ - base
+ #- bytestring
+ #- text
+ #- mtl
library:
- source-dirs: src
+ source-dirs: src
diff --git a/src/Lude.hs b/src/Lude.hs
@@ -1,20 +1,40 @@
module Lude (
+ -- Types,
+ Constraint,
+ Levity (..),
+ RuntimeRep (..),
+ Thunked,
+ LRep,
+ URep,
+ Type,
+ BoxedType,
+ LType,
+ UType,
+ Kind,
+ Unlift (..),
-- Function
const,
fix,
flip,
- ($),
- ($!),
- (&),
- (&!),
+ -- ($),
+ -- ($!),
+ -- (&),
+ -- (&!),
+ -- Bool
+ IsBool (..),
+ Bool (..),
+ (&&),
+ (||),
+ not,
-- Category
- Category ((.)),
- identity,
- (<<),
- (>>),
+ -- Category (identity, compose),
+ -- (<.),
+ -- (.>),
-- Functor
+ {-
Functor,
void,
+ Compose (Compose, getCompose),
Const (Const, getConst),
Identity (Identity, runIdentity),
map,
@@ -52,19 +72,61 @@ module Lude (
(^$!^),
plug',
(^&!^),
+ -}
) where
-import Control.Applicative (Applicative (liftA2, pure, (<*>)), (<**>))
-import Control.Category (Category (id, (.)))
+import Control.Applicative (Alternative (empty, (<|>)), Applicative (liftA2, pure, (<*>)), (<**>))
import Control.Monad (Monad ((>>=)))
+import Data.Bool (Bool (..), not, (&&), (||))
import Data.Foldable (Foldable)
import Data.Function (const, fix, flip)
import Data.Functor (Functor (fmap), void)
+import Data.Functor.Compose (Compose (Compose, getCompose))
import Data.Functor.Const (Const (Const, getConst))
import Data.Functor.Identity (Identity (Identity, runIdentity))
-import Data.Maybe (Maybe)
+import Data.Maybe (Maybe (..))
import Data.Traversable (Traversable (sequenceA))
+-- TODO: SIMD: VecCount (..) and VecElem (..)
+import GHC.Exts (Constraint, Levity (..), RuntimeRep (..))
+import GHC.Exts qualified as GHC
+
+infixl 8 ∙
+type (∙) f a = f a
+
+--------------------------------------------------------------------------------
+-- Types
+
+-- | An alias for the empty constraint.
+--
+-- Used to declare unlifted values at the top-level. For example, for any @r@
+-- and @A :: Type r@:
+-- @
+-- a :: Thunked => A
+-- a = ...
+-- @
+type Thunked = () :: Constraint
+
+type LRep = BoxedRep Lifted
+type URep = BoxedRep Unlifted
+
+type Type = GHC.TYPE
+type BoxedType l = Type (BoxedRep l)
+type LType = BoxedType Lifted
+type UType = BoxedType Unlifted
+
+-- | An alias for `LType`.
+type Kind = LType
+
+-- | Types with an unlifted alternative.
+--
+-- Laws:
+-- - @force (lift x) = x@
+class Unlift a where
+ type U a :: UType
+ force :: a -> U a
+ lift :: U a -> a
+
--------------------------------------------------------------------------------
-- Function
@@ -90,36 +152,275 @@ x & f = f x
!x &! f = f x
--------------------------------------------------------------------------------
--- Category
+-- Bool
-infixr 2 <<, >>
+class IsBool (bool :: Type r) where
+ true :: (Thunked) => bool
+ false :: (Thunked) => bool
+ bool :: a -> a -> bool -> a
--- | The identity morphism.
---
--- This is just a renamed version of @Control.Category.id@.
-identity :: (Category v) => v a a
-identity = id
+instance IsBool Bool where
+ true = True
+ false = False
+ bool t f = \case
+ True -> t
+ False -> f
+
+data UBool :: UType where
+ UTrue :: UBool
+ UFalse :: UBool
+
+instance IsBool UBool where
+ true = UTrue
+ false = UFalse
+ bool t f = \case
+ UTrue -> t
+ UFalse -> f
+
+instance Unlift Bool where
+ type U Bool = UBool
+
+ force True = UTrue
+ force False = UFalse
+
+ lift UTrue = True
+ lift UFalse = False
+
+--------------------------------------------------------------------------------
+-- Maybe
+
+class IsMaybe (maybe :: Type s -> Type r) where
+ just :: a -> maybe a
+ nothing :: (Thunked) => maybe a
+ maybe :: b -> (a -> b) -> maybe a -> b
+
+instance IsMaybe Maybe where
+ just = Just
+ nothing = Nothing
+ maybe n j = \case
+ Just a -> j a
+ Nothing -> n
+
+data UMaybe :: LType -> UType where
+ UJust :: a -> UMaybe a
+ UNothing :: UMaybe a
+
+instance IsMaybe UMaybe where
+ just = UJust
+ nothing = UNothing
+ maybe n j = \case
+ UJust a -> j a
+ UNothing -> n
+
+instance Unlift (Maybe a) where
+ type U (Maybe a) = UMaybe a
+
+ force (Just a) = UJust a
+ force Nothing = UNothing
+
+ lift (UJust a) = Just a
+ lift UNothing = Nothing
+
+data Maybe' :: UType -> LType where
+ Just' :: a -> Maybe' a
+ Nothing' :: Maybe' a
+
+instance IsMaybe Maybe' where
+ just = Just'
+ nothing = Nothing'
+ maybe n j = \case
+ Just' a -> j a
+ Nothing' -> n
+
+data UMaybe' :: UType -> UType where
+ UJust' :: a -> UMaybe' a
+ UNothing' :: UMaybe' a
+
+instance IsMaybe UMaybe' where
+ just = UJust'
+ nothing = UNothing'
+ maybe n j = \case
+ UJust' a -> j a
+ UNothing' -> n
+
+instance Unlift (Maybe' a) where
+ type U (Maybe' a) = UMaybe' a
+
+ force (Just' a) = UJust' a
+ force Nothing' = UNothing'
+
+ lift (UJust' a) = Just' a
+ lift UNothing' = Nothing'
+
+isJust :: forall s r (maybe :: Type s -> Type r) a. (IsMaybe maybe) => maybe a -> Bool
+isJust = maybe False (const True)
+
+isNothing :: (IsMaybe maybe) => maybe a -> Bool
+isNothing = maybe True (const False)
+
+-- type family Maybe# (r :: RuntimeRep) (l :: Levity) :: Type r -> BoxedType l
+-- type instance Maybe# LRep Lifted = Maybe
+-- type instance Maybe# URep Lifted = Maybe'
+-- type instance Maybe# LRep Unlifted = UMaybe
+-- type instance Maybe# URep Unlifted = UMaybe'
+
+-- type family Lower (a :: Kind) :: Kind where
+-- Lower (BoxedType l) = TypeU
+-- Lower (k -> l) = k -> Lower l
+-- type family X (a :: k) :: Lower k
+-- type instance X (MaybeL @l) = MaybeL @Unlifted
+
+--------------------------------------------------------------------------------
+-- Numeric types
+
+-- TODO
+
+--------------------------------------------------------------------------------
+-- Category
+
+-- infixr 9 ∘
+
+-- infixr 2 <.
+-- infixl 2 .>
+
+-- (⊲⊳)
+-- (⋖⋗)
+-- (⩹⩺)
+-- (⨟)
+-- (⦂)
+-- (⋄)
+-- (∧∨)
+-- (⩓⩔)
+-- (∩∪)
+-- (=≠≡≢≈≉)
+-- (<>≤≥≮≯≰≱)
+-- (≺≻≼≽⊀⊁⋠⋡)
+-- (⊂⊃⊆⊇⊄⊅⊈⊉)
+-- (⊏⊐⊑⊒)
+-- (⊢⊣⊤⊥)
+-- y = h ∘ g ∘ f ∙^ x
+-- (f ⦾ g ⦿ x)
+-- y = h ◁ g ◁ f ◀ x
+-- y = x ▶ f ▷ g ▷ h
+-- (⧑⧒⧓⧔⧕⧖⧗⋈⋉⋊)
+-- (↑↓↔↕↖↗↘↙)
+-- (⥼⥽⥾⥿)
+-- (⊰⊱)
+-- (⭘∘)
+-- (⦁∙⋅)
+-- (⊙)
+-- (⊚)
+-- (⬬⬭⬮⬯)
+-- (⬝⬞)
+-- (⋆)
+-- (⬥⬦⬧⬨⬩⬪⬫)
+-- (◖◗)
+-- (◐◑)
+-- (⫾)
+-- (■▪▬▮▰▲▶▼◀◆)
+-- (∙⋆⋄*≀⌑▫)
+-- y = x ▪ f ▫ g ▫ h
+-- y = x ⦂ f ⨟ g ⨟ h
+
+-- TODO: Op, Products, Sums, Clown, Joker
+
+{-
+
+class Category (mor :: obj -> obj -> TypeL) where
+ -- If we make morphisms representation-polymorphic, we must modify identity:
+ -- {-# MINIMAL (identity | identityU), compose #-}
+ -- identity :: (ρ ~ LRep) => mor a a
+ -- identity = force identityU
+ -- identityU :: Thunk (mor a a)
+ -- default identityU :: (ρ ~ LRep) => Thunk (mor a a)
+ -- identityU () = identity
+ identity :: mor a a
+ compose :: mor b c -> mor a b -> mor a c
+
+class (Category (DomOf f)) => Functor (f :: domObj -> Type ρ) where
+ type DomOf f :: domObj -> domObj -> TypeL
+ map :: DomOf f a b -> (f a -> f b)
+
+class (Category (LDomOf f)) => LFunctor (f :: lDomObj -> k -> Type ρ) where
+ type LDomOf f :: lDomObj -> lDomObj -> TypeL
+
+ mapl :: LDomOf f a b -> (f a c -> f b c)
+ default mapl :: (Bifunctor f) => LDomOf f a b -> (f a c -> f b c)
+ mapl = flip bimap identity
+
+class (Category (RDomOf f)) => RFunctor (f :: k -> rDomObj -> Type ρ) where
+ type RDomOf f :: rDomObj -> rDomObj -> TypeL
+
+ mapr :: RDomOf f a b -> (f c a -> f c b)
+ default mapr :: (Bifunctor f) => RDomOf f a b -> (f c a -> f c b)
+ mapr = bimap identity
+
+class (LFunctor f, RFunctor f, Category (Hask ρ)) => Bifunctor (f :: lDomObj -> rDomObj -> Type ρ) where
+ bimap :: LDomOf f a b -> RDomOf f c d -> (f a c -> f b d)
+ bimap f g = mapl f ∘ mapr g
+
+type Iso (mor :: obj -> obj -> TypeL) a b = (mor a b, mor b a) -- TODO: use strict pair
+
+class (Bifunctor f, LDomOf f ~ Hask ρ, RDomOf f ~ Hask ρ) => Monoidal (f :: Type ρ -> Type ρ -> Type ρ) where
+ type UnitOf f :: Type ρ
+ unitl :: Iso (Hask ρ) (f (UnitOf f) a) a
+ unitr :: Iso (Hask ρ) (f a (UnitOf f)) a
+ assoc :: Iso (Hask ρ) (f (f a b) c) (f a (f b c))
+
+-- TODO: Having this only work for Hask sucks and is needlessly specialized.
+-- We can generalize this and some above definitions to any category whose
+-- objects have kind Type ρ, which isn't just Hask (e.g., Kleisli).
+class (Monoidal f) => Cartesian (f :: Type ρ -> Type ρ -> Type ρ) where
+ fst :: forall (a :: Type ρ) (b :: Type ρ). f a b -> a
+ snd :: forall (a :: Type ρ) (b :: Type ρ). f a b -> b
+
+ pair :: forall (a :: Type ρ) (b :: Type ρ) (c :: Type ρ). (a -> b) -> (a -> c) -> a -> f b c
+ pair f g = bimap f g ∘ diag
+
+ diag :: forall (a :: Type ρ). a -> f a a
+ diag = pair identity identity
+
+type Hask ρ = (->) :: Type ρ -> Type ρ -> TypeL
+
+instance Category (Hask RepL) where
+ identity x = x
+ compose f g x = f (g x)
+
+(∘) :: (Category mor) => mor b c -> mor a b -> mor a c
+(∘) = compose
+
+-}
-- | Right-to-left composition.
--
-- This operator is right associative to exploit laziness in the case where
-- the outer function doesn't need its argument:
--
--- > (const x << (f << g)) y ---> const x ((f << g) y) ---> x
+-- > (const x <. (f <. g)) y ---> const x ((f <. g) y) ---> x
--
--- Note that @f << g@ is never evaluated.
-(<<) :: (Category v) => v b c -> v a b -> v a c
-(<<) = (.)
+-- Note that @f <. g@ is never evaluated.
+-- (<.) :: (Category v) => v b c -> v a b -> v a c
+-- (<.) = (.)
-- | Left-to-right composition.
-(>>) :: (Category v) => v a b -> v b c -> v a c
-(>>) = flip (.)
+--
+-- This operator is left associative to exploit laziness in the case where
+-- the outer function doesn't need its argument:
+--
+-- > ((g .> f) .> const x) y ---> const x ((g .> f) y) ---> x
+--
+-- Note that @g .> f@ is never evaluated.
+-- (.>) :: (Category v) => v a b -> v b c -> v a c
+-- (.>) = flip (.)
+
+-- TODO: (.:), (<.:), (.:>)
--------------------------------------------------------------------------------
-- Functor
-infixl 0 ^&, &^
-infixl 1 $^, ^$
+{-
+infixl 0 ^&, &^, ~^&, ^&~, ~&^, &^~
+infixl 1 $^, ^$, $^~, ~$^, ^$~, ~^$
infixr 2 <<^, ^>>, ^<<, >>^
-- | The action of a functor on a function.
@@ -130,7 +431,7 @@ map = fmap
-- | The action of a functor on a function, flipped.
--
-- With the BlockArguments extension, expressions like "@for xs \\x -> ...@"
--- look like imperative for-loops, hence the name "for".
+-- look like for-loops, hence the name "for".
for, (^&) :: (Functor f) => f a -> (a -> b) -> f b
for = flip map
(^&) = for
@@ -145,31 +446,89 @@ flor, (&^) :: (Functor f) => a -> f (a -> b) -> f b
flor = flip flap
(&^) = flor
+($^~) :: (Functor f, Functor g) => (a -> b) -> g (f a) -> g (f b)
+f $^~ a = (f $^) $^ a
+
+(~^&) :: (Functor f, Functor g) => g (f a) -> (a -> b) -> g (f b)
+(~^&) = flip ($^~)
+
+(~$^) :: (Functor f, Functor g) => g (a -> b) -> f a -> g (f b)
+f ~$^ a = f ^& ($^ a)
+
+(^&~) :: (Functor f, Functor g) => f a -> g (a -> b) -> g (f b)
+(^&~) = flip (~$^)
+
+(^$~) :: (Functor f, Functor g) => f (a -> b) -> g a -> g (f b)
+f ^$~ a = (f ^$) $^ a
+
+(~&^) :: (Functor f, Functor g) => g a -> f (a -> b) -> g (f b)
+(~&^) = flip (^$~)
+
+(~^$) :: (Functor f, Functor g) => g (f (a -> b)) -> a -> g (f b)
+f ~^$ a = f ^& (^$ a)
+
+(&^~) :: (Functor f, Functor g) => a -> g (f (a -> b)) -> g (f b)
+(&^~) = flip (~^$)
+
+-- TODO
+
-- | Right-to-left composition with the first function in a functor.
(<<^) :: (Functor f, Category v) => v b c -> f (v a b) -> f (v a c)
-g <<^ f = (g <<) $^ f
+g <<^ f = (g <.) $^ f
+
+-- TODO
-- | Left-to-right composition with the first function in a functor.
(^>>) :: (Functor f, Category v) => f (v a b) -> v b c -> f (v a c)
-f ^>> g = f ^& (>> g)
+f ^>> g = f ^& (.> g)
+
+-- TODO
-- | Right-to-left composition with the second function in a functor.
(^<<) :: (Functor f, Category v) => f (v b c) -> v a b -> f (v a c)
-g ^<< f = g ^& (<< f)
+g ^<< f = g ^& (<. f)
+
+-- TODO
-- | Left-to-right composition with the second function in a functor.
(>>^) :: (Functor f, Category v) => v a b -> f (v b c) -> f (v a c)
-f >>^ g = (f >>) $^ g
+f >>^ g = (f .>) $^ g
-- TODO: *^, ^*
--------------------------------------------------------------------------------
-- Applicative
-infixl 0 ^&^
-infixl 1 ^$^
+infixl 0 ^&^, ~^&^~
+infixl 1 ^$^, ~^$^~
infixr 2 ^<<^, ^>>^
+-- | Functions with applicative effects.
+newtype Appy f a b = Appy {runAppy :: f (a -> b)}
+
+instance (Functor f) => Functor (Appy f a) where
+ fmap f (Appy a) = Appy (f $^~ a)
+
+instance (Applicative f) => Applicative (Appy f a) where
+ pure = Appy . pure . const
+ Appy f <*> Appy a = Appy (f ~^$^~ a)
+
+hom :: (a -> b) -> (b -> b -> c) -> a -> a -> c
+hom f g x y = g (f x) (f y)
+
+instance (Alternative f) => Alternative (Appy f a) where
+ empty = Appy empty
+
+-- Appy x <|> Appy y = Appy (x <|> y)
+-- (<|>) = hom runAppy (<|>)
+
+instance (Applicative f) => Category (Appy f) where
+ id = Appy (pure id)
+ Appy f . Appy g = Appy ((.) $^ f ^$^ g)
+
+-- TODO: Remove ap and plug?
+-- TODO: liftA{,1,2,3,4}
+
-- | An alias for @pure ()@.
pass :: (Applicative f) => f ()
pass = pure ()
@@ -185,13 +544,19 @@ plug, (^&^) :: (Applicative f) => f a -> f (a -> b) -> f b
plug = (<**>)
(^&^) = plug
+(~^$^~) :: (Applicative f, Applicative g) => g (f (a -> b)) -> g (f a) -> g (f b)
+f ~^$^~ a = (^$^) $^ f ^$^ a
+
+(~^&^~) :: (Applicative f, Applicative g) => g (f a) -> g (f (a -> b)) -> g (f b)
+f ~^&^~ a = (^&^) $^ f ^$^ a
+
-- TODO: document
(^<<^) :: (Applicative f, Category v) => f (v b c) -> f (v a b) -> f (v a c)
-(^<<^) = liftA2 (<<)
+(^<<^) = liftA2 (<.)
-- TODO: document
(^>>^) :: (Applicative f, Category v) => f (v a b) -> f (v b c) -> f (v a c)
-(^>>^) = liftA2 (>>)
+(^>>^) = liftA2 (.>)
-- TODO: "semicolons"
@@ -230,3 +595,4 @@ plug' mx mf = do
f <- mf
pure $! f x
(^&!^) = plug'
+-}
