lude

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

Terminal.hs (844B)

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