Functional.hs (2940B)
1 {-# LANGUAGE CPP #-} 2 {-# LANGUAGE ImpredicativeTypes #-} 3 4 module Lude.Haskell.Functional ( 5 Lev, 6 coerceLev, 7 Functional# (..), 8 Box(..), -- Make constructors visible for coercions. 9 ($#), 10 lam2#, 11 app2#, 12 ) where 13 14 import Data.Coerce 15 import Data.Tuple.Experimental qualified as GHC 16 17 import Lude.Haskell.Constraint 18 import Lude.Haskell.Core 19 import Lude.Haskell.Repr qualified as Repr 20 import Lude.Haskell.Type 21 22 -- TODO: Replace Lev with Box in lam# and app#? 23 -- It's less convenient but more efficient for boxed types. 24 25 -------------------------------------------------------------------------------- 26 27 -- | Transparently box a type of any representation 28 -- 29 -- Use `Lev` to declare unlifted values at the top-level. For example, for any 30 -- @r :: Repr@, @A :: Type r@, and @bar :: A@: 31 -- @ 32 -- foo :: Lev A 33 -- foo = bar 34 -- @ 35 type Lev :: forall {r :: Repr}. Type# r -> Type 36 type Lev a = (GHC.CTuple0) => a 37 38 -- | Coerce between levitated types 39 coerceLev :: forall {r :: Repr} (a :: Type# r) (b :: Type# r). (Coercible a b) => Lev a -> Lev b 40 coerceLev = coerce @(Lev a) @(Lev b) 41 42 type Functional# :: Repr -> Constraint 43 class Functional# r where 44 data Box :: Type# r -> Type 45 mkBox# :: forall (a :: Type# r). a -> Box a 46 unBox# :: forall (a :: Type# r). Box a -> a 47 lam# :: forall (a :: Type# r) {s :: Repr} (b :: Type# s). (Lev a -> b) -> (a -> b) 48 app# :: forall (a :: Type# r) {s :: Repr} (b :: Type# s). (a -> b) -> (Lev a -> b) 49 50 ($#) :: forall (r :: Repr) (a :: Type# r) (s :: Repr) (b :: Type# s). (Functional# r) => (a -> b) -> (Lev a -> b) 51 ($#) = app# 52 infixl 1 $# 53 54 lam2# 55 :: forall {r0 :: Repr} (a0 :: Type# r0) {r1 :: Repr} (a1 :: Type# r1) {s :: Repr} (b :: Type# s) 56 . (Functional# r0, Functional# r1) => (Lev a0 -> Lev a1 -> b) -> (a0 -> a1 -> b) 57 lam2# f = lam# \x -> lam# (f x) 58 59 app2# 60 :: forall {r0 :: Repr} (a0 :: Type# r0) {r1 :: Repr} (a1 :: Type# r1) {s :: Repr} (b :: Type# s) 61 . (Functional# r0, Functional# r1) => (a0 -> a1 -> b) -> (Lev a0 -> Lev a1 -> b) 62 app2# f x y = f `app#` x `app#` y 63 64 -------------------------------------------------------------------------------- 65 66 #define FUNCTIONAL(R, DECLARE, C)\ 67 instance Functional# Repr.R where\ 68 DECLARE Box @Repr.R a = C a;\ 69 mkBox# = C; {-# INLINE mkBox# #-};\ 70 unBox# (C x) = x; {-# INLINE unBox# #-};\ 71 lam# f = \x -> f x; {-# INLINE lam# #-};\ 72 app# f = \x -> f x; {-# INLINE app# #-} 73 74 FUNCTIONAL(BoxL, newtype, MkBoxLBox) 75 FUNCTIONAL(BoxE, data, MkBoxEBox) 76 FUNCTIONAL(Addr, data, MkAddrBox) 77 FUNCTIONAL(Int, data, MkIntBox) 78 FUNCTIONAL(Int8, data, MkInt8Box) 79 FUNCTIONAL(Int16, data, MkInt16Box) 80 FUNCTIONAL(Int32, data, MkInt32Box) 81 FUNCTIONAL(Int64, data, MkInt64Box) 82 FUNCTIONAL(Nat, data, MkNatBox) 83 FUNCTIONAL(Nat8, data, MkNat8Box) 84 FUNCTIONAL(Nat16, data, MkNat16Box) 85 FUNCTIONAL(Nat32, data, MkNat32Box) 86 FUNCTIONAL(Nat64, data, MkNat64Box) 87 FUNCTIONAL(Flt32, data, MkFlt32Box) 88 FUNCTIONAL(Flt64, data, MkFlt64Box)