Lude.hs (15460B)
1 module Lude ( 2 -- Types, 3 -- Constraint, 4 -- Levity (..), 5 -- RuntimeRep (..), 6 -- Thunked, 7 -- LRep, 8 -- URep, 9 -- Type, 10 -- BoxedType, 11 -- LType, 12 -- UType, 13 -- Kind, 14 -- Unlift (..), 15 -- Function 16 -- const, 17 -- fix, 18 -- flip, 19 -- ($), 20 -- ($!), 21 -- (&), 22 -- (&!), 23 -- Bool 24 -- IsBool (..), 25 -- Bool (..), 26 -- (&&), 27 -- (||), 28 -- not, 29 -- Category 30 -- Category (identity, compose), 31 -- (<.), 32 -- (.>), 33 -- Functor 34 {- 35 Functor, 36 void, 37 Compose (Compose, getCompose), 38 Const (Const, getConst), 39 Identity (Identity, runIdentity), 40 map, 41 ($^), 42 for, 43 (^&), 44 flap, 45 (^$), 46 flor, 47 (&^), 48 (<<^), 49 (^>>), 50 (^<<), 51 (>>^), 52 -- Applicative 53 Applicative (pure), 54 pass, 55 ap, 56 (^$^), 57 plug, 58 (^&^), 59 (^<<^), 60 (^>>^), 61 -- Monad 62 Monad, 63 map', 64 ($!^), 65 for', 66 (^&!), 67 flap', 68 (^$!), 69 flor', 70 (&!^), 71 ap', 72 (^$!^), 73 plug', 74 (^&!^), 75 -} 76 77 ) where 78 79 {- 80 81 -- import Control.Applicative (Alternative (empty, (<|>)), Applicative (liftA2, pure, (<*>)), (<**>)) 82 -- import Control.Monad (Monad ((>>=))) 83 -- import Data.Bool (Bool (..), not, (&&), (||)) 84 -- import Data.Foldable (Foldable) 85 -- import Data.Function (const, fix, flip) 86 -- import Data.Functor (Functor (fmap), void) 87 -- import Data.Functor.Compose (Compose (Compose, getCompose)) 88 -- import Data.Functor.Const (Const (Const, getConst)) 89 -- import Data.Functor.Identity (Identity (Identity, runIdentity)) 90 -- import Data.Maybe (Maybe (..)) 91 -- import Data.Traversable (Traversable (sequenceA)) 92 93 -- TODO: SIMD: VecCount (..) and VecElem (..) 94 import GHC.Exts (Constraint, Levity (..), RuntimeRep (..)) 95 import GHC.Exts qualified as GHC 96 97 -------------------------------------------------------------------------------- 98 -- Types 99 100 -- | Types with an unlifted alternative. 101 -- 102 -- Laws: 103 -- - @force (lift x) = x@ 104 class Unlift a where 105 type U a :: UType 106 force :: a -> U a 107 lift :: U a -> a 108 109 -------------------------------------------------------------------------------- 110 111 -- type Functor :: forall r s. (Type r -> Type s) -> Constraint 112 -- class Functor @r f where 113 -- map :: forall (a :: Type r) (b :: Type r). (a -> b) -> f a -> f b 114 115 -- type SemiApplicative :: forall r s. (Type r -> Type s) -> Constraint 116 -- class (Functor f) => SemiApplicative @r f where 117 -- map2 :: forall (a :: Type r) (b :: Type r) (c :: Type r). (a -> b -> c) -> f a -> f b -> f c 118 119 -- type Applicative :: forall r s. (Type r -> Type s) -> Constraint 120 -- class (SemiApplicative f) => Applicative @r f where 121 -- pure :: forall (a :: Type r). a -> f a 122 123 -- type SemiMonad :: forall r s. (Type r -> Type s) -> Constraint 124 -- class (SemiApplicative f) => SemiMonad @r f where 125 -- bind :: forall (a :: Type r) (b :: Type r). (a -> f b) -> f a -> f b 126 127 -- type Monad :: forall r s. (Type r -> Type s) -> Constraint 128 -- class (Applicative f, SemiMonad f) => Monad @r f 129 130 -- type SemiComonad :: forall r s. 131 132 -------------------------------------------------------------------------------- 133 -- Function 134 135 -- Note how the associativities and (relative) precedences differ with the 136 -- infix operators in Data.Function. 137 -- infixl 0 &, &! 138 -- infixl 1 $, $! 139 140 -- | Function application. 141 -- ($) :: (a -> b) -> a -> b 142 -- f $ x = f x 143 144 -- | Strict function application. 145 -- ($!) :: (a -> b) -> a -> b 146 -- f $! !x = f x 147 148 -- Flipped function application, or "pipe". 149 -- (&) :: a -> (a -> b) -> b 150 -- x & f = f x 151 152 -- Strict flipped function application, or "pipe". 153 -- (&!) :: a -> (a -> b) -> b 154 -- !x &! f = f x 155 156 -------------------------------------------------------------------------------- 157 -- Bool 158 159 -- class IsBool (bool :: Type r) where 160 -- true :: (Thunked) => bool 161 -- false :: (Thunked) => bool 162 -- bool :: a -> a -> bool -> a 163 164 -- instance IsBool Bool where 165 -- true = True 166 -- false = False 167 -- bool t f = \case 168 -- True -> t 169 -- False -> f 170 171 -- data UBool :: UType where 172 -- UTrue :: UBool 173 -- UFalse :: UBool 174 175 -- instance IsBool UBool where 176 -- true = UTrue 177 -- false = UFalse 178 -- bool t f = \case 179 -- UTrue -> t 180 -- UFalse -> f 181 182 -- instance Unlift Bool where 183 -- type U Bool = UBool 184 185 -- force True = UTrue 186 -- force False = UFalse 187 188 -- lift UTrue = True 189 -- lift UFalse = False 190 191 -------------------------------------------------------------------------------- 192 -- Maybe 193 194 -- class IsMaybe (maybe :: Type s -> Type r) where 195 -- just :: a -> maybe a 196 -- nothing :: (Thunked) => maybe a 197 -- maybe :: b -> (a -> b) -> maybe a -> b 198 199 -- instance IsMaybe Maybe where 200 -- just = Just 201 -- nothing = Nothing 202 -- maybe n j = \case 203 -- Just a -> j a 204 -- Nothing -> n 205 206 -- data UMaybe :: LType -> UType where 207 -- UJust :: a -> UMaybe a 208 -- UNothing :: UMaybe a 209 210 -- instance IsMaybe UMaybe where 211 -- just = UJust 212 -- nothing = UNothing 213 -- maybe n j = \case 214 -- UJust a -> j a 215 -- UNothing -> n 216 217 -- instance Unlift (Maybe a) where 218 -- type U (Maybe a) = UMaybe a 219 220 -- force (Just a) = UJust a 221 -- force Nothing = UNothing 222 223 -- lift (UJust a) = Just a 224 -- lift UNothing = Nothing 225 226 -- data Maybe' :: UType -> LType where 227 -- Just' :: a -> Maybe' a 228 -- Nothing' :: Maybe' a 229 230 -- instance IsMaybe Maybe' where 231 -- just = Just' 232 -- nothing = Nothing' 233 -- maybe n j = \case 234 -- Just' a -> j a 235 -- Nothing' -> n 236 237 -- data UMaybe' :: UType -> UType where 238 -- UJust' :: a -> UMaybe' a 239 -- UNothing' :: UMaybe' a 240 241 -- instance IsMaybe UMaybe' where 242 -- just = UJust' 243 -- nothing = UNothing' 244 -- maybe n j = \case 245 -- UJust' a -> j a 246 -- UNothing' -> n 247 248 -- instance Unlift (Maybe' a) where 249 -- type U (Maybe' a) = UMaybe' a 250 251 -- force (Just' a) = UJust' a 252 -- force Nothing' = UNothing' 253 254 -- lift (UJust' a) = Just' a 255 -- lift UNothing' = Nothing' 256 257 -- isJust :: forall s r (maybe :: Type s -> Type r) a. (IsMaybe maybe) => maybe a -> Bool 258 -- isJust = maybe False (const True) 259 260 -- isNothing :: (IsMaybe maybe) => maybe a -> Bool 261 -- isNothing = maybe True (const False) 262 263 -- type family Maybe# (r :: RuntimeRep) (l :: Levity) :: Type r -> BoxedType l 264 -- type instance Maybe# LRep Lifted = Maybe 265 -- type instance Maybe# URep Lifted = Maybe' 266 -- type instance Maybe# LRep Unlifted = UMaybe 267 -- type instance Maybe# URep Unlifted = UMaybe' 268 269 -- type family Lower (a :: Kind) :: Kind where 270 -- Lower (BoxedType l) = TypeU 271 -- Lower (k -> l) = k -> Lower l 272 -- type family X (a :: k) :: Lower k 273 -- type instance X (MaybeL @l) = MaybeL @Unlifted 274 275 -------------------------------------------------------------------------------- 276 -- Numeric types 277 278 -- TODO 279 280 -------------------------------------------------------------------------------- 281 -- Category 282 283 -- infixr 9 ∘ 284 285 -- infixr 2 <. 286 -- infixl 2 .> 287 288 -- (⊲⊳) 289 -- (⋖⋗) 290 -- (⩹⩺) 291 -- (⨟) 292 -- (⦂) 293 -- (⋄) 294 -- (∧∨) 295 -- (⩓⩔) 296 -- (∩∪) 297 -- (=≠≡≢≈≉) 298 -- (<>≤≥≮≯≰≱) 299 -- (≺≻≼≽⊀⊁⋠⋡) 300 -- (⊂⊃⊆⊇⊄⊅⊈⊉) 301 -- (⊏⊐⊑⊒) 302 -- (⊢⊣⊤⊥) 303 -- y = h ∘ g ∘ f ∙^ x 304 -- (f ⦾ g ⦿ x) 305 -- y = h ◁ g ◁ f ◀ x 306 -- y = x ▶ f ▷ g ▷ h 307 -- (⧑⧒⧓⧔⧕⧖⧗⋈⋉⋊) 308 -- (↑↓↔↕↖↗↘↙) 309 -- (⥼⥽⥾⥿) 310 -- (⊰⊱) 311 -- (⭘∘) 312 -- (⦁∙⋅) 313 -- (⊙) 314 -- (⊚) 315 -- (⬬⬭⬮⬯) 316 -- (⬝⬞) 317 -- (⋆) 318 -- (⬥⬦⬧⬨⬩⬪⬫) 319 -- (◖◗) 320 -- (◐◑) 321 -- (⫾) 322 -- (■▪▬▮▰▲▶▼◀◆) 323 -- (∙⋆⋄*≀⌑▫) 324 -- y = x ▪ f ▫ g ▫ h 325 -- y = x ⦂ f ⨟ g ⨟ h 326 327 -- TODO: Op, Products, Sums, Clown, Joker 328 329 {- 330 331 class (Bifunctor f, LDomOf f ~ Hask ρ, RDomOf f ~ Hask ρ) => Monoidal (f :: Type ρ -> Type ρ -> Type ρ) where 332 type UnitOf f :: Type ρ 333 unitl :: Iso (Hask ρ) (f (UnitOf f) a) a 334 unitr :: Iso (Hask ρ) (f a (UnitOf f)) a 335 assoc :: Iso (Hask ρ) (f (f a b) c) (f a (f b c)) 336 337 -- TODO: Having this only work for Hask sucks and is needlessly specialized. 338 -- We can generalize this and some above definitions to any category whose 339 -- objects have kind Type ρ, which isn't just Hask (e.g., Kleisli). 340 class (Monoidal f) => Cartesian (f :: Type ρ -> Type ρ -> Type ρ) where 341 fst :: forall (a :: Type ρ) (b :: Type ρ). f a b -> a 342 snd :: forall (a :: Type ρ) (b :: Type ρ). f a b -> b 343 344 pair :: forall (a :: Type ρ) (b :: Type ρ) (c :: Type ρ). (a -> b) -> (a -> c) -> a -> f b c 345 pair f g = bimap f g ∘ diag 346 347 diag :: forall (a :: Type ρ). a -> f a a 348 diag = pair identity identity 349 350 -} 351 352 -- | Right-to-left composition. 353 -- 354 -- This operator is right associative to exploit laziness in the case where 355 -- the outer function doesn't need its argument: 356 -- 357 -- > (const x <. (f <. g)) y ---> const x ((f <. g) y) ---> x 358 -- 359 -- Note that @f <. g@ is never evaluated. 360 -- (<.) :: (Category v) => v b c -> v a b -> v a c 361 -- (<.) = (.) 362 363 -- | Left-to-right composition. 364 -- 365 -- This operator is left associative to exploit laziness in the case where 366 -- the outer function doesn't need its argument: 367 -- 368 -- > ((g .> f) .> const x) y ---> const x ((g .> f) y) ---> x 369 -- 370 -- Note that @g .> f@ is never evaluated. 371 -- (.>) :: (Category v) => v a b -> v b c -> v a c 372 -- (.>) = flip (.) 373 374 -- TODO: (.:), (<.:), (.:>) 375 376 -------------------------------------------------------------------------------- 377 -- Functor 378 379 {- 380 infixl 0 ^&, &^, ~^&, ^&~, ~&^, &^~ 381 infixl 1 $^, ^$, $^~, ~$^, ^$~, ~^$ 382 infixr 2 <<^, ^>>, ^<<, >>^ 383 384 -- | The action of a functor on a function. 385 map, ($^) :: (Functor f) => (a -> b) -> f a -> f b 386 map = fmap 387 ($^) = map 388 389 -- | The action of a functor on a function, flipped. 390 -- 391 -- With the BlockArguments extension, expressions like "@for xs \\x -> ...@" 392 -- look like for-loops, hence the name "for". 393 for, (^&) :: (Functor f) => f a -> (a -> b) -> f b 394 for = flip map 395 (^&) = for 396 397 -- | Application of a function in a functor to a pure value. 398 flap, (^$) :: (Functor f) => f (a -> b) -> a -> f b 399 flap f a = f ^& ($ a) 400 (^$) = flap 401 402 -- | Flipped application of a function in a functor to a pure value. 403 flor, (&^) :: (Functor f) => a -> f (a -> b) -> f b 404 flor = flip flap 405 (&^) = flor 406 407 ($^~) :: (Functor f, Functor g) => (a -> b) -> g (f a) -> g (f b) 408 f $^~ a = (f $^) $^ a 409 410 (~^&) :: (Functor f, Functor g) => g (f a) -> (a -> b) -> g (f b) 411 (~^&) = flip ($^~) 412 413 (~$^) :: (Functor f, Functor g) => g (a -> b) -> f a -> g (f b) 414 f ~$^ a = f ^& ($^ a) 415 416 (^&~) :: (Functor f, Functor g) => f a -> g (a -> b) -> g (f b) 417 (^&~) = flip (~$^) 418 419 (^$~) :: (Functor f, Functor g) => f (a -> b) -> g a -> g (f b) 420 f ^$~ a = (f ^$) $^ a 421 422 (~&^) :: (Functor f, Functor g) => g a -> f (a -> b) -> g (f b) 423 (~&^) = flip (^$~) 424 425 (~^$) :: (Functor f, Functor g) => g (f (a -> b)) -> a -> g (f b) 426 f ~^$ a = f ^& (^$ a) 427 428 (&^~) :: (Functor f, Functor g) => a -> g (f (a -> b)) -> g (f b) 429 (&^~) = flip (~^$) 430 431 -- TODO 432 433 -- | Right-to-left composition with the first function in a functor. 434 (<<^) :: (Functor f, Category v) => v b c -> f (v a b) -> f (v a c) 435 g <<^ f = (g <.) $^ f 436 437 -- TODO 438 439 -- | Left-to-right composition with the first function in a functor. 440 (^>>) :: (Functor f, Category v) => f (v a b) -> v b c -> f (v a c) 441 f ^>> g = f ^& (.> g) 442 443 -- TODO 444 445 -- | Right-to-left composition with the second function in a functor. 446 (^<<) :: (Functor f, Category v) => f (v b c) -> v a b -> f (v a c) 447 g ^<< f = g ^& (<. f) 448 449 -- TODO 450 451 -- | Left-to-right composition with the second function in a functor. 452 (>>^) :: (Functor f, Category v) => v a b -> f (v b c) -> f (v a c) 453 f >>^ g = (f .>) $^ g 454 455 -- TODO: *^, ^* 456 457 -------------------------------------------------------------------------------- 458 -- Applicative 459 460 infixl 0 ^&^, ~^&^~ 461 infixl 1 ^$^, ~^$^~ 462 infixr 2 ^<<^, ^>>^ 463 464 -- | Functions with applicative effects. 465 newtype Appy f a b = Appy {runAppy :: f (a -> b)} 466 467 instance (Functor f) => Functor (Appy f a) where 468 fmap f (Appy a) = Appy (f $^~ a) 469 470 instance (Applicative f) => Applicative (Appy f a) where 471 pure = Appy . pure . const 472 Appy f <*> Appy a = Appy (f ~^$^~ a) 473 474 hom :: (a -> b) -> (b -> b -> c) -> a -> a -> c 475 hom f g x y = g (f x) (f y) 476 477 instance (Alternative f) => Alternative (Appy f a) where 478 empty = Appy empty 479 480 -- Appy x <|> Appy y = Appy (x <|> y) 481 -- (<|>) = hom runAppy (<|>) 482 483 instance (Applicative f) => Category (Appy f) where 484 id = Appy (pure id) 485 Appy f . Appy g = Appy ((.) $^ f ^$^ g) 486 487 -- TODO: Remove ap and plug? 488 -- TODO: liftA{,1,2,3,4} 489 490 -- | An alias for @pure ()@. 491 pass :: (Applicative f) => f () 492 pass = pure () 493 494 -- | Application in an applicative functor. 495 ap, (^$^) :: (Applicative f) => f (a -> b) -> f a -> f b 496 ap = (<*>) 497 (^$^) = ap 498 499 -- | Flipped application in an applicative functor (with effects resolved as 500 -- they appear, left-to-right). 501 plug, (^&^) :: (Applicative f) => f a -> f (a -> b) -> f b 502 plug = (<**>) 503 (^&^) = plug 504 505 (~^$^~) :: (Applicative f, Applicative g) => g (f (a -> b)) -> g (f a) -> g (f b) 506 f ~^$^~ a = (^$^) $^ f ^$^ a 507 508 (~^&^~) :: (Applicative f, Applicative g) => g (f a) -> g (f (a -> b)) -> g (f b) 509 f ~^&^~ a = (^&^) $^ f ^$^ a 510 511 -- TODO: document 512 (^<<^) :: (Applicative f, Category v) => f (v b c) -> f (v a b) -> f (v a c) 513 (^<<^) = liftA2 (<.) 514 515 -- TODO: document 516 (^>>^) :: (Applicative f, Category v) => f (v a b) -> f (v b c) -> f (v a c) 517 (^>>^) = liftA2 (.>) 518 519 -- TODO: "semicolons" 520 521 -------------------------------------------------------------------------------- 522 -- Monad 523 524 infixl 0 ^&!, &!^, ^&!^ 525 infixl 1 $!^, ^$!, ^$!^ 526 527 map', ($!^) :: (Monad m) => (a -> b) -> m a -> m b 528 map' f mx = mx >>= \x -> pure $! f x 529 ($!^) = map' 530 531 for', (^&!) :: (Monad m) => m a -> (a -> b) -> m b 532 for' = flip map' 533 (^&!) = for 534 535 flap', (^$!) :: (Monad m) => m (a -> b) -> a -> m b 536 flap' mf x = mf >>= \f -> pure $! f x 537 (^$!) = flap' 538 539 flor', (&!^) :: (Monad m) => a -> m (a -> b) -> m b 540 flor' = flip flap' 541 (&!^) = flor' 542 543 ap', (^$!^) :: (Monad m) => m (a -> b) -> m a -> m b 544 ap' mf mx = do 545 f <- mf 546 x <- mx 547 pure $! f x 548 (^$!^) = ap' 549 550 plug', (^&!^) :: (Monad m) => m a -> m (a -> b) -> m b 551 plug' mx mf = do 552 x <- mx 553 f <- mf 554 pure $! f x 555 (^&!^) = plug' 556 -} 557 558 -- (.) :: (b0 -> c) -> (a0 -> b0) -> (a0 -> c) 559 -- (g . f) a0 = g (f a0) 560 -- (^.) :: (b0 -> b1 -> c) -> (a0 -> b1) -> (b0 -> a0 -> c) 561 -- (g ^. f) b0 a0 = g b0 (f a0) 562 -- (^^.) :: (b0 -> b1 -> b2 -> c) -> (a0 -> b2) -> (b0 -> b1 -> a0 -> c) 563 -- (g ^^. f) b0 b1 a0 = g b0 b1 (f a0) 564 -- (^^^.) :: (b0 -> b1 -> b2 -> b3 -> c) -> (a0 -> b3) -> (b0 -> b1 -> b2 -> a0 -> c) 565 -- (g ^^^. f) b0 b1 b2 a0 = g b0 b1 b2 (f a0) 566 -- (.^) :: (b0 -> c) -> (a0 -> a1 -> b0) -> (a0 -> a1 -> c) 567 -- (g .^ f) a0 a1 = g (f a0 a1) 568 -- (^.^) :: (b0 -> b1 -> c) -> (a0 -> a1 -> b1) -> (b0 -> a0 -> a1 -> c) 569 -- (g ^.^ f) b0 a0 a1 = g b0 (f a0 a1) 570 -- (^^.^) :: (b0 -> b1 -> b2 -> c) -> (a0 -> a1 -> b2) -> (b0 -> b1 -> a0 -> a1 -> c) 571 -- (g ^^.^ f) b0 b1 a0 a1 = g b0 b1 (f a0 a1) 572 -- (^^^.^) :: (b0 -> b1 -> b2 -> b3 -> c) -> (a0 -> a1 -> b3) -> (b0 -> b1 -> b2 -> a0 -> a1 -> c) 573 -- (g ^^^.^ f) b0 b1 b2 a0 a1 = g b0 b1 b2 (f a0 a1) 574 -- (.^^) :: (b0 -> c) -> (a0 -> a1 -> a2 -> b0) -> (a0 -> a1 -> a2 -> c) 575 -- (^.^^) :: (b0 -> b1 -> c) -> (a0 -> a1 -> a2 -> b1) -> (b0 -> a0 -> a1 -> a2 -> c) 576 -- (^^.^^) :: (b0 -> b1 -> b2 -> c) -> (a0 -> a1 -> a2 -> b2) -> (b0 -> b1 -> a0 -> a1 -> a2 -> c) 577 -- (^^^.^^) :: (b0 -> b1 -> b2 -> b3 -> c) -> (a0 -> a1 -> a2 -> b3) -> (b0 -> b1 -> b2 -> a0 -> a1 -> a2 -> c) 578 -- (.^^^) :: (b0 -> c) -> (a0 -> a1 -> a2 -> a3 -> b0) -> (a0 -> a1 -> a2 -> a3 -> c) 579 -- (^.^^^) :: (b0 -> b1 -> c) -> (a0 -> a1 -> a2 -> a3 -> b1) -> (b0 -> a0 -> a1 -> a2 -> a3 -> c) 580 -- (^^.^^^) :: (b0 -> b1 -> b2 -> c) -> (a0 -> a1 -> a2 -> a3 -> b2) -> (b0 -> b1 -> a0 -> a1 -> a2 -> a3 -> c) 581 -- (^^^.^^^) :: (b0 -> b1 -> b2 -> b3 -> c) -> (a0 -> a1 -> a2 -> a3 -> b3) -> (b0 -> b1 -> b2 -> a0 -> a1 -> a2 -> a3 -> c) 582 583 -}