lude

Haskell prelude alternative
git clone git://git.rr3.xyz/lude | git clone gits://git.rr3.xyz/lude
Log | Files | Refs | README | LICENSE

Core.hs (2175B)

      1 module Lude.Haskell.Core (
      2     module X,
      3     --
      4     Repr,
      5     KindOrType#,
      6     KindOrType,
      7     Kind,
      8     --
      9     Brand,
     10     OpenKind,
     11     --
     12     Endo,
     13     Biendo,
     14     type (.),
     15     type (∘),
     16 ) where
     17 
     18 import Data.Type.Equality as X (type (~), type (~~))
     19 import GHC.Exts as X (IsList (..), IsString (..), Symbol)
     20 
     21 import GHC.Exts qualified as GHC
     22 
     23 --------------------------------------------------------------------------------
     24 
     25 -- | This is just so "kind-level primitives" (@Kind@, @Repr@, etc.) receive a
     26 -- valid Lude signature in GHC diagnostic messages
     27 type KIND = GHC.TYPE GHC.LiftedRep
     28 
     29 type Repr :: KIND
     30 type Repr = GHC.RuntimeRep
     31 
     32 -- NOTE: We typically avoid conflating types and kinds for clarity,
     33 -- but when we do conflate them, we use KindOrType.
     34 
     35 type KindOrType# :: Repr -> KIND
     36 type KindOrType# = GHC.TYPE
     37 
     38 type KindOrType :: KIND
     39 type KindOrType = KindOrType# GHC.LiftedRep
     40 
     41 type Kind :: KIND
     42 type Kind = KindOrType
     43 
     44 --------------------------------------------------------------------------------
     45 -- Open Kinds (i.e., extensible kinds)
     46 
     47 -- | The kind of brands for `OpenKind`
     48 type Brand :: KIND
     49 type Brand = Kind
     50 
     51 -- | Open (i.e., extensible) kinds, which have a brand to distinguish different
     52 -- open kinds
     53 --
     54 -- Example usage:
     55 -- @
     56 -- data FooBrand :: Brand
     57 -- type FooKind = OpenKind FooBrand
     58 -- data FooA :: FooKind       -- Nullary FooKind constructor
     59 -- data FooB :: X -> FooKind  -- Unary FooKind constructor
     60 -- -- ...
     61 -- @
     62 --
     63 -- Open kinds can also have arguments:
     64 -- @
     65 -- data BarBrand :: X -> Brand
     66 -- type BarKind x = OpenKind (BarBrand x)
     67 -- -- ...
     68 -- @
     69 type OpenKind :: Brand -> Kind
     70 type OpenKind b = b -> Kind
     71 
     72 --------------------------------------------------------------------------------
     73 -- Util
     74 
     75 -- TODO: Move?
     76 
     77 -- | @Endo a = a -> a@
     78 type Endo :: forall (r :: Repr). KindOrType# r -> KindOrType
     79 type Endo a = a -> a
     80 
     81 -- | @Biendo a = a -> a -> a@
     82 type Biendo :: forall (r :: Repr). KindOrType# r -> KindOrType
     83 type Biendo a = a -> a -> a
     84 
     85 type (.) :: forall i j k. (j -> k) -> (i -> j) -> (i -> k)
     86 type (f . g) x = f (g x)
     87 infixr 9 .
     88 
     89 type (∘) :: forall i j k. (j -> k) -> (i -> j) -> (i -> k)
     90 type (f ∘ g) x = f (g x)
     91 infixr 9 ∘