{-# LANGUAGE AllowAmbiguousTypes #-} module Pandora.Paradigm.Structure.Interface.Dictionary where import Pandora.Pattern.Category ((/)) import Pandora.Paradigm.Controlflow.Effect.Interpreted (run) import Pandora.Paradigm.Schemes.TU (type (<:.>)) import Pandora.Paradigm.Structure.Ability.Morphable (Morphable (Morphing), Morph (Lookup), morph) type Dictionary f t = Morphable (Lookup f) t lookup :: forall f k t u a . (Dictionary f t, Morphing (Lookup f) t ~ ((->) k <:.> u)) => k -> t a -> u a lookup :: k -> t a -> u a lookup k key t a xs = TU Covariant Covariant ((->) k) u a -> ((->) k :. u) := a forall (t :: * -> *) a. Interpreted t => t a -> Primary t a run (TU Covariant Covariant ((->) k) u a -> ((->) k :. u) := a) -> TU Covariant Covariant ((->) k) u a -> ((->) k :. u) := a forall (m :: * -> * -> *). Category m => m ~~> m / t a -> Morphing ('Lookup f) t a forall k (f :: k) (t :: * -> *). Morphable f t => t ~> Morphing f t morph @(Lookup f) t a xs (((->) k :. u) := a) -> ((->) k :. u) := a forall (m :: * -> * -> *). Category m => m ~~> m / k key discover :: forall f k v t u a . (Dictionary f t, Morphing (Lookup f) t ~ ((->) (v k) <:.> u)) => v k -> t a -> u a discover :: v k -> t a -> u a discover v k keys t a xs = TU Covariant Covariant ((->) (v k)) u a -> ((->) (v k) :. u) := a forall (t :: * -> *) a. Interpreted t => t a -> Primary t a run (TU Covariant Covariant ((->) (v k)) u a -> ((->) (v k) :. u) := a) -> TU Covariant Covariant ((->) (v k)) u a -> ((->) (v k) :. u) := a forall (m :: * -> * -> *). Category m => m ~~> m / t a -> Morphing ('Lookup f) t a forall k (f :: k) (t :: * -> *). Morphable f t => t ~> Morphing f t morph @(Lookup f) t a xs (((->) (v k) :. u) := a) -> ((->) (v k) :. u) := a forall (m :: * -> * -> *). Category m => m ~~> m / v k keys