Funktsionaalprogrammeerimine 2024/25 sügis

Kodutöö 13 (vabatahtlik)

Selles praktikumis vaatame monaade, nende defineerimist, nende kombineerimist ning nendega programmeerimist.

Enamik allpool toodud koodijuppidest on lahenduste juures vajalikud. Seega kopeerige nad ka oma lahendustesse etteantud järjekorras. Ülesannete lahendustes täitke ära kõik neisse koodijuppidesse jäetud augud.

Loenguslaidid

Näitekood loengust, 2, 3, 4, 5, 6

Lisalugemine (vabatahtlik):

Type-Driven development with Idris peatükid:

• Chapter 7. Interfaces: using constrained generic types, alampeatükid:
  • 7.3. Interfaces parameterized by Type -> Type
    • 7.3.1. Applying a function across a structure with Functor
    • 7.3.2. Reducing a structure using Foldable
    • 7.3.3. Generic do notation using Monad and Applicative

Monaadid ja kõrvalefektidega programmeerimine

Puhta funktsionaalse programmeerimine üks nõrkusi on, et defineeritud programmid käituvad kui matemaatilised funktsioonid, mis iga sisendi jaoks tagastavad täpselt ühe väljundi ilma võimaluseta vigu töödelda, mällu kirjutada või sealt lugeda, sisendit-väljundit kasutada ning mittedeterministlike või tõenäosuslike valikuid teha.

Selliseid programmide (mittematemaatilisi) omadusi nimetatakse üheskoos kõrvalefektideks. Üks viis kuidas kõrvalefekte ning neid sisaldavaid programme modelleerida on kasutada monaade.

Etteantud kood loengust (kopeerida oma lahenduse algusesse):

Monaadide tüübiklassi Monaad definitsioon ning tõestus, et meie defineeritud monaadide tüübiklassi kuuluvusest järeldub ka Idrise sisseehitatud monaadide tüübiklassi Monad kuuluvus, mis võimaldab meil omakorda hiljem kasutada do-notatsiooni.

interface Monaad (0 m : Type -> Type) where
  return : a -> m a
  bind   : m a -> (a -> m b) -> m b

Monaad m => Functor m where
  map f p = bind p (return . f)                      -- : (a -> b) -> m a -> m b

Monaad m => Applicative m where
  pure      = return                                 -- : a -> m a
  (<*>) p q = bind p (\ f => bind q (return . f))    -- : m (a -> b) -> m a -> m b

Monaad m => Monad m where
  (>>=) = bind                                       -- : m a -> (a -> m b) -> m b

Seega võime praktikumi hilisemas osas lugeda (>>=) ja bind kui üksteise sünonüüme. Lisaks on need operatsioonid sünonüümid ka do-notatsioonile (vt 8. praktikumi materjale).

Nagu loenguski, defineerime näited monaadidest kasutades tüübiklassi Monaad, kuna nii väldime kolme eraldi tüübiklassi kuuluvuse näitamise vajalikkust, mida otse Monad'i liikmete defineerimise puhul peaksime tegema.

Ülesanne 1 : Erandeid ja instrumenteerimist kombineeriv monaad (esimene variant)

Loengus näitasime, et eranditega programmide modelleerimiseks sobib Option monaad.

data Option a =
    None
  | Some a

Eq a => Eq (Option a) where
  None   == None   = True
  Some x == None   = False
  None   == Some y = False
  Some x == Some y = x == y

oReturn : a -> Option a
oReturn x = Some x

oBind : Option a -> (a -> Option b) -> Option b
oBind comp f = case comp of
                 None => None
                 Some x => f x

Monaad Option where
  return = oReturn
  bind   = oBind

oThrow : Option a
oThrow = None

Lisaks näitasime, et arvutuste instrumenteerimiseks (näiteks väärtustatud avaldiste arvu lugemiseks) sobib Ctr monaad.

Counter = Int

Ctr' : Type -> Type
Ctr' a = (a , Counter)

data Ctr a = MkCtr (Ctr' a)

cReturn : a -> Ctr a
cReturn x = MkCtr (x , 0)

cBind : Ctr a -> (a -> Ctr b) -> Ctr b
cBind comp f = case comp of
                  MkCtr (x,c1) => case (f x) of
                                    MkCtr (y,c2) => MkCtr (y , c1 + c2)

Monaad Ctr where
  return = cReturn
  bind   = cBind

cCount : Ctr ()
cCount = MkCtr ((), 1)

Käesolevas kodutöö ülesandes on eesmärgiks näidata, et järgmine tüüp OptCtr, mis kombineerib erandeid ning instrumenteerimist, on samuti monaad.

Selleks defineerige vastavad return ja bind operatsioonid. Lisaks defineerige ka veast teatamise, instrumenteerimise operatsioonid ning veatöötluse operatsioonid.

Arvutuslikult kirjeldab OptCtr a programme, mis kas teatavad veast (väärtusega None) või tagastavad paari a-tüüpi väärtusest ja loenduri väärtusest (kujul Some (x,c)).

data OptCtr a = MkOptCtr (Option (a,Counter))

Eq a => Eq (OptCtr a) where
  (MkOptCtr None)         == (MkOptCtr None)          = True
  (MkOptCtr None)         == (MkOptCtr (Some (y,c'))) = False
  (MkOptCtr (Some (x,c))) == (MkOptCtr None)          = False
  (MkOptCtr (Some (x,c))) == (MkOptCtr (Some (y,c'))) = x == y && c == c'

ocReturn : a -> OptCtr a
ocReturn = ?rhs_ocreturn

ocBind : OptCtr a -> (a -> OptCtr b) -> OptCtr b
ocBind = ?rhs_ocbind

Monaad OptCtr where
  return = ocReturn
  bind   = ocBind

ocCount : OptCtr ()
ocCount = ?rhs_occount

ocThrow : OptCtr a
ocThrow = ?rhs_octhrow

ocTryCatch : OptCtr a -> OptCtr a -> OptCtr a
ocTryCatch = ?rhs_octrycatch

Oma koodi võite testida järgmiste võrdustega:

  do {x <- return 4; return x}        == return {m = OptCtr} 4
  do {ocCount; ocCount; return ()}    == do {ocCount; ocCount}
  do {ocCount; ocCount; ocThrow}      == do {ocCount; ocThrow {a = ()}}
  do {ocCount; ocCount; ocThrow}      == ocThrow {a = ()}
  do {ocThrow {a = ()}; ocCount}      == do {ocCount; ocThrow}
  not (do {ocCount; ocCount; ocThrow} == return 4)
  do {ocCount; ocCount; ocThrow}      == do {ocCount; ocCount; ocThrow {a = ()}; ocCount}

  ocTryCatch (do {x <- return 4; return x}) (do {ocCount; return 7})   == return 4
  ocTryCatch (do {ocCount; ocCount; ocThrow}) (do {ocCount; return 7}) == do {ocCount; return 7}

Ülesanne 2 : Erandeid ja instrumenteerimist kombineeriv monaad (teine variant)

Eelmises ülesandes defineeritud monaad OptCtr on üks kahest loomulikust viisist erandite ning instrumenteerimise monaadide kombineerimiseks.

Kui eelmises ülesandes defineeritud monaad unustab erandi tõstatamisel loenduri väärtuse ära, siis selles ülesandes defineerige monaad OptCtr', mis erandi tõstatamisel tagastab erinevalt esimesest ülesandest ka selleks hetkeks arvutatud loenduri väärtuse.

Vihjeks vaadake, et mis tüüpi väärtusi peavad kolmandas ülesandes defineeritavad funktsioonid returnValue' ja numberOfExps' tagastama.

data OptCtr' a = ?rhs_optctr_teine

Eq a => Eq (OptCtr' a) where
  x == y     = ?rhs_optctr_eq_teine

ocReturn' : a -> OptCtr' a
ocReturn' = ?rhs_ocreturn_teine

ocBind' : OptCtr' a -> (a -> OptCtr' b) -> OptCtr' b
ocBind' = ?rhs_ocbind_teine

Monaad OptCtr' where
  return = ocReturn'
  bind   = ocBind'

ocCount' : OptCtr' ()
ocCount' = ?rhs_occount_teine

ocThrow' : OptCtr' a
ocThrow' = ?rhs_octhrow_teine

ocTryCatch' : OptCtr' a -> OptCtr' a -> OptCtr' a
ocTryCatch' = ?rhs_octrycatch_teine

Oma koodi võite testida järgmiste võrdustega:

  do {x <- return 4; return x}           == return {m = OptCtr'} 4
  do {ocCount'; ocCount'; return ()}     == do {ocCount'; ocCount'}
  not (do {ocCount'; ocCount'; ocThrow'} == do {ocCount'; ocThrow' {a = ()}})
  not (do {ocCount'; ocCount'; ocThrow'} == ocThrow' {a = ()})
  not (do {ocThrow' {a = ()}; ocCount'}  == do {ocCount'; ocThrow'})
  not (do {ocCount'; ocCount'; ocThrow'} == return 4)
  do {ocCount'; ocCount'; ocThrow'}      == do {ocCount'; ocCount'; ocThrow' {a = ()}; ocCount'}

  ocTryCatch' (do {x <- return 4; return x}) (do {ocCount'; return 7})      == return 4
  ocTryCatch' (do {ocCount'; ocCount'; ocThrow'}) (do {ocCount'; return 7}) == do {ocCount'; ocCount'; ocCount'; return 7}

Ülesanne 3 : Aritmeetiliste avaldiste väärtustamine veatöötluse ja instrumenteerimisega

Selles ülesandes defineerime esimeses kahes ülesandes defineeritud monaade kasutades aritmeetiliste avaldiste väärtustamise, mis toetab nii erandeid kui ka väärtustatud avaldiste arvu lugemist.

Esmalt aritmeetiliste avaldiste tüüp ja mõned näited aritmeetilistest avaldistest.

infixl 10 :+:, :-: 
infixl 11 :*:, :/:

data Expr = Num Int
          | (:+:) Expr Expr
          | (:-:) Expr Expr
          | (:*:) Expr Expr
          | (:/:) Expr Expr

exp1 : Expr
exp1 = Num 1 :+: Num 2

exp2 : Expr
exp2 = Num 2 :*: (Num 4 :-: Num 1)

exp3 : Expr
exp3 = Num 4 :*: Num 3 :/: Num 2

exp4 : Expr
exp4 = Num 4 :*: Num 3 :/: (Num 2 :-: Num 2)

Teiseks defineerime monaadide alamklassi, mis toetavad nii erandite tõstatamist, nende töötlemist kui ka instrumenteerimist. Nii saame allpool eval funktsiooni defineerida iga monaadi jaoks, mis toetab count, throw ja tryCatch operatsioone.

interface Monaad m => CountThrowTryCatchMonaad m where
  count : m ()
  throw : m a
  tryCatch : m a -> m a -> m a

CountThrowTryCatchMonaad OptCtr where
  count = ocCount
  throw = ocThrow
  tryCatch = ocTryCatch

CountThrowTryCatchMonaad OptCtr' where
  count = ocCount'
  throw = ocThrow'
  tryCatch = ocTryCatch'

Defineerige eval funktsioon, mis väärtustab etteantud aritmeetilise avaldise, loeb kokku väärtustatud tehete arvu ning tõstatad erandi kui peaks toimuma nulliga jagamine.

Monaadiliste programmide defineerimisel, nagu näiteks eval puhul, proovige võimalikult palju kasutada do-notatsiooni (vt loenguslaide ja Idrise näiteid loengust).

eval : CountThrowTryCatchMonaad m => Expr -> m Int
eval = ?rhs_eval

Näidete ja testide käivitamiseks defineerige ka järgmised funktsioonid, mis tagastavad esimeses ja teises ülesandes defineeritud monaadide jaoks arvutuste lõplikud väärtused ja loendurid.

returnValue : OptCtr a -> Option a
returnValue = ?rhs_returnvalue

numberOfExps : OptCtr a -> Option Counter
numberOfExps = ?rhs_numberofexps

returnValue' : OptCtr' a -> Option a
returnValue' = ?rhs_returnvalue_teine

numberOfExps' : OptCtr' a -> Counter
numberOfExps' = ?rhs_numberofexps_teine

Oma koodi võite testida järgmiste võrdustega:

  returnValue (eval exp1) == Some 3
  returnValue (eval exp2) == Some 6
  returnValue (eval exp3) == Some 6
  returnValue (eval exp4) == None

  numberOfExps (eval exp1) == Some 1
  numberOfExps (eval exp2) == Some 2
  numberOfExps (eval exp3) == Some 2
  numberOfExps (eval exp4) == None

  returnValue' (eval exp1) == Some 3
  returnValue' (eval exp2) == Some 6
  returnValue' (eval exp3) == Some 6
  returnValue' (eval exp4) == None

  numberOfExps' (eval exp1) == 1
  numberOfExps' (eval exp2) == 2
  numberOfExps' (eval exp3) == 2
  numberOfExps' (eval exp4) == 2

Ülesanne 4 : Erandite monaaditeisendaja

Selles ülesandes näitame, et esimeses ülesandes defineeritud erandite ja instrumenteerimise monaadide kombinatsioon pole õnnelik juhus.

Nimelt näidake, et OptionT võimaldab meil iga monaadi m kombineerida Option monaadiga ning konstrueerida uue kombineeritud monaadi OptionT m.

Sellist operatsiooni, mis etteantud monaadist konstrueerib talle struktuuri lisades uue monaadi, nimetatakse monaaditeisendajaks (ingl monad transformer). Esimeses ülesandes defineeritud monaad on näide sellest konstruktsioonist, kui valime m = Ctr ehk kui kasutame konstrueeritud monaadi OptionT Ctr.

data OptionT : (Type -> Type) -> Type -> Type where
  MkOptionT : m (Option a) -> OptionT m a

omReturn : Monaad m => a -> OptionT m a
omReturn = ?rhs_omreturn

omBind : Monaad m => OptionT m a -> (a -> OptionT m b) -> OptionT m b
omBind = ?rhs_ombind

Monaad m => Monaad (OptionT m) where
  return = omReturn
  bind   = omBind

Lisaks saame näidata, et iga monaadi m abil modelleeritud arvutus on ka monaadi OptionT m abil modelleeritud arvutus ning et ka OptionT m monaadis on võimalik erandeid tõstatada.

omLift : Monaad m => m a -> OptionT m a
omLift = ?rhs_omlift

omThrow : Monaad m => OptionT m a
omThrow = ?rhs_omthrow

Näidete ja testide jaoks kopeerige oma koodi ka järgnev tõestus, et List on samuti Monaad. Arvutuslikus mõttes modelleerib List monaad mittedeterministlikke arvutusi, kus iga arvutuse lõpptulemuseks on hulk/loend kõigist võimalikest väärtustest, mida antud arvutus mittedeterministlikult tagastaks.

Monaad List where
  return = \ x => [x]
  bind   = listBind

Nii saame näidetes ja testides kasutada konkreetset monaadi OptionT List. Selle monaadi jaoks saame defineerida operatsiooni choose, mis intuitiivselt käivitab mittedeterministlikult ühe etteantud erandeid kasutatavatest Option a arvutustest.

choose : List (Option a) -> OptionT List a
choose xs = MkOptionT xs

Oma koodi võite testida järgmiste võrdustega:

  let _ = the (do {x <- choose [oReturn 3 , oThrow , oReturn 7]; return (x * x)}                   = choose [oReturn 9 , oThrow , oReturn 49]) Refl in True
  let _ = the (do {omThrow {a = ()}; x <- choose [oReturn 3 , oThrow , oReturn 7]; return (x * x)} = choose [oThrow]) Refl in True
  let _ = the (do {x <- choose [oReturn 3 , oThrow , oReturn 7]; omThrow {a = ()}; return (x * x)} = choose [oThrow , oThrow , oThrow]) Refl in True

Kuna me pole näidanud, et OptionT kuulub Eq tüübiklassi, siis kasutame == asemel võrdusliku tõestamise võrdust =. Selliste testide üldkuju on järgmine: kui tahame testida sama tüüpi programmide foo ja bar võrdust, siis kirjutame

  let _ = the (foo = bar) Refl in True

kus True tagastatakse ainult juhul kui foo ja bar arvutuvad mõlemad samaks lõpptulemuseks.

Tärnülesanne : 2. ülesandele vastav monaaditeisendaja

Kellele monaaditeisendajad rohkem huvi pakuvad võivad nuputada ja proovida Idrises näidata, et kas 2. ülesandes konstrueeritud monaad OptCtr' on ka mõne üldise monaaditeisendaja näide.

Ülesanne 5 : Muudetavate muutujatega puude peal arvutamine

Selles ülesandes tuletame meelde loengus nähtud muudetavate muutujatega programmeerimise olekumonaadi abil ning kasutame seda monaadi puude andmestruktuuride peal (imperatiivseks) arvutamiseks

data Vars = X | Y | Z

Eq Vars where
  X == X = True
  X == _ = False
  Y == Y = True
  Y == _ = False
  Z == Z = True
  Z == _ = False

State : Type
State = Vars -> Int

lookup : Vars -> State -> Int
lookup x s = s x

update : Vars -> Int -> State -> State
update x i s y = if x == y then i else s y

St' : Type -> Type
St' a = State -> (a,State)

data St : Type -> Type where
  MkSt : St' a -> St a

sReturn : a -> St a
sReturn x = MkSt (\ s => (x,s))

sBind : St a -> (a -> St b) -> St b
sBind f g = MkSt (\ s => case f of 
                           MkSt f' => case f' s of
                                        (x,s') => case g x of
                                                    MkSt g' => g' s')

Monaad St where
  return = sReturn
  bind   = sBind

prefix 8 ^!
(^!) : Vars -> St Int
(^!) x = MkSt (\ s => (lookup x s,s))

infix 7 ^=
(^=) : Vars -> Int -> St ()
(^=) x i = MkSt (\ s => ((),update x i s))

run : St a -> State -> (a,State)
run (MkSt f) s = f s

stateToList : State -> List Int
stateToList s = [s X , s Y , s Z]

runToList : St a -> State -> (a,List Int)
runToList f s = let (x,s') = run f s in (x, stateToList s')

Lisaks defineerime kahendpuude tüübi, kus igas tipus hoitakse muutuja ja täisarvu paari.

data Tree =
    Leaf
  | Node Tree Vars Int Tree

Defineerige olekumonaadi St ning temaga seotud operatsioone kasutades funktsioon, mis liidab iga muutuja kohta kokku kõik vastavad väärtused puud tippudes ning lisab saadud summa algolekus sellele muutujale vastavale väärtusele.

sumVars : Tree -> St ()
sumVars = ?rhs_sumvars

Näidete ja testide jaoks lisage oma koodi ka kaks näidisalgolekut ja kaks näidispuud:

initialState1 : Vars -> Int
initialState1 X = 0
initialState1 Y = 0
initialState1 Z = 0

initialState2 : Vars -> Int
initialState2 X = 3
initialState2 Y = 5
initialState2 Z = 7

tree1 : Tree
tree1 = Node (Node (Node Leaf Z 5 Leaf) X 2 (Node Leaf Y 7 Leaf)) Y 1 (Node Leaf Z 9 (Node Leaf X 5 Leaf)) 

tree2 : Tree
tree2 = Node (Node (Node Leaf Y 5 Leaf) X 2 Leaf) Z 1 (Node Leaf X 9 (Node Leaf X 5 Leaf)) 

Oma koodi võite testida järgmiste võrdustega:

  runToList (sumVars Leaf) initialState1 == ((),[0,0,0])
  runToList (sumVars Leaf) initialState2 == ((),[3,5,7])
  runToList (sumVars tree1) initialState1 == ((),[7,8,14])
  runToList (sumVars tree1) initialState2 == ((),[10,13,21])

  runToList (do {sumVars tree1; sumVars tree2}) initialState1 == ((),[23,13,15])
  runToList (do {sumVars tree1; sumVars tree2}) initialState2 == ((),[26,18,22])

Ülesanne 6 : Olekumonaaditeisendaja

Selles ülesandes näitame, et sarnaselt Option monaadiga, saab ka olekumonaade iga teise monaadiga kombineerida. Selleks defineerige allpool olev monaaditeisendaja StateT.

Lisaks defineerige globaalse oleku lugemise operatsioon sttGet, globaalse oleku asendamise/kirjutamise operatsioon sttSet ning monaadis m olevate arvutuste tõstmine monaadis StateT m s olevateks arvutusteks.

StateT' : (Type -> Type) -> Type -> Type -> Type
StateT' m s a = s -> m (a,s)

data StateT : (Type -> Type) -> Type -> Type -> Type where
  MkStateT : StateT' m s a -> StateT m s a

sttReturn : Monaad m => a -> StateT m s a
sttReturn = ?rhs_sttreturn

sttBind : Monaad m => StateT m s a -> (a -> StateT m s b) -> StateT m s b
sttBind = ?rhs_sttbind

Monaad m => Monaad (StateT m s) where
  return = sttReturn
  bind   = sttBind

sttGet : Monaad m => StateT m s s
sttGet = ?rhs_stget

sttSet : Monaad m => s -> StateT m s ()
sttSet s = ?rhs_stset

sttLift : Monaad m => m a -> StateT m s a
sttLift = ?rhs_sttlift

Selgituseks, et tüüpides StateT' ja StateT tähistab parameeter s kasutatavate olekute tüüpi. Teisisõnu, nagu loengus mainitud, võib olekumonaadi olekute tüübiks olla ükskõik milline tüüp---tüüp s ei pea toetama mingeid lisaoperatsioone.

Oma koodi võite testida järgmiste võrdustega:

  let _ = the (do {_ <- sttGet; return 4}           = return {m = StateT List Int} 4) Refl in True
  let _ = the (do {_ <- sttGet; sttSet 7; return 4} = do {sttSet 7; return {m = StateT List Int} 4}) Refl in True
  let _ = the (do {sttSet 5; sttSet 7; return 4}    = do {sttSet 7; return {m = StateT List Int} 4}) Refl in True
  let _ = the (do {s <- sttGet; sttSet s; return 4} = return {m = StateT List Int} 4) Refl in True
  let _ = the (do {sttSet 4; s <- sttGet; return s} = do {sttSet 4; return {m = StateT List Int} 4}) Refl in True

Lisaülesanded

Ülesanne 7 : Erandite ja olekumonaadide kombineerimine

Selles ülesandes kasutame eelmises ülesandes defineeritud monaaditeisendajat StateT selleks, et kombineerida erandite monaadi ja olekumonaadi.

Täpsemalt defineerige monaad T, mis kombineerib erandid ja oleku kasutamise. Lisaks defineerige oleku kasutamise (muutujate väärtuste lugemise ja kirjutamise), erandite tõstatamise ning erandite töötlemise operatsioonid.

Kus võimalik, ärge kasutage funktsioonide defineerimisel tüübi T sisemist struktuuri vaid kasutage hoopis tema Monaad olemise omadust ja sellega kaasnevat do-notatsiooni kasutamise võimalust. Kasuks võivad tulla ka nende osamonaadide operatsioonid, millest monaad T on konstrueeritud.

T : Type -> Type
T a = ?rhs_t

prefix 8 ^^!
(^^!) : Vars -> T Int
(^^!) x = ?rhs_tread

infix 7 ^^=
(^^=) : Vars -> Int -> T ()
(^^=) x i = ?rhs_twrite

tThrow : T a
tThrow = ?rhs_tthrow

tTryCatch : T a -> T a -> T a
tTryCatch = ?rhs_ttrycatch

Lõpetuseks defineerige ka tRunToList funktsioon, mis võimaldab T monaadiga modelleeritud arvutusi algolekust alates jooksutada ning mis samal ajal teisendab lõppoleku muutujate lõppväärtuste loendiks (vt ka runToList ülal).

tRunToList : T a -> State -> Option (a , List Int)
tRunToList = ?rhs_truntolist

Oma koodi võite testida järgmiste võrdustega:

  tRunToList (do {X ^^= 4; Y ^^= 8}) initialState1                         == Some ((), [4, 8, 0])
  tRunToList (do {x <- ^^! X; Y ^^= 8 + x}) initialState2                  == Some ((), [3, 11, 7])
  tRunToList (do {x <- ^^! X; tThrow {a = ()}; Y ^^= 8 + x}) initialState2 == None

  tRunToList (tTryCatch (do {x <- ^^! X; Y ^^= 8 + x}) (Z ^^= 42)) initialState2                  == Some ((), [3, 11, 7])
  tRunToList (tTryCatch (do {x <- ^^! X; tThrow {a = ()}; Y ^^= 8 + x}) (Z ^^= 42)) initialState2 == Some ((), [3, 5, 42])

Ülesanne 8 : Erandite ja olekumonaadi kombinatsiooniga puude peal arvutamine

Defineerime kahendpuude tüübi, kus igas tipus on laiendatud muutujate ja väärtuste paar.

data Tree' =
    Leaf'
  | Node' Tree' (Option Vars) Int Tree'

Me kasutame siin Option tüüpi, et lisada muutujate hulka üks uus muutuja. Varasemalt kasutatud muutujad tüübist Vars on nüüd kujul Some v ning see uus muutuja on kujul None.

Nüüd, kasutades eelmises ülesandes defineeritud monaadi T, defineerige järgmiselt käituv funktsioon maxVars:

• funktsioon külastab kõiki puu tippe
• funktsioon tagastab igale muutujale vastava suurima väärtuse, kui see on algolekus olevast vastavast väärtusest suurem
• kui puus esineb muutujatest X, Y, Z erinev muutuja, siis funktsioon tõstatab erandi

maxVars : Tree' -> T ()
maxVars = ?rhs_maxvars

Näidete ja testide jaoks lisage oma koodi järgmised kaks puud.

tree1' : Tree'
tree1' = 
  Node' 
    (Node' (Node' Leaf' (Some Y) 5 Leaf') None 2 Leaf') 
    (Some Z) 1 
    (Node' Leaf' (Some X) 9 (Node' Leaf' (Some X) 5 Leaf')) 

tree2' : Tree'
tree2' =
  Node' 
    (Node' (Node' Leaf' (Some Y) 5 Leaf') (Some X) 2 Leaf') 
    (Some Z) 1 
    (Node' Leaf' (Some X) 9 (Node' Leaf' (Some X) 5 Leaf')) 

Oma koodi võite testida järgmiste võrdustega:

  tRunToList (maxVars tree1') initialState1 == None
  tRunToList (maxVars tree2') initialState1 == Some ((), [9, 5, 1])
  tRunToList (maxVars tree2') initialState2 == Some ((), [9, 5, 7])

Ülesanne 9 : Erandite monaadi seadused

Viimases ülesandes seome monaadide temaatika tõestamisega Idrises.

Esmalt defineerime monaadide alamklassi, kus olevad monaadid peavad ka monaadide seadusi rahuldama.

interface Monaad m => SeadustegaMonaad m where

  leftUnitLaw      : (x : a) 
                  -> (f : a -> m b) 
                  --------------------------------
                  -> do {x <- return x; f x} = f x

  rightUnitLaw     : (comp : m a) 
                   ---------------------------------
                  -> do {x <- comp; return x} = comp

  associativityLaw : (comp : m a)
                  -> (f : a -> m b)
                  -> (g : b -> m c)
                  -----------------------------------------------------------------------
                  -> do {y <- (do {x <- comp; f x}); g y} = do {x <- comp; y <- f x; g y}

Tõestage, et erandite monaadi Option jaoks kehtivad monaadide seadused.

SeadustegaMonaad Option where
  leftUnitLaw = ?rhs_leftunitlaw
  rightUnitLaw = ?rhs_rightunitlaw
  associativityLaw = ?rhs_associativitylaw

Tärnülesanne : Teiste monaadide seadused

Kellele monaadide seaduste tõestamine rohkem huvi pakub võivad proovida neid tõestada ka teiste loengus ja selles kodutöös konstrueeritud monaadide jaoks.

Näiteks võite proovida tõestada monaadide seadused loengus nähtud Ctr monaadi jaoks. Kuna Ctr on defineeritud kasutades Idrise sisseehitatud Int tüüpi ning liitmisoperatsiooni sellel, mis on defineeritud sisseehitatud FFI funktsiooni prim__add_Int kasutades, siis peate eeldama selle funktsiooni jaoks oodatud monoidi omadused:

prim__add_Int_lunit : (i : Int) -> prim__add_Int 0 i = i
prim__add_Int_runit : (i : Int) -> prim__add_Int i 0 = i
prim__add_Int_assoc : (i,j,k : Int) 
                   -> prim__add_Int (prim__add_Int i j) k 
                    = prim__add_Int i (prim__add_Int j k)

Alternatiivselt võite te defineerida Ctr monaadi variandi, mis kasutab Int asemel Nat tüüpi, mille puhul saate vastavad liitmise omadused induktsiooniga tõestada.

Ülesanne 10 : Monaadid monoididena endofunktorite kategoorias

Kui te FP keeltes monaadidega rohkem programmeerite, siis kuulete te kindlasti ühel hetkel ütlemist "monaad pole mitte midagi muud, kui monoid endofunktorite kategoorias".

Selles ülesandes näidake, et loengus ja ülesannetes kasutatud bind operatsioonil põhinevast monaadide esitusest järeldub monoidi korrutisel põhinev monaadide esitus ning vastupidi.

bindToMu : {m : Type -> Type} 
        -> (forall a. a -> m a) 
        -> (forall a,b. m a -> (a -> m b) -> m b) 
        -> m (m a) -> m a
bindToMu return bind = ?rhs_bindtomu

muToBind : Functor m 
        => (forall a. a -> m a) 
        -> (forall a. m (m a) -> m a) 
        -> m a -> (a -> m b) -> m b
muToBind eta mu = ?rhs_mutobind

Nimelt monaadide monoididel põhinevas esituses on nõutud, et monaad m on lisaks Functor ning et ta toetab bind operatsiooni asemel binaarset korrutamise operatsiooni mu : m (m a) -> m a, kokkuvõtvalt:

interface Functor m => Monaad' m where
  eta : a -> m a
  mu  : m (m a) -> m a