lude

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

ReprGenericMaybe.hs.txt (2620B)

      1 --------------------------------------------------------------------------------
      2 
      3 type TypeB :: Repr.EvalOrder -> Kind
      4 type TypeB eo = Type# (Repr.Box eo)
      5 
      6 type TypeL :: Kind
      7 type TypeL = TypeB Repr.Lazy
      8 
      9 type TypeE :: Kind
     10 type TypeE = TypeB Repr.Eager
     11 
     12 --------------------------------------------------------------------------------
     13 
     14 type MaybeB :: forall (eo :: Repr.EvalOrder) -> forall (r :: Repr). Type# r -> TypeB eo
     15 data family MaybeB
     16 data instance MaybeB Repr.Lazy @Repr.BoxL a = NothingLL | JustLL a
     17 data instance MaybeB Repr.Eager @Repr.BoxL a = NothingEL | JustEL a
     18 data instance MaybeB Repr.Lazy @Repr.BoxE a = NothingLE | JustLE a
     19 data instance MaybeB Repr.Eager @Repr.BoxE a = NothingEE | JustEE a
     20 
     21 type IsMaybe :: forall {r :: Repr} {s :: Repr}. (Type# r -> Type# s) -> Constraint
     22 class IsMaybe (maybe :: Type# r -> Type# s) where
     23     nothing :: forall (a :: Type# r). Lev (maybe a)
     24     just :: forall (a :: Type# r). a -> maybe a
     25     elimMaybe :: forall {t :: Repr} (b :: Type# t) (a :: Type# r). Lev b -> (a -> b) -> (maybe a -> b)
     26 
     27 instance IsMaybe (MaybeB Repr.Lazy @Repr.BoxL) where nothing = NothingLL; just = JustLL; elimMaybe n j = \case NothingLL -> n; JustLL a -> j a
     28 instance IsMaybe (MaybeB Repr.Eager @Repr.BoxL) where nothing = NothingEL; just = JustEL; elimMaybe n j = \case NothingEL -> n; JustEL a -> j a
     29 instance IsMaybe (MaybeB Repr.Lazy @Repr.BoxE) where nothing = NothingLE; just = JustLE; elimMaybe n j = \case NothingLE -> n; JustLE a -> j a
     30 instance IsMaybe (MaybeB Repr.Eager @Repr.BoxE) where nothing = NothingEE; just = JustEE; elimMaybe n j = \case NothingEE -> n; JustEE a -> j a
     31 
     32 --------------------------------------------------------------------------------
     33 
     34 type Maybe# :: forall (r :: Repr). Type# r -> Type
     35 newtype Maybe# a = MkMaybe# {unMaybe# :: forall (s :: Repr) (b :: Type# s). Lev b -> (a -> b) -> b}
     36 
     37 -- | Laws:
     38 -- - @elimMaybe n _ nothing@ = @n@
     39 -- - @elimMaybe _ j (just x)@ = @j x@
     40 -- - @elimMaybe nothing just@ = @id@
     41 type IsMaybe :: forall {r :: Repr}. (Type# r -> Type) -> Constraint
     42 class IsMaybe (maybe :: Type# r -> Type) where
     43     nothing :: forall (a :: Type# r). maybe a
     44     just :: forall (a :: Type# r). a -> maybe a
     45     elimMaybe :: forall (a :: Type# r) {s :: Repr} (b :: Type# s). Lev b -> (a -> b) -> maybe a -> b
     46 
     47 instance IsMaybe Maybe where
     48     nothing = Nothing
     49     just = Just
     50     elimMaybe n j = \case
     51         Nothing -> n
     52         Just x -> j x
     53 
     54 instance forall (r :: Repr). (Functional# r) => IsMaybe (Maybe# @r) where
     55     nothing = MkMaybe# \n _ -> n
     56     just = lam# \x -> MkMaybe# \_ j -> j $# x
     57     elimMaybe n j m = unMaybe# m n j