Saizan

module tramp

// we want to use an existential type, but F# makes that complicated so obj it is.
type Tree = | Bind of Tree * (obj -> Tree)
            | Delay of (unit -> Tree)
            | Leaf of obj

type FnStack<'a,'b> = | End of ('a -> 'b) 
                      | Cons of ('a -> Tree) * FnStack<obj,'b>

Saizan

module state =
  type StateM<'s,'a> = abstract Apply : 's  -> ('s -> 'a -> 'r) -> 'r

  let mkStateM (f : 's -> 's * 'a) : StateM<'s,'a> = 
     { new StateM< 's , 'a > with member __.Apply s k =  match f s with (s,a) -> k s a }

  let runStateM (m : StateM<'s,'a>) : 's -> 's * 'a = fun s ->
      m.Apply s (fun s a -> (s,a))

  // defined directly to avoid the value restriction.

Saizan

module Prims where
  primitive
    primLockUniv : Set₁

open Prims renaming (primLockUniv to LockU) public

postulate
  Cl : Set
  k0 : Cl
  Tick : Cl → LockU

Saizan

{-# OPTIONS --cubical #-}
module _ where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels
open import Cubical.HITs.SetTruncation

elimSetTrunc : ∀ {ℓ} (A : Type ℓ) (B : ∥ A ∥₀ → Type ℓ) →
  (f : (a : A) → B (∣ a ∣₀)) →
  (g : (x y : ∥ A ∥₀) → (p q : x ≡ y) →

Saizan

{-# OPTIONS --cubical #-}
module Extension where

open import Agda.Primitive
open import Cubical.Core.Everything
open import Agda.Builtin.Nat

infixr 4 _,,_

record I×_ (A : Setω) : Setω where

Saizan

{-# OPTIONS --type-in-type #-}
module Coden (m : Set → Set) where

open import Category.Functor
open RawFunctor {{...}}

Ran : (K : Set → Set) → Set → Set
Ran K a = (c : Set) → (a → K c) → m c

α : ∀ {a}{K} → Ran K (K a) → m a

Saizan

record SP : Set₁ where
  field
    F    : Set → Set

    mon  : ∀{ρ ρ'} → (ρ → ρ') → (Fρ : F ρ) → F ρ'

    Supp : ∀ {ρ} → F ρ → Set

    mon-Supp : ∀ {ρ ρ'} (f : ρ → ρ') (Fρ : F ρ)
               → Supp (mon f Fρ) → Supp Fρ

Saizan

{-# LANGUAGE KindSignatures #-}
import Bound.Class

{-

What laws should Bound have?

We need at least enough to make sure the typical Monad Exp instances are valid.

Let's start by writing some generic Bound instances.

Saizan

module Impossible where

open import Coinduction
open import Function
open import Data.Empty
open import Data.Conat
open import Data.Bool
open import Data.Maybe using (Maybe; just; nothing)
open import Data.Product
open import Relation.Nullary

Saizan

{-# LANGUAGE GADTs, EmptyDataDecls#-}

module Calculator where

type Stack = [Double]

data Arity = Unary | Binary
data Associativity = Left | Right

data Operator = Operator Arity Associativity