{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE GADTs #-}
{-# 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
sem :: fn as b -> FunTy as b
class IsMember (fn :: [Type] -> Type -> Type) fnU (path :: [PathElem]) where
injectFn0 :: fn as b -> fnU as b
:: 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)
= 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
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)
type Univ = [Type] -> Type -> Type
data
Oneof
fn
fn'
(fnU :: [Type] -> Type -> Type)
(as :: [Type])
b
= OneofLeft !(fn fnU as b)
| OneofRight !(fn' fnU as b)
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
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
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
(==)
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
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
(||)
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
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)
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
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