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
- 7.3. Interfaces parameterized by Type -> Type
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
Ü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