module Examples.Lam where

open import Data.Product
open import Data.Sum
open import Data.Unit
open import Data.Empty
open import Data.Bool hiding (T)
open import Data.Maybe
open import Function
open import Relation.Binary.PropositionalEquality

open import Data.Container as Cont
open import Data.Container.Combinator hiding (id; _∘_)


open import Prelude Set (λ A B → B -> A) (λ c → id) (λ f g → g ∘ f)

open import Uniform.posIR Set (λ A B → B -> A) (λ c → id) (λ f g → g ∘ f)
open import Uniform.Intro Set (λ A B → B -> A) (λ c → id) (λ f g → g ∘ f)

open import Examples.NestedTypes

-- Identity functor as a container
I : Cont
I = Data.Container.Combinator.id

-- Maybe functor as a container
M : Cont
M = Bool ▷ (λ x → if x then ⊥ else ⊤)

fromMaybe : {X : Set} -> Maybe X -> Cont.⟦ M ⟧ X
fromMaybe (just x) = false , (λ _ → x)
fromMaybe nothing = true , (λ ())

-- Lambda terms as a nested type
LamN : Nest
LamN = K I ⊞ (Id ⊠ Id) ⊞ (Id ⊛ K M)

-- and their interpretation via initial algebras of IR+
Lam : Set -> Set
Lam = Cont.⟦ U ⟪ LamN ⟫IR ▷ T ⟧

-- the expected constructors are definable (the terms look noisy
-- because of the coproduct encoding):

var : {A : Set} -> A -> Lam A
var a = (intro (true , true , _ , (λ ()) , (λ ()) , _ , _)) , (λ _ → a)

app : {A : Set} -> Lam A -> Lam A -> Lam A
app f s
 = (intro (true , false , _ , (λ _ → proj₁ f) , (λ _ → proj₁ s) , _ , _)) ,
   (λ { (inj₁ x) → proj₂ s x ; (inj₂ y) → proj₂ f y })

abs : {A : Set} -> Lam (Maybe A) -> Lam A
abs t
 = intro (false , _ , _ , (λ _ → proj₁ t) , (λ ()) , (proj₁ ∘ t') , _) ,
   (λ x → proj₂ (t' (proj₁ x)) (proj₂ x))
    where t' = fromMaybe ∘ (proj₂ t)