Funktsionaalprogrammeerimine 2021/22 sügis

9. Praktikum

Selles praktikumis võtame kokku Monaadide teema ja harjutame tüüpimispuude joonistamist lihtsalt tüübitud {$\lambda$}-arvutuses.

Monaadid Idrises

Kõik monaadid peavad olema funktorid. S.t. neil on funktsioon map.

interface Functor f where
    map : (a -> b) -> f a -> f b

Et olla matemaatilises mõttes funktor, peavad kehtima vastavad võrdused. (Ei kontrollita.)

            map id  ==  id
       map (f . g)  ==  map f . map g

Intuitsioon: funktorid on konteinerid, mis ei interakteeru nende sisuga.

Lisaks peavad monaadid olema aplikatiivsed funktorid. Peame saama pure-ga konteinerisse väärtuseid panna. Ning, kui meil on konteiner funktsiooniga ja konteiner argumendiga, peame saama konteineri funktsiooni tulemusega.

interface Functor f => Applicative f where
    pure : a -> f a
    (<*>) : f (a -> b) -> f a -> f b

Peavad kehtima vastavad võrdused. (Ei kontrollita.)

                  pure id <*> v == v
     pure (.) <*> u <*> v <*> w == u <*> (v <*> w)
              pure f <*> pure x == pure (f x)
                   u <*> pure y == pure ($ y) <*> u

Monaad pole mitte ainult aplikatiivne funktor, vaid tal peab olema ka >>= operaator.

interface Applicative m => Monad m where
     (>>=) : m a -> (a -> m b) -> m b

Peavad kehtima vastavad võrdused. (Ei kontrollita.)

               pure a >>= k  ==  k a
               m >>= pure    ==  m
     m >>= (\x => k x >>= h) ==  (m >>= k) >>= h

Intuitsioon: järjestikku täidetavad arvutusmasinad.

Vaatame kiiresti veel ühte "monaadi": Future.

Future

Future on lihtne (ilma sõnumiteta) samaaegse arvutuse primitiiv. Tüüp data Future : Type -> Type on Funktor, Applicative ja Monad. Kasutamiseks tuleb importida System.Future.

Sellel tüübil on lisaks kaks funktsiooni: fork ja await. Hargnemine, mis käivitab samaaegse arvutuse: fork (f x) : Future a, kui (f x) : a. Vastuse ootamine: await y : a, kui y : Future a.

Näide:

     h  (f x)  (g x)

v.s. samaaegne arvutus

     let u = fork (f x) in
     let v = fork (g x) in
     h (await u) (await v)

Future on monaad:

     await (do u <- fork (f x)
               v <- fork (g x)
               pure (h u v))

inetu?

Future on aplikatiivne funktor:

     await (h <$> fork (f x) <*> fork (g x))

Pane tähele, et (<$>) === map

Kui funktsioonid tagastavad Future

     h' <$> f' x <*> g' x

v.s. järjestikune kood

     h  (f x)  (g x)

Ülesanded

Antud järgnev kood:

import System.Future
import System.Clock

time: Lazy a -> IO a
time v = do
    c1 <- clockTime UTC
    let r = v
    c2 <- clockTime UTC
    let d = timeDifference c2 c1
    printLn d
    pure r

longFun' : Int -> Int
longFun' x = if x>20000000 then 1 else longFun' (x+1)

one_long: () -> Int
one_long () = longFun' 0 

two_long: () -> Int
two_long () = longFun' 0 + longFun' 0

ülesanne 1

Muuda longFun' funktsioonis olevat konstanti, et teie arvutis töötaks one_long arvutamine umbes 3 sekundit. Kasutage funktsiooni time.

ülesanne 2

Kasutades Future-eid, implementeeri kolm funktsiooni, mis "paralleliseerivad" two_long arvutust. Funktsioon paralet peaks kasutama let-e ja fork, await funktsioone -- tulemus peaks olema kiirem twolong-st. Funktsioon paramonad kasutagu do-süntaksit, fork, await funktsioone -- tulemus ei pruugi olla kiirem twolong-st. Funktsioon paraapp peaks kasutama <$>, <*>, fork ja await funktsioone -- tulemus peaks olema kiirem twolong-st.

paralet: () -> Int
paralet () = ?q1

paramonad : () -> Int
paramonad () = ?q2

paraapp : () -> Int
paraapp () = ?q3

Tulemusi uurides peaksite saama aru, miks monaadid on "järjestikuse arvutamise mudel". Miks paramonad arvutamist ei paralelliseerinud?

(See arusaamine peaks tekkima iseseisval uurimisel peale praktilist harjutamist. Loengus rääkisime, et see nii on, aga nüüd peaksite sellest tegelikult aru saama. Kui ei saa aru, küsige uuesti!)

Tüüpimispuud

Ülesanded

Joonistage järgnevad tüüpimispuud -- kui võimalik. Mis väärtused tuleb panna lünkadesse? Kui tüüpimispuu on võimatu, kirjeldage põhjust.

1. {$ \{a : \alpha\} \vdash (\lambda x:\alpha. x)\, a :\, ? $}
2. {$ \vdash (\lambda x:\alpha. x\,x)\,(\lambda x:\alpha. x\,x) :\, ? $}
3. {$ \vdash (\lambda x:\alpha,\, y:\alpha\to\beta\to\gamma. (\lambda z:\alpha. y)\,x\,x) :\, ? $}
4. {$ \vdash (\lambda x:\alpha,\, y:\beta, z:\alpha\to(\beta\to\alpha)\to(\beta\to\beta). z\,(\lambda w:\beta. x)\,y) :\, ? $}
5. {$ \vdash \lambda x:\alpha, y:\alpha\to\beta. (\lambda f:(\alpha\to\beta)\to\alpha\to\beta. f)\, y\, x\, :\, ? $}