{-# 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