module Data.Witness.List where
{
import Prelude hiding (id,(.));
import Data.Witness.Representative;
import Data.Type.Equality;
import Control.Category.Dual;
import Data.Constraint(Dict(..));
import Control.Applicative;
import Control.Category;
import Data.Functor.Identity as Import;
;
data ListType (w :: * -> *) (lt :: *) where
{
NilListType :: ListType w ();
ConsListType :: w a -> ListType w lt -> ListType w (a,lt);
};
instance Eq1 w => Eq1 (ListType w) where
{
equals1 NilListType NilListType = True;
equals1 (ConsListType pe pl) (ConsListType qe ql) = (equals1 pe qe) && (equals1 pl ql);
equals1 _ _ = False;
};
instance Eq1 w => Eq (ListType w a) where
{
(==) = equals1;
};
instance (Representative w) => Representative (ListType w) where
{
getRepWitness NilListType = Dict;
getRepWitness (ConsListType w lw) = case (getRepWitness w,getRepWitness lw) of
{
(Dict,Dict) -> Dict;
};
};
instance (Representative w) => Is (ListType w) () where
{
representative = NilListType;
};
instance (Is w a,Is (ListType w) lt) => Is (ListType w) (a,lt) where
{
representative = ConsListType representative representative;
};
instance (TestEquality w) => TestEquality (ListType w) where
{
testEquality NilListType NilListType = Just Refl;
testEquality (ConsListType wpa wpb) (ConsListType wqa wqb) = do
{
Refl <- testEquality wpa wqa;
Refl <- testEquality wpb wqb;
return Refl;
};
testEquality _ _ = Nothing;
};
listFill :: ListType w t -> (forall a. w a -> a) -> t;
listFill NilListType _f = ();
listFill (ConsListType wa wr) f = (f wa,listFill wr f);
listMap :: ListType w t -> (forall a. w a -> a -> a) -> t -> t;
listMap NilListType _f () = ();
listMap (ConsListType wa wr) f (a,rest) = (f wa a,listMap wr f rest);
listLift2 :: ListType w t -> (forall a. w a -> a -> a -> a) -> t -> t -> t;
listLift2 NilListType _f () () = ();
listLift2 (ConsListType wa wr) f (a,resta) (b,restb) = (f wa a b,listLift2 wr f resta restb);
listTypeToList :: (forall a. w a -> r) -> ListType w t -> [r];
listTypeToList _wr NilListType = [];
listTypeToList wr (ConsListType wa rest) = (wr wa):(listTypeToList wr rest);
listTypeMap :: (forall a. w1 a -> w2 a) -> ListType w1 t -> ListType w2 t;
listTypeMap _ww NilListType = NilListType;
listTypeMap ww (ConsListType wa rest) = ConsListType (ww wa) (listTypeMap ww rest);
listIdentity :: ListType Identity lt -> lt;
listIdentity NilListType = ();
listIdentity (ConsListType (Identity a) rest) = (a,listIdentity rest);
listSequence :: (Applicative f) => ListType f lt -> f lt;
listSequence NilListType = pure ();
listSequence (ConsListType fa rest) = liftA2 (,) fa (listSequence rest);
data AppendList w la lb = forall lr. MkAppendList
{
listAppendWitness :: ListType w lr,
listAppend :: la -> lb -> lr,
listSplit :: lr -> (la,lb)
};
appendList :: ListType w la -> ListType w lb -> AppendList w la lb;
appendList NilListType wlb = MkAppendList
{
listAppendWitness = wlb,
listAppend = \() lb -> lb,
listSplit = \lb -> ((),lb)
};
appendList (ConsListType wa wla) wlb = case appendList wla wlb of
{
MkAppendList wit join split -> MkAppendList
{
listAppendWitness = ConsListType wa wit,
listAppend = \(a,la) lb -> (a,join la lb),
listSplit = \(a,lab) -> case split lab of
{
(la,lb) -> ((a,la),lb);
}
};
};
data AddItemList w a l = forall lr. MkAddItemList
{
listAddItemWitness :: ListType w lr,
listAddItem :: a -> l -> lr,
listSplitItem :: lr -> (a,l)
};
addListItem :: w a -> ListType w l -> AddItemList w a l;
addListItem wa wl = MkAddItemList
{
listAddItemWitness = ConsListType wa wl,
listAddItem = (,),
listSplitItem = id
};
data MergeItemList w a l = forall lr. MkMergeItemList
{
listMergeItemWitness :: ListType w lr,
listMergeItem :: (Maybe a -> a) -> l -> lr,
listUnmergeItem :: lr -> (a,l)
};
mergeListItem :: (TestEquality w) => ListType w l -> w a -> MergeItemList w a l;
mergeListItem NilListType wa = MkMergeItemList
{
listMergeItemWitness = ConsListType wa NilListType,
listMergeItem = \maa () -> (maa Nothing,()),
listUnmergeItem = id
};
mergeListItem wl@(ConsListType wa' _) wa | Just Refl <- testEquality wa wa' = MkMergeItemList
{
listMergeItemWitness = wl,
listMergeItem = \maa (a,l) -> (maa (Just a),l),
listUnmergeItem = \(a,l) -> (a,(a,l))
};
mergeListItem (ConsListType wa' wl) wa = case mergeListItem wl wa of
{
MkMergeItemList wit merge unmerge -> MkMergeItemList
{
listMergeItemWitness = ConsListType wa' wit,
listMergeItem = \maa (a',l) -> (a',merge maa l),
listUnmergeItem = \(a',l') -> case unmerge l' of
{
(a,l) -> (a,(a',l));
}
};
};
data MergeList w la lb = forall lr. MkMergeList
{
listMergeWitness :: ListType w lr,
listMerge :: (forall t. w t -> t -> t -> t) -> la -> lb -> lr,
listUnmerge :: lr -> (la,lb)
};
mergeList :: (TestEquality w) => ListType w la -> ListType w lb -> MergeList w la lb;
mergeList wla NilListType = MkMergeList
{
listMergeWitness = wla,
listMerge = \_ la () -> la,
listUnmerge = \la -> (la,())
};
mergeList wla (ConsListType wb wlb) = case mergeListItem wla wb of
{
MkMergeItemList wla' mergeItem unmergeItem -> case mergeList wla' wlb of
{
MkMergeList wlr merge unmerge -> MkMergeList
{
listMergeWitness = wlr,
listMerge = \f la (b,lb) -> merge f (mergeItem (\mb' -> case mb' of
{
Just b' -> f wb b' b;
Nothing -> b;
}) la) lb,
listUnmerge = \lr -> case unmerge lr of
{
(la',lb) -> case unmergeItem la' of
{
(b,la) -> (la,(b,lb));
};
}
};
};
};
class Tensor cc where
{
tensorUnit :: cc () ();
tensorPair :: cc a1 b1 -> cc a2 b2 -> cc (a1,a2) (b1,b2);
};
instance Tensor (->) where
{
tensorUnit = id;
tensorPair ab1 ab2 (a1,a2) = (ab1 a1,ab2 a2);
};
instance (Tensor cc) => Tensor (Dual cc) where
{
tensorUnit = Dual tensorUnit;
tensorPair (Dual ab1) (Dual ab2) = Dual (tensorPair ab1 ab2);
};
type MapWitness cc w1 w2 = forall r v1. w1 v1 -> (forall v2. w2 v2 -> (cc v1 v2) -> r) -> r;
sameMapWitness :: (forall v. w v -> cc v v) -> MapWitness cc w w;
sameMapWitness wc w wcr = wcr w (wc w);
data MapList cc w2 l = forall lr. MkMapList
{
listMapWitness :: ListType w2 lr,
listMapW :: cc l lr
};
mapList :: (Tensor cc) => MapWitness cc w1 w2 -> ListType w1 l -> MapList cc w2 l;
mapList _ NilListType = MkMapList
{
listMapWitness = NilListType,
listMapW = tensorUnit
};
mapList mapwit (ConsListType w rest) = case mapList mapwit rest of
{
MkMapList wit listMapW' -> mapwit w (\w' vmap -> MkMapList
{
listMapWitness = ConsListType w' wit,
listMapW = tensorPair vmap listMapW'
});
};
data RemoveFromList w a l = forall lr. MkRemoveFromList
{
listRemoveWitness :: ListType w lr,
listInsert :: a -> lr -> l,
listRemove :: l -> lr
};
removeAllMatching :: (TestEquality w) => w a -> ListType w l -> RemoveFromList w a l;
removeAllMatching _ NilListType = MkRemoveFromList
{
listRemoveWitness = NilListType,
listInsert = \_ -> id,
listRemove = id
};
removeAllMatching wa (ConsListType wb rest) = case removeAllMatching wa rest of
{
MkRemoveFromList wit ins rm -> case testEquality wa wb of
{
Just Refl -> MkRemoveFromList
{
listRemoveWitness = wit,
listInsert = \a l2 -> (a,ins a l2),
listRemove = \(_,l1) -> rm l1
};
Nothing -> MkRemoveFromList
{
listRemoveWitness = ConsListType wb wit,
listInsert = \a (b,l2) -> (b,ins a l2),
listRemove = \(b,l1) -> (b,rm l1)
};
};
};
data RemoveManyFromList wit lx l = forall lr. MkRemoveManyFromList
{
listRemoveManyWitness :: ListType wit lr,
listInsertMany :: lx -> lr -> l,
listRemoveMany :: l -> lr
};
removeAllMatchingMany :: (TestEquality wit) => ListType wit lx -> ListType wit l -> RemoveManyFromList wit lx l;
removeAllMatchingMany NilListType wl = MkRemoveManyFromList
{
listRemoveManyWitness = wl,
listInsertMany = \_ lr -> lr,
listRemoveMany = \l -> l
};
removeAllMatchingMany (ConsListType wa wlx) wl = case removeAllMatching wa wl of
{
MkRemoveFromList wl' ins rm -> case removeAllMatchingMany wlx wl' of
{
MkRemoveManyFromList wl'' insM remM -> MkRemoveManyFromList
{
listRemoveManyWitness = wl'',
listInsertMany = \(a,lx) lr -> ins a (insM lx lr),
listRemoveMany = remM . rm
};
};
};
newtype EitherWitness (w1 :: k -> *) (w2 :: k -> *) (a :: k) = MkEitherWitness (Either (w1 a) (w2 a));
instance (TestEquality w1,TestEquality w2) => TestEquality (EitherWitness w1 w2) where
{
testEquality (MkEitherWitness (Left wa)) (MkEitherWitness (Left wb)) = testEquality wa wb;
testEquality (MkEitherWitness (Right wa)) (MkEitherWitness (Right wb)) = testEquality wa wb;
testEquality _ _ = Nothing;
};
data PartitionList wit1 wit2 l = forall l1 l2. MkPartitionList
{
listPartitionWitness1 :: ListType wit1 l1,
listPartitionWitness2 :: ListType wit2 l2,
listFromPartition :: l1 -> l2 -> l,
listToPartition1 :: l -> l1,
listToPartition2 :: l -> l2
};
partitionList :: ListType (EitherWitness w1 w2) l -> PartitionList w1 w2 l;
partitionList NilListType = MkPartitionList
{
listPartitionWitness1 = NilListType,
listPartitionWitness2 = NilListType,
listFromPartition = \() () -> (),
listToPartition1 = \() -> (),
listToPartition2 = \() -> ()
};
partitionList (ConsListType (MkEitherWitness (Left w1a)) rest) = case partitionList rest of
{
MkPartitionList pw1 pw2 fp tp1 tp2 -> MkPartitionList
{
listPartitionWitness1 = ConsListType w1a pw1,
listPartitionWitness2 = pw2,
listFromPartition = \(a,l1) l2 -> (a,fp l1 l2),
listToPartition1 = \(a,l) -> (a,tp1 l),
listToPartition2 = \(_,l) -> tp2 l
};
};
partitionList (ConsListType (MkEitherWitness (Right w2a)) rest) = case partitionList rest of
{
MkPartitionList pw1 pw2 fp tp1 tp2 -> MkPartitionList
{
listPartitionWitness1 = pw1,
listPartitionWitness2 = ConsListType w2a pw2,
listFromPartition = \l1 (a,l2) -> (a,fp l1 l2),
listToPartition1 = \(_,l) -> tp1 l,
listToPartition2 = \(a,l) -> (a,tp2 l)
};
};
}