{-# OPTIONS --without-K #-}

module Dialogue.Core where

open import Basis

-- An EscardΓ³ dialogue, representing a functional on a space whose
-- neighborhoods are lists of Y.
data π”ˆ (X Y Z : Set) : Set where
  -- return x means that the result is x.
  return
    : Z
    β†’ π”ˆ X Y Z

  -- ask i m means that we request the ith element x of the choice sequence
  -- and proceed with 𝓭 x.
  ask
    : X
    β†’ (Y β†’ π”ˆ X Y Z)
    β†’ π”ˆ X Y Z


-- In the normalized (Brouwerian) version of the dialogue tree, queries are
-- given in order.
data 𝔅 (Y Z : Set) : Set where
  -- Ξ· x means that the result is x.
  spit
    : Z
    β†’ 𝔅 Y Z

  -- ϝ 𝓭 means that we request the *current* element x of the choice sequence
  -- and proceed with 𝓭 x.
  bite
    : (Y β†’ 𝔅 Y Z)
    β†’ 𝔅 Y Z


private
  variable {X Y} : Set

  π”ˆ-bind : {A B : Set} β†’ (A β†’ π”ˆ X Y B) β†’ π”ˆ X Y A β†’ π”ˆ X Y B
  π”ˆ-bind f (return x) = f x
  π”ˆ-bind f (ask i m) = ask i Ξ» x β†’ π”ˆ-bind f (m x)

  π”ˆ-bind/ρ : {A : Set} (m : π”ˆ X Y A) β†’ π”ˆ-bind return m ≑ m
  π”ˆ-bind/ρ (return x) = refl
  π”ˆ-bind/ρ (ask i m) =
    ≑.cong
     (ask i)
     (funext Ξ» x β†’
      π”ˆ-bind/ρ (m x))

  π”ˆ-bind/Ξ± : {A B C : Set} {f : A β†’ π”ˆ X Y B} {g : B β†’ π”ˆ X Y C} (m : π”ˆ X Y A) β†’ π”ˆ-bind g (π”ˆ-bind f m) ≑ π”ˆ-bind (π”ˆ-bind g ∘ f) m
  π”ˆ-bind/Ξ± (return x) = refl
  π”ˆ-bind/Ξ± (ask i m) =
    ≑.cong
     (ask i)
     (funext Ξ» x β†’
      π”ˆ-bind/Ξ± (m x))

instance
  π”ˆ-monad : Monad (π”ˆ X Y)
  Monad.ret π”ˆ-monad = return
  Monad.bind π”ˆ-monad = π”ˆ-bind
  Monad.law/Ξ» π”ˆ-monad = refl
  Monad.law/ρ π”ˆ-monad = π”ˆ-bind/ρ
  Monad.law/Ξ± π”ˆ-monad = π”ˆ-bind/Ξ±


private
  variable Z W : Set

-- An EscardΓ³ dialogue may be run against a choice sequence.
π”ˆ[_β‹„_] : π”ˆ X Y Z β†’ (X β†’ Y) β†’ Z
π”ˆ[ return x β‹„ Ξ± ] = x
π”ˆ[ ask i m β‹„ Ξ± ] =
  π”ˆ[ m (Ξ± i) β‹„ Ξ± ]


-- A Brouwerian dialogue may be run against a choice sequence.
𝔅[_β‹„_] : 𝔅 Y Z β†’ (β„• β†’ Y) β†’ Z
𝔅[ spit x β‹„ Ξ± ] = x
𝔅[ bite m β‹„ Ξ± ] = 𝔅[ m (Ξ± 0) β‹„ (Ξ± ∘ suc) ]


generic : π”ˆ X Y X β†’ π”ˆ X Y Y
generic m = do
  i ← m
  ask i ret

module ⊒ where
  β‹„-extensional
    : (m : π”ˆ X Y Z)
    β†’ {Ξ± Ξ² : X β†’ Y}
    β†’ (βˆ€ i β†’ Ξ± i ≑ Ξ² i)
    β†’ π”ˆ[ m β‹„ Ξ± ] ≑ π”ˆ[ m β‹„ Ξ² ]

  β‹„-extensional (return _) _ =
    refl

  β‹„-extensional (ask i m) {Ξ±} {Ξ²} h =
    ≑.seq
     (β‹„-extensional (m (Ξ± i)) h)
     (≑.cong
      (Ξ» β–  β†’ π”ˆ[ m β–  β‹„ Ξ² ])
      (h i))

  β‹„-natural
    : (f : Z β†’ W)
    β†’ (m : π”ˆ X Y Z)
    β†’ (Ξ± : X β†’ Y)
    β†’ f π”ˆ[ m β‹„ Ξ± ] ≑ π”ˆ[ map f m β‹„ Ξ± ]

  β‹„-natural f (return x) Ξ± =
    refl

  β‹„-natural f (ask _ m) Ξ± =
    β‹„-natural f (m _) Ξ±


  β‹„-commutes-with-bind
    : {m : Z β†’ π”ˆ X Y W}
    β†’ (n : π”ˆ X Y Z)
    β†’ (Ξ± : X β†’ Y)
    β†’ π”ˆ[ m π”ˆ[ n β‹„ Ξ± ] β‹„ Ξ± ] ≑ π”ˆ[ (n >>= m) β‹„ Ξ± ]

  β‹„-commutes-with-bind (return _) _ =
    refl

  β‹„-commutes-with-bind (ask _ m) Ξ± =
    β‹„-commutes-with-bind (m _) Ξ±


  generic-diagram
    : (Ξ± : X β†’ Y)
    β†’ (m : π”ˆ X Y X)
    β†’ Ξ± π”ˆ[ m β‹„ Ξ± ] ≑ π”ˆ[ generic m β‹„ Ξ± ]

  generic-diagram Ξ± (return x) =
    refl

  generic-diagram Ξ± (ask _ m) =
    generic-diagram Ξ± (m _)