Agda Typeclasses

sandbox.agda

module src.sandbox where 
    open import Cubical.Data.Sigma
    open import Cubical.Data.Bool

    record Monad (F : Set → Set) : Set₁ where 
        field
            return : ∀ {A} → A → F A
            _>>=_ : ∀{A B} → F A → (A → F B) → F B
        
        _>>_ : ∀{A B} → F A → F B → F B
        x >> y = x >>= λ _ → y
        
    -- notice the curly braces and elipse ...
    -- this allows Monad to be an Instance Argument 
    -- https://agda.readthedocs.io/en/latest/language/instance-arguments.html
    open Monad{{...}}

    data Maybe (A : Set) : Set where 
        just : A → Maybe A 
        none : Maybe A

    State : (S A : Set) → Set
    State S A = S → (A × S)

    -- definine the instances, the type checker will find these "automagically"
    instance 
        maybeMonad : Monad Maybe 
        maybeMonad .return a = just a
        maybeMonad ._>>=_ none f = none
        maybeMonad ._>>=_ (just a) f = f a

        stateMonad : {S : Set} → Monad (State S)
        stateMonad .return a s =  a , s
        stateMonad ._>>=_ st f s = let 
                                     a = fst (st s)
                                     s' = snd (st s) 
                                     b = fst (f a s')
                                     s'' = snd (f a s')
                                    in b , s''

    -- a module that takes in any monad
    -- again curly braces for instance arguments
    module usage {F : Set → Set} {{ M : Monad F }} where

        exampleProgram : F Bool 
        exampleProgram = return true >>= λ b → return (not b)

    -- automatic instance resolution
    _ : Maybe Bool 
    _ = return true

    _ : State Bool Bool 
    _ = return true