lude

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

Quantifier.hs.txt (2020B)

      1 module Todo.Quantifier where
      2 
      3 import Lude
      4 
      5 --------------------------------------------------------------------------------
      6 
      7 -- TODO: zap?
      8 
      9 type Exists :: forall {i}. (i -> Type) -> Type
     10 data Exists f = forall x. MkExists (f x)
     11 
     12 instance Functorial Exists where
     13     type Dom Exists = Discrete ==> Function -- Could be generalized beyond Discrete.
     14     type Cod Exists = Function
     15     map (Naturally f) = \(MkExists a) -> MkExists (f a)
     16 
     17 type Forall :: forall {i}. (i -> Type) -> Type
     18 data Forall f = MkForall (forall x. f x)
     19 
     20 instance Functorial Forall where
     21     type Dom Forall = Discrete ==> Function -- Could be generalized beyond Discrete.
     22     type Cod Forall = Function
     23     map (Naturally f) = \(MkForall a) -> MkForall (f a)
     24 
     25 type Under :: forall {i}. (i -> Type) -> Type -> (i -> Type)
     26 newtype Under f a x = MkUnder {unUnder :: f x -> a}
     27 
     28 instance Functorial (Under f a) where
     29     type Dom (Under f a) = Dual Discrete
     30     type Cod (Under f a) = Function
     31     map (MkDual MkDiscrete) = identity
     32 
     33 instance Functorial (Under f) where
     34     type Dom (Under f) = Function
     35     type Cod (Under f) = Dual Discrete ==> Function
     36     map f = Naturally \(MkUnder g) -> MkUnder (f . g)
     37 
     38 instance Functorial Under where
     39     type Dom Under = Dual (Discrete ==> Function)
     40     type Cod Under = Function ==> Dual Discrete ==> Function
     41     map (MkDual (Naturally f)) = Naturally (Naturally \(MkUnder g) -> MkUnder (g . f))
     42 
     43 -- elimExists :: forall {i} (f :: i -> Type) (a :: Type). Forall (Under f a) -> Exists f -> a
     44 -- elimExists (MkForall k) (MkExists f) = unUnder k f
     45 
     46 -- elimForall :: forall {i} (f :: i -> Type) (a :: Type). Exists (Under f a) -> Forall f -> a
     47 -- elimForall (MkExists k) (MkForall f) = unUnder k f
     48 
     49 elimExists :: forall {i} (f :: i -> Type) (a :: Type). Forall (Under f a) -> Under Exists a f
     50 elimExists (MkForall k) = MkUnder \(MkExists f) -> unUnder k f
     51 
     52 elimForall :: forall {i} (f :: i -> Type) (a :: Type). Exists (Under f a) -> Under Forall a f
     53 elimForall (MkExists k) = MkUnder \(MkForall f) -> unUnder k f