lude

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

Const.hs (2009B)

      1 -- TODO: Const functors are also bifunctors?
      2 type HasConstFunctor :: forall {i} {j}. Cat i -> Cat j -> Constraint
      3 class (Categorical p, Categorical q, forall (b :: j) (f :: i -> j). (f ~ ConstOn p q b) => FunctorialOn p q f) => HasConstFunctor (p :: Cat i) (q :: Cat j) where
      4     type ConstOn p q :: j -> i -> j
      5 
      6     -- TODO: Use Iso abstraction here. Also, `p` is ambiguous, so we should
      7     -- probably require the `p` type argument.
      8     mkConstOn :: forall (a :: i) (b :: j). b `q` ConstOn p q b a
      9     unConstOn :: forall (a :: i) (b :: j). ConstOn p q b a `q` b
     10 
     11 type Const :: forall {i}. Cat i -> Type -> i -> Type
     12 newtype Const p b a = MkConst {unConst :: b}
     13 instance (Categorical p) => Functorial (Const p b) where
     14     type Dom (Const p b) = p
     15     type Cod (Const p b) = Function
     16     map _ = coerce
     17 instance (Categorical p) => HasConstFunctor p Function where
     18     type ConstOn p Function = Const p
     19     mkConstOn = MkConst
     20     unConstOn = unConst
     21 
     22 -- TODO: Is this misnamed?
     23 type Tautology :: forall {i}. Cat i -> Constraint -> i -> Constraint
     24 class (b) => Tautology p b a
     25 instance (b) => Tautology p b a
     26 instance (Categorical p) => Functorial (Tautology p b) where
     27     type Dom (Tautology p b) = p
     28     type Cod (Tautology p b) = Entailment
     29     map _ = Entail MkEvidence
     30 instance (Categorical p) => HasConstFunctor p Entailment where
     31     type ConstOn p Entailment = Tautology p
     32     mkConstOn = Entail MkEvidence
     33     unConstOn = Entail MkEvidence
     34 
     35 instance (HasTerminalObject q, HasConstFunctor p q) => HasTerminalObject (NT p q) where
     36     type Terminal (NT p q) = ConstOn p q (Terminal q)
     37     terminate @f = Naturally \ @a -> mkConstOn @p . terminate \\ f `preservesObj` a
     38 
     39 instance (HasInitialObject q, HasConstFunctor p q) => HasInitialObject (NT p q) where
     40     type Initial (NT p q) = ConstOn p q (Initial q)
     41     initiate @f = Naturally \ @a -> initiate . unConstOn @p \\ f `preservesObj` a
     42 
     43 test :: forall p f. (FunctorialOn p Entailment f) => NT p Entailment f (Tautology p Verum)
     44 test = terminate