lude

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

SomeType.hs.txt (2368B)

      1 {-# LANGUAGE UndecidableInstances #-}
      2 {-# OPTIONS_GHC -Wno-orphans #-}
      3 
      4 module Todo.SomeType where
      5 
      6 import Lude hiding (Box)
      7 import Lude.Haskell.Repr qualified as Repr
      8 import Todo.DependentKinds
      9 
     10 --------------------------------------------------------------------------------
     11 
     12 type instance DefaultCat SomeType = SomeFunction
     13 
     14 type SomeType :: Kind
     15 type SomeType = Repr @* Type#
     16 
     17 -- | The full subcategory of arbitrarily-represented Haskell types and functions
     18 -- whose `Repr`s are `Functional#`
     19 type SomeFunction :: Cat SomeType
     20 data SomeFunction a b = (Functional# `OnIdx` a, Functional# `OnIdx` b) => MkHFunction (Val a -> Val b)
     21 
     22 instance SomeFunction a b `Witnesses` Mor SomeFunction a b where
     23     witness (MkHFunction _) = MkEvidence
     24 
     25 -- TODO: Ugghhhh this is a lie. Composition is not associative due to Haskell's
     26 -- garbage lazy semantics. We could just say it's only lawful up to bottoms and
     27 -- go on with life.
     28 instance Categorical SomeFunction where
     29     type Obj SomeFunction = OnIdx Functional#
     30     identity = MkHFunction identityFunction
     31     compose (MkHFunction f) (MkHFunction g) = MkHFunction (composeFunction f g)
     32     witnessMor = witness
     33 
     34 type Some :: Type -> SomeType
     35 type Some = MkExists Repr.BoxL
     36 instance Functorial Some where
     37     map f = MkHFunction f
     38 
     39 type Box :: SomeType -> Type
     40 newtype Box a = MkBox {unBox :: Lev (Val a)}
     41 instance Functorial Box where
     42     map (MkHFunction f) = \(MkBox x) -> MkBox (app# f x)
     43 
     44 -- We can't define products `HFunction^2 -> HFunction` as
     45 --     (r, a) * (s, b)  :=  (Repr.Tuple [r, s], Tuple2# a b),
     46 -- because we don't implement Functional# on tuples. Instead,
     47 --     (r, a) * (s, b)  :=  (BoxL, forall (t :: Repr) (c :: Type# t). (a -> b -> c) -> c),
     48 -- i.e., Church-encoded.
     49 
     50 -- infixr 1 ->#
     51 -- type (->#) :: SomeType -> forall (r :: Repr). Type# r -> Type
     52 -- type a -># b = Val a -> b
     53 
     54 -- infixr 1 ->#
     55 -- type (->#) :: SomeType -> SomeType -> SomeType
     56 -- type a -># b = MkExists Repr.BoxL (Val a -> Val b)
     57 
     58 type Prod :: SomeType -> SomeType -> Type
     59 newtype Prod a b = MkProd {unProd :: forall {r :: Repr} (c :: Type# r). (Val a -> Val b -> c) -> c}
     60 
     61 instance forall (a :: SomeType). (Obj SomeFunction a) => Functorial (Prod a) where
     62     map (MkHFunction f) = \(MkProd p) -> MkProd \k -> p (k *.# f)
     63 instance Functorial Prod where
     64     map (MkHFunction f) = Naturally \(MkProd p) -> MkProd \k -> p (k .# f)