{-# OPTIONS --no-termination-check #-}

open import Algebra
open import Prelude

module Hyper.Monadic {m} {๐‘€ : Type m โ†’ Type m} (mon : Monad ๐‘€) where

open Monad mon

_โ†ฌโ€ฒ_ : Type m โ†’ Type m โ†’ Type m
record _โ†ฌ_ (A : Type m) (B : Type m) : Type m

{-# NO_POSITIVITY_CHECK #-}
record _โ†ฌ_ A B where
  inductive; constructor hyp
  infixl 4 _ยท_
  field _ยท_ : B โ†ฌโ€ฒ A โ†’ B
open _โ†ฌ_ public

A โ†ฌโ€ฒ B = ๐‘€ (B โ†ฌ A) โ†’ B

pure : A โ†’ ๐‘€ A
pure = return

_<*>_ : ๐‘€ (A โ†’ B) โ†’ ๐‘€ A โ†’ ๐‘€ B
fs <*> xs = do
  f โ† fs
  x โ† xs
  pure (f x)

infixr 9 _โŠ™_ _โŠ™โ€ฒ_ _โŠ™โ€ณ_
mutual
  _โŠ™โ€ณ_ : B โ†ฌโ€ฒ C โ†’ ๐‘€ (A โ†ฌ B) โ†’ A โ†ฌโ€ฒ C
  (f โŠ™โ€ณ g) k = f โฆ‡ g โŠ™ k โฆˆ

  _โŠ™โ€ฒ_ : B โ†ฌ C โ†’ A โ†ฌโ€ฒ B โ†’ A โ†ฌโ€ฒ C
  (f โŠ™โ€ฒ g) k = f ยท g โŠ™โ€ณ k

  _โŠ™_ : B โ†ฌ C โ†’ A โ†ฌ B โ†’ A โ†ฌ C
  f โŠ™ g ยท k = f ยท g โŠ™โ€ฒ k

_โ—ƒ_ : (A โ†’ B) โ†’ A โ†ฌ B โ†’ A โ†ฌ B
(f โ—ƒ h) ยท k = f (k (return h))

k : A โ†’ B โ†ฌ A
k x ยท _ = x

โ–ณ : (A โ†’ B) โ†’ A โ†ฌ B
โ–ณ f ยท k = f (k (return (โ–ณ f)))

๐•€ : A โ†ฌ A
๐•€ ยท x = x (return ๐•€)

โ–ฝ : A โ†ฌ B โ†’ A โ†’ B
โ–ฝ h x = h ยท ฮป _ โ†’ x


-- run : A โ†ฌ A โ†’ A
-- run x = x ยท ฮป k โ†’ {!k !}