{-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE DerivingVia #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE FunctionalDependencies #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE GeneralizedNewtypeDeriving #-} {-# LANGUAGE ImportQualifiedPost #-} {-# LANGUAGE LambdaCase #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-} module Constrained.Univ where import Constrained.List import Control.Monad.Identity import Data.Functor.Const import Data.Kind import Data.Map (Map) import Data.Map qualified as Map import Data.Set (Set) import Data.Set qualified as Set class FunctionLike fn where -- | The semantics of a function is given by `sem` sem :: fn as b -> FunTy as b -- | Evidence that `fn` exists somewhere in `fnU`. To make it possible -- for `fnU` to consist of a balanced tree of functions we need the `path` -- to help GHC disambiguate instances of this class during solving. class IsMember (fn :: [Type] -> Type -> Type) fnU (path :: [PathElem]) where -- | Inject a specific function symbol into a function -- universe. injectFn0 :: fn as b -> fnU as b extractFn0 :: fnU as b -> Maybe (fn as b) type Member fn univ = IsMember fn univ (Path fn univ) injectFn :: forall fn fnU as b. Member fn fnU => fn as b -> fnU as b injectFn :: forall (fn :: [*] -> * -> *) (fnU :: [*] -> * -> *) (as :: [*]) b. Member fn fnU => fn as b -> fnU as b injectFn = forall (fn :: [*] -> * -> *) (fnU :: [*] -> * -> *) (path :: [PathElem]) (as :: [*]) b. IsMember fn fnU path => fn as b -> fnU as b injectFn0 @fn @fnU @(Path fn fnU) extractFn :: forall fn fnU as b. Member fn fnU => fnU as b -> Maybe (fn as b) extractFn :: forall (fn :: [*] -> * -> *) (fnU :: [*] -> * -> *) (as :: [*]) b. Member fn fnU => fnU as b -> Maybe (fn as b) extractFn = forall (fn :: [*] -> * -> *) (fnU :: [*] -> * -> *) (path :: [PathElem]) (as :: [*]) b. IsMember fn fnU path => fnU as b -> Maybe (fn as b) extractFn0 @fn @fnU @(Path fn fnU) data PathElem = PFix | PLeft | PRight ------------------------------------------------------------------------ -- Fixpoints ------------------------------------------------------------------------ {- On the most basic level what we are after is a first order representation of typed functions. Furthermore, we need the representation to be compositional so that you can plug-in your own functions into the universe. That might sound like it's no problem, but the issue is with higher-order functions. Consider: data ListFn where MapFn :: _ '[a] b -> ListFn '[[a]] [b] What should go in place of `_`? It turns out that you need to specify the global function universe and make sure the global universe is the same everywhere. data ListFn fn where MapFn :: fn '[a] b -> ListFn fn '[[a]] [b] -} newtype Fix (fn :: Univ -> Univ) (as :: [Type]) b = Fix (fn (Fix fn) as b) deriving via (fn (Fix fn)) instance FunctionLike (fn (Fix fn)) => FunctionLike (Fix fn) deriving via (fn (Fix fn) as b) instance Eq (fn (Fix fn) as b) => Eq (Fix fn as b) deriving via (fn (Fix fn) as b) instance Show (fn (Fix fn) as b) => Show (Fix fn as b) ------------------------------------------------------------------------ -- Universes ------------------------------------------------------------------------ type Univ = [Type] -> Type -> Type -- TODO: there are faster implementation of this data Oneof fn fn' -- NOTE: everything needs to be quantified over the -- universe because otherwise it would be impossible -- to write higher-order functions (like `foldMap`). (fnU :: [Type] -> Type -> Type) (as :: [Type]) b = OneofLeft !(fn fnU as b) | OneofRight !(fn' fnU as b) -- | Build a balanced tree of `Oneof` from a list of function universes. -- NOTE: it is important that this is a balanced tree as that reduces the amount of -- overhead in `injectFn` and `extractFn` from `O(n)` to `O(log(n))`. Surprisingly, -- we've observed this making more than 10% difference in runtime on some generation -- tasks even though the list `as` is typically small (< 20 elements). type family OneofL as where OneofL '[t] = t OneofL (t : ts) = Insert t (OneofL ts) type family Insert a t where Insert a (Oneof fn fn') = Oneof fn' (Insert a fn) Insert a t = Oneof a t -- | Compute the path to look up `fn` in `fnU` type family MPath fn fnU :: Maybe [PathElem] where MPath fn fn = 'Just '[] MPath fn (Oneof fn' fn'' fnU) = Resolve (MPath fn (fn' fnU)) (MPath fn (fn'' fnU)) MPath fn (Fix fn') = AddFix (MPath fn (fn' (Fix fn'))) MPath _ _ = 'Nothing type family AddFix mpath where AddFix ('Just path) = 'Just ('PFix ': path) AddFix 'Nothing = 'Nothing type family Resolve a b where Resolve ('Just as) _ = 'Just ('PLeft ': as) Resolve _ ('Just bs) = 'Just ('PRight ': bs) Resolve _ _ = 'Nothing type family FromJust m where FromJust ('Just a) = a type family Path fn fn' where Path fn fn' = FromJust (MPath fn fn') instance IsMember fn fn '[] where injectFn0 :: forall (as :: [*]) b. fn as b -> fn as b injectFn0 = forall a. a -> a id extractFn0 :: forall (as :: [*]) b. fn as b -> Maybe (fn as b) extractFn0 = forall a. a -> Maybe a Just instance IsMember fn (fn' (Fix fn')) path => IsMember fn (Fix fn') ('PFix : path) where injectFn0 :: forall (as :: [*]) b. fn as b -> Fix fn' as b injectFn0 fn as b fn = forall (fn :: ([*] -> * -> *) -> [*] -> * -> *) (as :: [*]) b. fn (Fix fn) as b -> Fix fn as b Fix (forall (fn :: [*] -> * -> *) (fnU :: [*] -> * -> *) (path :: [PathElem]) (as :: [*]) b. IsMember fn fnU path => fn as b -> fnU as b injectFn0 @_ @_ @path fn as b fn) extractFn0 :: forall (as :: [*]) b. Fix fn' as b -> Maybe (fn as b) extractFn0 (Fix fn' (Fix fn') as b fn) = forall (fn :: [*] -> * -> *) (fnU :: [*] -> * -> *) (path :: [PathElem]) (as :: [*]) b. IsMember fn fnU path => fnU as b -> Maybe (fn as b) extractFn0 @_ @_ @path fn' (Fix fn') as b fn instance IsMember fn (fn' fnU) path => IsMember fn (Oneof fn' fn'' fnU) ('PLeft : path) where injectFn0 :: forall (as :: [*]) b. fn as b -> Oneof fn' fn'' fnU as b injectFn0 fn as b fn = forall {k} (fn :: ([*] -> * -> *) -> [*] -> k -> *) (fn' :: ([*] -> * -> *) -> [*] -> k -> *) (fnU :: [*] -> * -> *) (as :: [*]) (b :: k). fn fnU as b -> Oneof fn fn' fnU as b OneofLeft (forall (fn :: [*] -> * -> *) (fnU :: [*] -> * -> *) (path :: [PathElem]) (as :: [*]) b. IsMember fn fnU path => fn as b -> fnU as b injectFn0 @_ @_ @path fn as b fn) extractFn0 :: forall (as :: [*]) b. Oneof fn' fn'' fnU as b -> Maybe (fn as b) extractFn0 (OneofLeft fn' fnU as b fn) = forall (fn :: [*] -> * -> *) (fnU :: [*] -> * -> *) (path :: [PathElem]) (as :: [*]) b. IsMember fn fnU path => fnU as b -> Maybe (fn as b) extractFn0 @_ @_ @path fn' fnU as b fn extractFn0 Oneof fn' fn'' fnU as b _ = forall a. Maybe a Nothing instance IsMember fn (fn'' fnU) path => IsMember fn (Oneof fn' fn'' fnU) ('PRight : path) where injectFn0 :: forall (as :: [*]) b. fn as b -> Oneof fn' fn'' fnU as b injectFn0 fn as b fn = forall {k} (fn :: ([*] -> * -> *) -> [*] -> k -> *) (fn' :: ([*] -> * -> *) -> [*] -> k -> *) (fnU :: [*] -> * -> *) (as :: [*]) (b :: k). fn' fnU as b -> Oneof fn fn' fnU as b OneofRight (forall (fn :: [*] -> * -> *) (fnU :: [*] -> * -> *) (path :: [PathElem]) (as :: [*]) b. IsMember fn fnU path => fn as b -> fnU as b injectFn0 @_ @_ @path fn as b fn) extractFn0 :: forall (as :: [*]) b. Oneof fn' fn'' fnU as b -> Maybe (fn as b) extractFn0 (OneofRight fn'' fnU as b fn) = forall (fn :: [*] -> * -> *) (fnU :: [*] -> * -> *) (path :: [PathElem]) (as :: [*]) b. IsMember fn fnU path => fnU as b -> Maybe (fn as b) extractFn0 @_ @_ @path fn'' fnU as b fn extractFn0 Oneof fn' fn'' fnU as b _ = forall a. Maybe a Nothing instance (FunctionLike (fn fnU), FunctionLike (fn' fnU)) => FunctionLike (Oneof fn fn' fnU) where sem :: forall (as :: [*]) b. Oneof fn fn' fnU as b -> FunTy as b sem (OneofLeft fn fnU as b f) = forall (fn :: [*] -> * -> *) (as :: [*]) b. FunctionLike fn => fn as b -> FunTy as b sem fn fnU as b f sem (OneofRight fn' fnU as b f) = forall (fn :: [*] -> * -> *) (as :: [*]) b. FunctionLike fn => fn as b -> FunTy as b sem fn' fnU as b f instance (Show (fn fnU as b), Show (fn' fnU as b)) => Show (Oneof fn fn' fnU as b) where show :: Oneof fn fn' fnU as b -> String show (OneofLeft fn fnU as b fn) = forall a. Show a => a -> String show fn fnU as b fn show (OneofRight fn' fnU as b fn') = forall a. Show a => a -> String show fn' fnU as b fn' instance (Eq (fn fnU as b), Eq (fn' fnU as b)) => Eq (Oneof fn fn' fnU as b) where OneofLeft fn fnU as b fn == :: Oneof fn fn' fnU as b -> Oneof fn fn' fnU as b -> Bool == OneofLeft fn fnU as b fn' = fn fnU as b fn forall a. Eq a => a -> a -> Bool == fn fnU as b fn' OneofRight fn' fnU as b fn == OneofRight fn' fnU as b fn' = fn' fnU as b fn forall a. Eq a => a -> a -> Bool == fn' fnU as b fn' Oneof fn fn' fnU as b _ == Oneof fn fn' fnU as b _ = Bool False ------------------------------------------------------------------------ -- Equality ------------------------------------------------------------------------ equalFn :: forall fn a. (Eq a, Member (EqFn fn) fn) => fn '[a, a] Bool equalFn :: forall (fn :: [*] -> * -> *) a. (Eq a, Member (EqFn fn) fn) => fn '[a, a] Bool equalFn = forall (fn :: [*] -> * -> *) (fnU :: [*] -> * -> *) (as :: [*]) b. Member fn fnU => fn as b -> fnU as b injectFn (forall k (fn :: [*] -> * -> *). Eq k => EqFn fn '[k, k] Bool Equal @_ @fn) data EqFn (fn :: [Type] -> Type -> Type) as b where Equal :: Eq a => EqFn fn '[a, a] Bool deriving instance Eq (EqFn fn as b) deriving instance Show (EqFn fn as b) instance FunctionLike (EqFn fn) where sem :: forall (as :: [*]) b. EqFn fn as b -> FunTy as b sem EqFn fn as b Equal = forall a. Eq a => a -> a -> Bool (==) ------------------------------------------------------------------------ -- Booleans ------------------------------------------------------------------------ notFn :: forall fn. Member (BoolFn fn) fn => fn '[Bool] Bool notFn :: forall (fn :: [*] -> * -> *). Member (BoolFn fn) fn => fn '[Bool] Bool notFn = forall (fn :: [*] -> * -> *) (fnU :: [*] -> * -> *) (as :: [*]) b. Member fn fnU => fn as b -> fnU as b injectFn forall a b. (a -> b) -> a -> b $ forall (fn :: [*] -> * -> *). BoolFn fn '[Bool] Bool Not @fn orFn :: forall fn. Member (BoolFn fn) fn => fn '[Bool, Bool] Bool orFn :: forall (fn :: [*] -> * -> *). Member (BoolFn fn) fn => fn '[Bool, Bool] Bool orFn = forall (fn :: [*] -> * -> *) (fnU :: [*] -> * -> *) (as :: [*]) b. Member fn fnU => fn as b -> fnU as b injectFn forall a b. (a -> b) -> a -> b $ forall (fn :: [*] -> * -> *). BoolFn fn '[Bool, Bool] Bool Or @fn -- | Operations on Bool. -- One might expect And :: BoolFn fn '[Bool, Bool] Bool -- But this is problematic because a Term like ( p x &&. q y ) has to solve for -- x or y first, choose x, so once x is fixed, it might be impossible to solve for y -- Luckily we can get conjuction by using Preds, in fact using Preds, the x and y -- can even be the same variable. -- Or can be problematic too (by using a form of DeMorgan's laws: x && y = not(not x || not y)) -- but while that is possible, there are many scenarios which can only be specified using Or. -- If one inadvertantly uses a form of DeMorgan's laws, the worst that can happen is an ErrorSpec -- is returned, and the user can reformulate using Preds. So Or is incomplete, but sound, when it works. data BoolFn (fn :: [Type] -> Type -> Type) as b where Not :: BoolFn fn '[Bool] Bool Or :: BoolFn fn '[Bool, Bool] Bool deriving instance Eq (BoolFn fn as b) deriving instance Show (BoolFn fn as b) instance FunctionLike (BoolFn fn) where sem :: forall (as :: [*]) b. BoolFn fn as b -> FunTy as b sem BoolFn fn as b Not = Bool -> Bool not sem BoolFn fn as b Or = Bool -> Bool -> Bool (||) ------------------------------------------------------------------------ -- Pairs ------------------------------------------------------------------------ data Prod a b = Prod {forall a b. Prod a b -> a prodFst :: a, forall a b. Prod a b -> b prodSnd :: b} deriving (Prod a b -> Prod a b -> Bool forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a forall a b. (Eq a, Eq b) => Prod a b -> Prod a b -> Bool /= :: Prod a b -> Prod a b -> Bool $c/= :: forall a b. (Eq a, Eq b) => Prod a b -> Prod a b -> Bool == :: Prod a b -> Prod a b -> Bool $c== :: forall a b. (Eq a, Eq b) => Prod a b -> Prod a b -> Bool Eq, Prod a b -> Prod a b -> Bool Prod a b -> Prod a b -> Ordering forall a. Eq a -> (a -> a -> Ordering) -> (a -> a -> Bool) -> (a -> a -> Bool) -> (a -> a -> Bool) -> (a -> a -> Bool) -> (a -> a -> a) -> (a -> a -> a) -> Ord a forall {a} {b}. (Ord a, Ord b) => Eq (Prod a b) forall a b. (Ord a, Ord b) => Prod a b -> Prod a b -> Bool forall a b. (Ord a, Ord b) => Prod a b -> Prod a b -> Ordering forall a b. (Ord a, Ord b) => Prod a b -> Prod a b -> Prod a b min :: Prod a b -> Prod a b -> Prod a b $cmin :: forall a b. (Ord a, Ord b) => Prod a b -> Prod a b -> Prod a b max :: Prod a b -> Prod a b -> Prod a b $cmax :: forall a b. (Ord a, Ord b) => Prod a b -> Prod a b -> Prod a b >= :: Prod a b -> Prod a b -> Bool $c>= :: forall a b. (Ord a, Ord b) => Prod a b -> Prod a b -> Bool > :: Prod a b -> Prod a b -> Bool $c> :: forall a b. (Ord a, Ord b) => Prod a b -> Prod a b -> Bool <= :: Prod a b -> Prod a b -> Bool $c<= :: forall a b. (Ord a, Ord b) => Prod a b -> Prod a b -> Bool < :: Prod a b -> Prod a b -> Bool $c< :: forall a b. (Ord a, Ord b) => Prod a b -> Prod a b -> Bool compare :: Prod a b -> Prod a b -> Ordering $ccompare :: forall a b. (Ord a, Ord b) => Prod a b -> Prod a b -> Ordering Ord, Int -> Prod a b -> ShowS forall a. (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a forall a b. (Show a, Show b) => Int -> Prod a b -> ShowS forall a b. (Show a, Show b) => [Prod a b] -> ShowS forall a b. (Show a, Show b) => Prod a b -> String showList :: [Prod a b] -> ShowS $cshowList :: forall a b. (Show a, Show b) => [Prod a b] -> ShowS show :: Prod a b -> String $cshow :: forall a b. (Show a, Show b) => Prod a b -> String showsPrec :: Int -> Prod a b -> ShowS $cshowsPrec :: forall a b. (Show a, Show b) => Int -> Prod a b -> ShowS Show) fstFn :: forall fn a b. Member (PairFn fn) fn => fn '[Prod a b] a fstFn :: forall (fn :: [*] -> * -> *) a b. Member (PairFn fn) fn => fn '[Prod a b] a fstFn = forall (fn :: [*] -> * -> *) (fnU :: [*] -> * -> *) (as :: [*]) b. Member fn fnU => fn as b -> fnU as b injectFn forall a b. (a -> b) -> a -> b $ forall (fn :: [*] -> * -> *) a k. PairFn fn '[Prod a k] a Fst @fn sndFn :: forall fn a b. Member (PairFn fn) fn => fn '[Prod a b] b sndFn :: forall (fn :: [*] -> * -> *) a b. Member (PairFn fn) fn => fn '[Prod a b] b sndFn = forall (fn :: [*] -> * -> *) (fnU :: [*] -> * -> *) (as :: [*]) b. Member fn fnU => fn as b -> fnU as b injectFn forall a b. (a -> b) -> a -> b $ forall (fn :: [*] -> * -> *) k b. PairFn fn '[Prod k b] b Snd @fn pairFn :: forall fn a b. Member (PairFn fn) fn => fn '[a, b] (Prod a b) pairFn :: forall (fn :: [*] -> * -> *) a b. Member (PairFn fn) fn => fn '[a, b] (Prod a b) pairFn = forall (fn :: [*] -> * -> *) (fnU :: [*] -> * -> *) (as :: [*]) b. Member fn fnU => fn as b -> fnU as b injectFn forall a b. (a -> b) -> a -> b $ forall (fn :: [*] -> * -> *) k v. PairFn fn '[k, v] (Prod k v) Pair @fn data PairFn (fn :: [Type] -> Type -> Type) args res where Pair :: PairFn fn '[a, b] (Prod a b) Fst :: PairFn fn '[Prod a b] a Snd :: PairFn fn '[Prod a b] b deriving instance Show (PairFn fn args res) deriving instance Eq (PairFn fn args res) instance FunctionLike (PairFn fn) where sem :: forall (as :: [*]) b. PairFn fn as b -> FunTy as b sem = \case PairFn fn as b Pair -> forall a b. a -> b -> Prod a b Prod PairFn fn as b Fst -> forall a b. Prod a b -> a prodFst PairFn fn as b Snd -> forall a b. Prod a b -> b prodSnd type family ProdOver as where ProdOver '[] = () ProdOver '[a] = a ProdOver (a : as) = Prod a (ProdOver as) listToProd :: (ProdOver as -> r) -> List Identity as -> r listToProd :: forall (as :: [*]) r. (ProdOver as -> r) -> List Identity as -> r listToProd ProdOver as -> r k List Identity as Nil = ProdOver as -> r k () listToProd ProdOver as -> r k (Identity a a :> List Identity as1 Nil) = ProdOver as -> r k a a listToProd ProdOver as -> r k (Identity a a :> Identity a b :> List Identity as1 as) = ProdOver as -> r k (forall a b. a -> b -> Prod a b Prod a a (forall (as :: [*]) r. (ProdOver as -> r) -> List Identity as -> r listToProd forall a. a -> a id (Identity a b forall {k} (f :: k -> *) (a :: k) (as1 :: [k]). f a -> List f as1 -> List f (a : as1) :> List Identity as1 as))) prodToList :: forall as. TypeList as => ProdOver as -> List Identity as prodToList :: forall (as :: [*]). TypeList as => ProdOver as -> List Identity as prodToList = forall (ts :: [*]). List (Const ()) ts -> ProdOver ts -> List Identity ts go (forall (as :: [*]). TypeList as => List (Const ()) as listShape @as) where go :: forall ts. List (Const ()) ts -> ProdOver ts -> List Identity ts go :: forall (ts :: [*]). List (Const ()) ts -> ProdOver ts -> List Identity ts go List (Const ()) ts Nil ProdOver ts _ = forall {k} (f :: k -> *). List f '[] Nil go (Const () a _ :> List (Const ()) as1 Nil) ProdOver ts a = forall a. a -> Identity a Identity ProdOver ts a forall {k} (f :: k -> *) (a :: k) (as1 :: [k]). f a -> List f as1 -> List f (a : as1) :> forall {k} (f :: k -> *). List f '[] Nil go (Const () a _ :> Const () a ix :> List (Const ()) as1 ixs) (Prod a a ProdOver (a : as1) as) = forall a. a -> Identity a Identity a a forall {k} (f :: k -> *) (a :: k) (as1 :: [k]). f a -> List f as1 -> List f (a : as1) :> forall (ts :: [*]). List (Const ()) ts -> ProdOver ts -> List Identity ts go (Const () a ix forall {k} (f :: k -> *) (a :: k) (as1 :: [k]). f a -> List f as1 -> List f (a : as1) :> List (Const ()) as1 ixs) ProdOver (a : as1) as appendProd :: forall xs ys. (TypeList xs, TypeList ys) => ProdOver xs -> ProdOver ys -> ProdOver (Append xs ys) appendProd :: forall (xs :: [*]) (ys :: [*]). (TypeList xs, TypeList ys) => ProdOver xs -> ProdOver ys -> ProdOver (Append xs ys) appendProd ProdOver xs xs ProdOver ys ys = forall (as :: [*]) r. (ProdOver as -> r) -> List Identity as -> r listToProd forall a. a -> a id (forall {a} (f :: a -> *) (as :: [a]) (bs :: [a]). List f as -> List f bs -> List f (Append as bs) appendList @Identity @xs @ys (forall (as :: [*]). TypeList as => ProdOver as -> List Identity as prodToList ProdOver xs xs) (forall (as :: [*]). TypeList as => ProdOver as -> List Identity as prodToList ProdOver ys ys)) splitProd :: forall xs ys. (TypeList xs, TypeList ys) => ProdOver (Append xs ys) -> Prod (ProdOver xs) (ProdOver ys) splitProd :: forall (xs :: [*]) (ys :: [*]). (TypeList xs, TypeList ys) => ProdOver (Append xs ys) -> Prod (ProdOver xs) (ProdOver ys) splitProd = forall (as :: [*]) (bs :: [*]). List (Const ()) as -> List (Const ()) bs -> ProdOver (Append as bs) -> Prod (ProdOver as) (ProdOver bs) go (forall (as :: [*]). TypeList as => List (Const ()) as listShape @xs) (forall (as :: [*]). TypeList as => List (Const ()) as listShape @ys) where go :: List (Const ()) as -> List (Const ()) bs -> ProdOver (Append as bs) -> Prod (ProdOver as) (ProdOver bs) go :: forall (as :: [*]) (bs :: [*]). List (Const ()) as -> List (Const ()) bs -> ProdOver (Append as bs) -> Prod (ProdOver as) (ProdOver bs) go List (Const ()) as Nil List (Const ()) bs _ ProdOver (Append as bs) p = forall a b. a -> b -> Prod a b Prod () ProdOver (Append as bs) p go (Const () a _ :> List (Const ()) as1 Nil) List (Const ()) bs Nil ProdOver (Append as bs) p = forall a b. a -> b -> Prod a b Prod ProdOver (Append as bs) p () go (Const () a _ :> List (Const ()) as1 Nil) (Const () a _ :> List (Const ()) as1 _) ProdOver (Append as bs) p = ProdOver (Append as bs) p go (Const () a _ :> Const () a a :> List (Const ()) as1 as) List (Const ()) bs bs (Prod a x ProdOver (a : Append as1 bs) xs) = forall a b. a -> b -> Prod a b Prod (forall a b. a -> b -> Prod a b Prod a x ProdOver (a : as1) p0) ProdOver bs p1 where Prod ProdOver (a : as1) p0 ProdOver bs p1 = forall (as :: [*]) (bs :: [*]). List (Const ()) as -> List (Const ()) bs -> ProdOver (Append as bs) -> Prod (ProdOver as) (ProdOver bs) go (Const () a a forall {k} (f :: k -> *) (a :: k) (as1 :: [k]). f a -> List f as1 -> List f (a : as1) :> List (Const ()) as1 as) List (Const ()) bs bs ProdOver (a : Append as1 bs) xs ------------------------------------------------------------------------ -- Sums ------------------------------------------------------------------------ data Sum a b = SumLeft a | SumRight b deriving (Sum a b -> Sum a b -> Bool Sum a b -> Sum a b -> Ordering forall a. Eq a -> (a -> a -> Ordering) -> (a -> a -> Bool) -> (a -> a -> Bool) -> (a -> a -> Bool) -> (a -> a -> Bool) -> (a -> a -> a) -> (a -> a -> a) -> Ord a forall {a} {b}. (Ord a, Ord b) => Eq (Sum a b) forall a b. (Ord a, Ord b) => Sum a b -> Sum a b -> Bool forall a b. (Ord a, Ord b) => Sum a b -> Sum a b -> Ordering forall a b. (Ord a, Ord b) => Sum a b -> Sum a b -> Sum a b min :: Sum a b -> Sum a b -> Sum a b $cmin :: forall a b. (Ord a, Ord b) => Sum a b -> Sum a b -> Sum a b max :: Sum a b -> Sum a b -> Sum a b $cmax :: forall a b. (Ord a, Ord b) => Sum a b -> Sum a b -> Sum a b >= :: Sum a b -> Sum a b -> Bool $c>= :: forall a b. (Ord a, Ord b) => Sum a b -> Sum a b -> Bool > :: Sum a b -> Sum a b -> Bool $c> :: forall a b. (Ord a, Ord b) => Sum a b -> Sum a b -> Bool <= :: Sum a b -> Sum a b -> Bool $c<= :: forall a b. (Ord a, Ord b) => Sum a b -> Sum a b -> Bool < :: Sum a b -> Sum a b -> Bool $c< :: forall a b. (Ord a, Ord b) => Sum a b -> Sum a b -> Bool compare :: Sum a b -> Sum a b -> Ordering $ccompare :: forall a b. (Ord a, Ord b) => Sum a b -> Sum a b -> Ordering Ord, Sum a b -> Sum a b -> Bool forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a forall a b. (Eq a, Eq b) => Sum a b -> Sum a b -> Bool /= :: Sum a b -> Sum a b -> Bool $c/= :: forall a b. (Eq a, Eq b) => Sum a b -> Sum a b -> Bool == :: Sum a b -> Sum a b -> Bool $c== :: forall a b. (Eq a, Eq b) => Sum a b -> Sum a b -> Bool Eq, Int -> Sum a b -> ShowS forall a. (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a forall a b. (Show a, Show b) => Int -> Sum a b -> ShowS forall a b. (Show a, Show b) => [Sum a b] -> ShowS forall a b. (Show a, Show b) => Sum a b -> String showList :: [Sum a b] -> ShowS $cshowList :: forall a b. (Show a, Show b) => [Sum a b] -> ShowS show :: Sum a b -> String $cshow :: forall a b. (Show a, Show b) => Sum a b -> String showsPrec :: Int -> Sum a b -> ShowS $cshowsPrec :: forall a b. (Show a, Show b) => Int -> Sum a b -> ShowS Show) injLeftFn :: forall fn a b. Member (SumFn fn) fn => fn '[a] (Sum a b) injLeftFn :: forall (fn :: [*] -> * -> *) a b. Member (SumFn fn) fn => fn '[a] (Sum a b) injLeftFn = forall (fn :: [*] -> * -> *) (fnU :: [*] -> * -> *) (as :: [*]) b. Member fn fnU => fn as b -> fnU as b injectFn @(SumFn fn) @fn forall (fn :: [*] -> * -> *) k v. SumFn fn '[k] (Sum k v) InjLeft injRightFn :: forall fn a b. Member (SumFn fn) fn => fn '[b] (Sum a b) injRightFn :: forall (fn :: [*] -> * -> *) a b. Member (SumFn fn) fn => fn '[b] (Sum a b) injRightFn = forall (fn :: [*] -> * -> *) (fnU :: [*] -> * -> *) (as :: [*]) b. Member fn fnU => fn as b -> fnU as b injectFn @(SumFn fn) @fn forall (fn :: [*] -> * -> *) k v. SumFn fn '[k] (Sum v k) InjRight data SumFn (fn :: [Type] -> Type -> Type) args res where InjLeft :: SumFn fn '[a] (Sum a b) InjRight :: SumFn fn '[b] (Sum a b) deriving instance Show (SumFn fn args res) deriving instance Eq (SumFn fn args res) instance FunctionLike (SumFn fn) where sem :: forall (as :: [*]) b. SumFn fn as b -> FunTy as b sem = \case SumFn fn as b InjLeft -> forall a b. a -> Sum a b SumLeft SumFn fn as b InjRight -> forall a b. b -> Sum a b SumRight type family SumOver as where SumOver '[a] = a SumOver (a : as) = Sum a (SumOver as) ------------------------------------------------------------------------ -- Sets ------------------------------------------------------------------------ singletonFn :: forall fn a. (Member (SetFn fn) fn, Ord a) => fn '[a] (Set a) singletonFn :: forall (fn :: [*] -> * -> *) a. (Member (SetFn fn) fn, Ord a) => fn '[a] (Set a) singletonFn = forall (fn :: [*] -> * -> *) (fnU :: [*] -> * -> *) (as :: [*]) b. Member fn fnU => fn as b -> fnU as b injectFn forall a b. (a -> b) -> a -> b $ forall k (fn :: [*] -> * -> *). Ord k => SetFn fn '[k] (Set k) Singleton @_ @fn unionFn :: forall fn a. (Member (SetFn fn) fn, Ord a) => fn '[Set a, Set a] (Set a) unionFn :: forall (fn :: [*] -> * -> *) a. (Member (SetFn fn) fn, Ord a) => fn '[Set a, Set a] (Set a) unionFn = forall (fn :: [*] -> * -> *) (fnU :: [*] -> * -> *) (as :: [*]) b. Member fn fnU => fn as b -> fnU as b injectFn forall a b. (a -> b) -> a -> b $ forall k (fn :: [*] -> * -> *). Ord k => SetFn fn '[Set k, Set k] (Set k) Union @_ @fn subsetFn :: forall fn a. (Member (SetFn fn) fn, Ord a) => fn '[Set a, Set a] Bool subsetFn :: forall (fn :: [*] -> * -> *) a. (Member (SetFn fn) fn, Ord a) => fn '[Set a, Set a] Bool subsetFn = forall (fn :: [*] -> * -> *) (fnU :: [*] -> * -> *) (as :: [*]) b. Member fn fnU => fn as b -> fnU as b injectFn forall a b. (a -> b) -> a -> b $ forall k (fn :: [*] -> * -> *). Ord k => SetFn fn '[Set k, Set k] Bool Subset @_ @fn memberFn :: forall fn a. (Member (SetFn fn) fn, Ord a) => fn '[a, Set a] Bool memberFn :: forall (fn :: [*] -> * -> *) a. (Member (SetFn fn) fn, Ord a) => fn '[a, Set a] Bool memberFn = forall (fn :: [*] -> * -> *) (fnU :: [*] -> * -> *) (as :: [*]) b. Member fn fnU => fn as b -> fnU as b injectFn forall a b. (a -> b) -> a -> b $ forall k (fn :: [*] -> * -> *). Ord k => SetFn fn '[k, Set k] Bool Member @_ @fn elemFn :: forall fn a. (Member (SetFn fn) fn, Eq a) => fn '[a, [a]] Bool elemFn :: forall (fn :: [*] -> * -> *) a. (Member (SetFn fn) fn, Eq a) => fn '[a, [a]] Bool elemFn = forall (fn :: [*] -> * -> *) (fnU :: [*] -> * -> *) (as :: [*]) b. Member fn fnU => fn as b -> fnU as b injectFn forall a b. (a -> b) -> a -> b $ forall k (fn :: [*] -> * -> *). Eq k => SetFn fn '[k, [k]] Bool Elem @_ @fn disjointFn :: forall fn a. (Member (SetFn fn) fn, Ord a) => fn '[Set a, Set a] Bool disjointFn :: forall (fn :: [*] -> * -> *) a. (Member (SetFn fn) fn, Ord a) => fn '[Set a, Set a] Bool disjointFn = forall (fn :: [*] -> * -> *) (fnU :: [*] -> * -> *) (as :: [*]) b. Member fn fnU => fn as b -> fnU as b injectFn forall a b. (a -> b) -> a -> b $ forall k (fn :: [*] -> * -> *). Ord k => SetFn fn '[Set k, Set k] Bool Disjoint @_ @fn fromListFn :: forall fn a. (Member (SetFn fn) fn, Ord a) => fn '[[a]] (Set a) fromListFn :: forall (fn :: [*] -> * -> *) a. (Member (SetFn fn) fn, Ord a) => fn '[[a]] (Set a) fromListFn = forall (fn :: [*] -> * -> *) (fnU :: [*] -> * -> *) (as :: [*]) b. Member fn fnU => fn as b -> fnU as b injectFn forall a b. (a -> b) -> a -> b $ forall k (fn :: [*] -> * -> *). Ord k => SetFn fn '[[k]] (Set k) FromList @_ @fn data SetFn (fn :: [Type] -> Type -> Type) args res where Subset :: Ord a => SetFn fn '[Set a, Set a] Bool Disjoint :: Ord a => SetFn fn '[Set a, Set a] Bool Member :: Ord a => SetFn fn '[a, Set a] Bool Singleton :: Ord a => SetFn fn '[a] (Set a) Union :: Ord a => SetFn fn '[Set a, Set a] (Set a) Elem :: Eq a => SetFn fn '[a, [a]] Bool FromList :: Ord a => SetFn fn '[[a]] (Set a) deriving instance Show (SetFn fn args res) deriving instance Eq (SetFn fn args res) instance FunctionLike (SetFn fn) where sem :: forall (as :: [*]) b. SetFn fn as b -> FunTy as b sem = \case SetFn fn as b Subset -> forall a. Ord a => Set a -> Set a -> Bool Set.isSubsetOf SetFn fn as b Disjoint -> forall a. Ord a => Set a -> Set a -> Bool Set.disjoint SetFn fn as b Member -> forall a. Ord a => a -> Set a -> Bool Set.member SetFn fn as b Singleton -> forall a. a -> Set a Set.singleton SetFn fn as b Union -> forall a. Semigroup a => a -> a -> a (<>) SetFn fn as b Elem -> forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool elem SetFn fn as b FromList -> forall a. Ord a => [a] -> Set a Set.fromList ------------------------------------------------------------------------ -- Maps ------------------------------------------------------------------------ data MapFn (fn :: [Type] -> Type -> Type) args res where Dom :: Ord k => MapFn fn '[Map k v] (Set k) Rng :: MapFn fn '[Map k v] [v] Lookup :: Ord k => MapFn fn '[k, Map k v] (Maybe v) deriving instance Show (MapFn fn args res) deriving instance Eq (MapFn fn args res) instance FunctionLike (MapFn fn) where sem :: forall (as :: [*]) b. MapFn fn as b -> FunTy as b sem = \case MapFn fn as b Dom -> forall k a. Map k a -> Set k Map.keysSet MapFn fn as b Rng -> forall k a. Map k a -> [a] Map.elems MapFn fn as b Lookup -> forall k a. Ord k => k -> Map k a -> Maybe a Map.lookup domFn :: forall fn k v. (Member (MapFn fn) fn, Ord k) => fn '[Map k v] (Set k) domFn :: forall (fn :: [*] -> * -> *) k v. (Member (MapFn fn) fn, Ord k) => fn '[Map k v] (Set k) domFn = forall (fn :: [*] -> * -> *) (fnU :: [*] -> * -> *) (as :: [*]) b. Member fn fnU => fn as b -> fnU as b injectFn forall a b. (a -> b) -> a -> b $ forall k (fn :: [*] -> * -> *) v. Ord k => MapFn fn '[Map k v] (Set k) Dom @_ @fn rngFn :: forall fn k v. Member (MapFn fn) fn => fn '[Map k v] [v] rngFn :: forall (fn :: [*] -> * -> *) k v. Member (MapFn fn) fn => fn '[Map k v] [v] rngFn = forall (fn :: [*] -> * -> *) (fnU :: [*] -> * -> *) (as :: [*]) b. Member fn fnU => fn as b -> fnU as b injectFn forall a b. (a -> b) -> a -> b $ forall (fn :: [*] -> * -> *) k v. MapFn fn '[Map k v] [v] Rng @fn lookupFn :: forall fn k v. (Member (MapFn fn) fn, Ord k) => fn '[k, Map k v] (Maybe v) lookupFn :: forall (fn :: [*] -> * -> *) k v. (Member (MapFn fn) fn, Ord k) => fn '[k, Map k v] (Maybe v) lookupFn = forall (fn :: [*] -> * -> *) (fnU :: [*] -> * -> *) (as :: [*]) b. Member fn fnU => fn as b -> fnU as b injectFn forall a b. (a -> b) -> a -> b $ forall k (fn :: [*] -> * -> *) v. Ord k => MapFn fn '[k, Map k v] (Maybe v) Lookup @_ @fn