lude

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

Initial.hs (829B)

      1 module Lude.Algebra.Category.Initial (
      2     HasInitialObject (..),
      3     absurd,
      4 ) where
      5 
      6 import Lude.Algebra.Category.Core
      7 import Lude.Constraint.Falsum
      8 import Lude.Haskell
      9 import Lude.Void
     10 
     11 --------------------------------------------------------------------------------
     12 
     13 type HasInitialObject :: forall {i}. Cat i -> Constraint
     14 class (Categorical p) => HasInitialObject (p :: Cat i) where
     15     type Initial p :: i
     16     initiate :: forall (a :: i). (Obj p a) => Initial p `p` a
     17 
     18 -- | Alias for `initiate`
     19 absurd :: forall {i} (a :: i) (p :: Cat i). (HasInitialObject p, Obj p a) => Initial p `p` a
     20 absurd = initiate
     21 
     22 instance HasInitialObject Function where
     23     type Initial Function = Void
     24     initiate = \case {}
     25 
     26 instance HasInitialObject Entailment where
     27     type Initial Entailment = Falsum
     28     initiate = Entail contradiction