Ce cărți FP mai citiți?


#1

Să zicem așa mai pentru muritori :grinning:

Eu mă chinui cu haskellbook.com ce încă n-am apucat s-o termin din lipsă de timp, și tocmai ce mi-am cumpărat How to Bake Pi că pare interesantă.

În trecut am citit Functional Programming in Scala, destul de greoaie, cu exerciții și incitantă, m-a ținut captivat de subiect, dar se parcurge greu.


#2

HaskellBook este intr-adevar foarte buna, eu asa am invatat Haskell. :+1:

Pentru cine este interesat de partea putin mai teoretica:

  • Category Theory
    • Bartosz Mileski blogs / videos
    • David Spivak videos. Am auzit ca cele doua carti ale lui sunt foarte bune dar nu am apucat sa le citesc (one / two)
  • Type Theory
    • TAPL o reocmand calduros oricui interesat de static typing
    • Type Theory and Formal Proof este un pic formala/dura ca introducere, dar mie mi se pare digerabila dupa TAPL
  • Other
    • Software Foundations este o serie de 3 carti care trec prin Logica, Programming Languages si Program Verification folosind Coq pentru a verifica/demonstra tot ce se poate.

#3

Salutare!

Am citit și eu o bună parte din “How to Bake Pi” și cred că poate fi o introducere mai blândă în lumea categoriilor. Pentru o variantă comprimată, recomand prezentarea Eugenei Cateogry Theory in Life – mi se pare că surprinde ideile esențiale din carte.

Acum parcurg “Seven Sketches in Compositionality” a lui Fong și Spivak, pe care a menționat-o și Vlad. E foarte interesantă, dar crește rapid în dificultate :slight_smile:

De fapt, acum citesc cartea lui Fong și Spivak pentru cursul on-line al lui John C. Baez de Applied Category Theory. Dacă mai e cineva interesat, dați de veste – mi-ar făcea plăcere să am cu cine discuta. Și nu vă faceți griji, nu e prea târziu, abia a introdus categoriile, iar acum se discută despre baze de date! Spre exemplu:

A database schema is really a category, while an actual database is a functor from that category to Set. The database schema has “abstract” objects and morphisms like Employee and WorksIn : Employee → Department, while the functor makes these “concrete”, turning them into actual sets and functions!

P.S.: @cvlad link-ul către TAPL ne întoarce de unde am plecat.


#4

Cred că voiai să-l menționezi pe @cvlad


#5

Da, pe el voiam să-l menționez; scuze, pentru notificare :slight_smile:


#6

Eu n-am mai citit nicio carte strict legată de FP în ultima vreme. Dacă a fost ceva, probabil a fost un paper sau blog post, nu o carte.

Am citit în schimb Thinking Forth, care m-a făcut să-mi pun niște întrebări legate de referential transparency. Forth e un limbaj stack-based (nu poți da nume rezultatelor de apel de funcții, ci sunt împinse într-o stivă numită data stack), care încurarează un stil foarte imperativ (are variabile globale mutabile, pointer arithmetic și manual memory management).

Oricum, ce-mi place la el e stilul compozițional care-l favorizează pentru apelurile de funcții. E practic un limbaj care impune point-free style. Limbajele de tipul ăsta se numesc concatenative, în opoziție cu cele aplicative, iar unele sunt funcționale. Ideea asta face ca Forth să fie un limbaj mai simplu, sintactic, chiar decât orice variantă de Lisp.

Apoi, tot citind despre Forth, care-i cam imperativ, m-am întrebat cum ar arăta un limbaj din ăsta funcțional și cum ai putea verifica că-i chiar funcțional. Iar testul cel mai simplu este cel de referential transparency. De exemplu:

println("foo"); println("foo") // prints twice

E o bucată de cod impură, pentru că nu putem elimina duplicarea codului prin extragerea unui indentificator local fără a schimba semantica programului.

val a = println("foo") // prints once
a; a // does nothing

Acum, prima variantă de mai sus, poate fi scrisă în GForth așa:

/ this is a line comment
s" foo" / pushes "foo" and its length on the stack
2dup    / duplicate the last two stack values, because we need them twice
type    / print "foo" once
type    / print "foo" twice

Iar acum vine partea interesantă. Dat fiind că Forth n-are local variables, cum putem reproduce al doilea snippet de mai sus? După ce m-am gândit un pic, mi-am dat seama că felul în care extragi o variabilă în Forth e să împingi ceva pe stack, apoi apelezi dup (care duplică ultima valoare de pe stack) de un număr de ori, în funcție de numărul de folosiri ale acelei valori. Așadar, primul apel type deja ar fi trebuit să pună o valoare pe stack, deci în loc să apelăm type a doua oară, am fi putut la fel de bine să apelăm dup.

s" foo" / pushes "foo" and its length on the stack
2dup    / duplicate the last two stack values, because we need them twice
type    / print "foo" once
dup     / dupes "foo"'s length, i.e., 3

Evident, în Forth lucrul ăsta nu merge, pentru că type nu este o funcție — nu împinge o valoare pe stack, ci execută un side effect.

Se pot modela efectele într-un mod pur în Forth? Probabil, pentru că are o noține de suspendare de execuție, dar n-am încercat încă. Atunci type ar putea deveni un word (funcție, în terminologia Forth) care împinge valori effectful pe stack, iar la sfârșitul lumii, să ai un alt word care le scoate și le execută pentru side-effects. De-acolo și până la Forth monads, nu mai e decât un pas.


#7

@igstan – mersi pentru postare! Ai încercat vreodată să implementezi un interpretor pentru un limbaj concatenativ? Știu că ai încercat la un moment dat să scrii un compilator de la Scheme la Forth :slight_smile:

De-acolo și până la Forth monads, nu mai e decât un pas.

Pentru monade nu ai avea nevoie de tipuri de date cu kind-ul * -> *? Ai așa ceva în Forth? În principiu, ai putea defini liste sau tuple folosind doar funcții, dar pentru asta e nevoie de higher-order functions. Are Forth higher-order functions?

Care ar fi concluzia – de ce ingrediente avem nevoie pentru a “modela efecte”? Funcții și variabile?


#8

Daca tot vorbim despre asta (type classes), unul ditre creatorii de librarii foarte interesante de PureScript a tinut o prezentare recent la PureScript online meetup care mi s-a parut foarte bine organizat / facut. Practic vorbeste despre code reuse folosind functii, typeclasses si interpretoare, si arata cumva si cum ar putea fi implementate daca nu am avea suport de la compilator (si care ar fi problemele, in cazul asta).

Nu stiu suficiente despre Forth sa imi dau cu parerea, dar poate dupa prezentarea asta iti dai tu seama daca ar merge. Teoretic, poti inlocui (up to a point) typeclasses cu dictionare.

Acum cam jumatate de an a tinut alt talk care poate fi privit ca sequel-ul acestuia (chiar si zice in talk Nate chestia asta). Link-ul este aici:


#9

Typeclasses nu sunt altceva decât un mecanism de a descrie funcții ce pot transforma un nume de tip într-o valoare.

Din cauza asta parametrii “impliciți” din Scala sunt considerați a fi un echivalent, diferența fiind că parametrii impliciți sunt mai flexibili, gen că nu ai reguli de “coherence” (deși din câte am auzit, nici GHC nu face o treabă bună) și că acceptă cu ușurință tipuri cu mai mulți parametrii de tip (e.g. MultiParamTypeClasses este o extensie GHC, dar nu e în Haskell98), plus reguli flexibile dar complexe de rezolvare a conflictelor.

Practic în orice limbaj, dacă introduci parametrii impliciți, obții type classes, pentru că conceptele sunt echivalente. Vor să introducă asta și în OCaml, vezi Modular Implicits.


#10

Pentru mine monadele n-au treabă nici cu higher-kinded types, nici cu type-classes — astea fiind doar niște modalități de a le reprezenta în anumite limbaje.

Forth e untyped, deci implicit nu are nici higher-kinded types, dar are o modalitate de a întârzia execuția unei bucăți de cod — există un word primitiv numit POSTPONE. Un limbaj concatenativ mai modern, Factor, are și el noțiunea asta:

Apare însă o problemă de DX (developer experience) când vrei să scrii cod generic (pentru orice tip algebric) și nu prea ai chef să pasezi acele dicționare de mână. Acolo vrei o noțiune de polymorphism (ad-hoc sau subtyping, poate, dar nu parametric). Dacă n-ai tipuri, poți folosi dynamic dispatch și duck-typing ca să faci dispatch polimorfic la instanța algebrică. E cam hand-wavy ce-am zis, dar n-am timp să scriu niște cod acum (prin care mi-aș valida și eu teoria).

Ah, și ca să răspund la întrebarea ta inițială, @dan.oneata, am un mic playground în lucru unde vreau să experimentez cu un limbaj concatenativ stack-based și unul queue-based (am auzit c-ar avea niște avantaje). Oricum, am introdus un mini-EDSL stack-based într-un proiect la lucru :smiley:

Mă interesează limbajele concatenative pentru modelarea de EDSLs pentru că te lasă să faci “global static analysis” la tot “scripul” embedded. De pildă, dacă ai modela un stack (exemplul meu favorit :P) folosindu-te de state monad, codul ar putea arăta așa:

script = do
  push 1
  push 2
  a <- pop
  b <- pop
  return a + b

Dar asta nu te lasă să “interprezi” printr-un analizor care să-ți zică, de pildă, câte instrucțiuni s-au folosit și care-s alea. Ai putea dacă n-ai avea data dependencies între pași și ai folosi Applicative în loc de Monad (via GHC’ ApplicativeDo language extension).

Dar! Dacă am reprezenta scriptul într-un mod concatenativ, atunci putem avea o privire de ansamblu a scriptului și eventual să-l optimizăm. De exemplu:

data Inst =
    Push Int
  | Exec (Int -> Int -> Int)

-- Note that we don't need to give names to intermediate values, like in
-- monadic, do-notation version.
script = [
  Push 1,
  Push 2,
  Exec (+)
]

Acum avem un DSL care suportă data dependencies (Exec (+) trebuie executat după cele două instrucțiuni Push), însă putem analiza scriptul pentru potențiale optimizări într-un interpretor (batching, instruction reordering, speculative execution, etc.)

Ideea asta se aplică cumva și pentru Arrow type-class. Am citit de curând un articol în care vorbea cineva despre static analysis peste Arrow EDSLs: https://elvishjerricco.github.io/2017/03/10/profunctors-arrows-and-static-analysis.html

Care e de fapt diferența între Arrow și un EDSLs concatenativ, încă nu știu. Sunt curios care-i echivalența dintre operatorii de stack manipulation din Forth sau Factor (swap, dup, rot, etc.) și operatorii din Arrow (&&&, ***). Ăsta-i subject for further research, cum s-ar zice :slight_smile:


#11

Ai putea elabora, te rog, ce înțelegi prin monadă? :stuck_out_tongue:

Pornind de la definiție eu mă gândeam că o monadă e un tuplu de două transformări naturale (funcții) și un functor (un constructor de date), care respectă anumite legi. Dar, într-adevăr, dacă limbajul e untyped (sau uni-typed cum îi numește Harper), atunci există un singur tip U și nu mai avem nevoie de functor la nivel de tipuri (nu ar face decât să-l mapeze pe U la el însuși). În cazul acesta o moandă ar rămâne doar o pereche de funcții:

return :: U -> U
(>>=) :: U -> (U -> U) -> U

De văzut și postarea lui Roman Cheplyaka despre moande în limbajele dinamice.


#12

Evident, după cum mă știi, nu am o definiție așa formală. Intuiția pe care o folosesc e că o monadă te lasă să specifici ordinea și efectele care se întâmplă între computații. E cumva umplutura dintre ; și rândul următor, așa cum zicea Don Stewart. Deci, oricare ar fi limbajul, dacă găsești o posibilitate să instrumentezi două computații în așa fel încât să mai facă și altceva (adică efectul) pe lângă a calcula o valoare, atunci o consider o monadă. Evident, ai nevoie și de noținea de colapsare a două efecte nested (monadic join).

O intuiție alternativă pe care o folosesc e că o monadă mă lasă să fac embed unui limbaj într-un meta-limbaj, cu interleaving al efectelor meta-limbajului printre rezultatele limbajului. Exemplu: stack language (push, pop); meta-language: Haskell; efecte: modificarea unei stări globale relativ la operațiunile limbajului stack.

Cum faci asta? Atunci când scrii codul din limbaj trebuie să lași niște hook points pentru meta-limbaj (specificate de o anumită interfață), prin care hook points poți să interleave efectele de care ziceam.

Nu cred că ajută prea mult ce-am zis eu, dar așa le văd. Iar ceea ce zice Cheplyaka e parțial în asentimentul meu. Mi se pare, însă, că simplificarea aia la forma unityped e un pic cam forțată. Chiar dacă ai un limbaj dinamic/unityped/untyped, tot gândești în termeni de type-constructors.

O să mă mai gândesc la ce-ai zis cu tripla formată din două transformări naturale și un functor — încă n-o pot internaliza, dar sună interesant.


#13
return :: U -> U
(>>=) :: U -> (U -> U) -> U

Definiția asta nu-i corectă, deoarece presupune comportament de “auto flattening”, ceea ce face de fapt Promise-ul din JS, fiind un dezastru din mai multe motive, printre care și asta. Și când spun că nu-i corectă, mă refer la faptul că ar viola legile definite.

De altfel dacă vorbim de un limbaj dinamic, dacă “M a” nu există, atunci nu există nici “U -> U”.
Evident că batem deja câmpii.

Din punct de vedere al “type theory” limbajele dinamice pot fi considerate unityped, dar asta doar din punct de vedere al compilatorului și a ce poți demonstra de la compilare. Tipurile de date însă nu încetează să existe la runtime și faptul că întorci un “M b” sau nu rămâne cât se poate de relevant.


#14

De ce ar viola legile de monadă? Nu este acesta un exemplu care respectă legile?

return x = x
x >>= f = f x

#15

@dan.oneata Nu cred că Id este un exemplu relevant.

Spune-mi de exemplu cum ai defini instanța pt un tip simplu gen List.


#16

Hmmm, cred că înțeleg ce vrei să zici: orice valoare dintr-un limbaj uni-typed nu poate avea decât un singur tip, și anume U. Eu mă gândeam astfel: așa cum Hask e categoria în care obiectele sunt tipuri și morfismele funcții între aceste tipuri, tot așa am putea aveam Unitype să fie categoria cu un singur obiect U și morfisme să fie funcții de la U la U. Deci când am scris f :: U -> U o interpretam ca pe o afirmație în meta-limbaj, în modelul categoric, și nu tipul lui f (care ar fi tot U). Dar e foarte posibil să fie eronat modul acesta de gândire… Dar de ce am recurs la acest model? Pentru a adapta noțiunea de monadă pentru limbajele uni-typed. Eu eram, de fapt, curios care sunt feature-urile minime de limbaj pentru a implementa monade.


#17

Ca să explic — în cazul în care definești instanța așa …

return x = x :: Nil

x >>= f = case x of
  Nil -> Nil
  x :: xs -> f(x) ++ (xs >>= f)

Definiția este incorectă deoarece atunci când afirmi că tipul trebuie să fie U, atunci este forall U. Și apar probleme, cum ar fi că devine legal să faci asta:

list >>= (\x -> x)

Și într-un limbaj ca JavaScript, astfel de legi pot fi testate prin property-based testing, adică jsverify și dacă-i bagi acolo generator pentru orice tip U, implementarea ar fi una incorectă.

O implementare corectă (conform semnăturii descrise), ar fi asta (pseucod, e.g. list mai jos ar trebui să fie un fel de instanceOf, și nu cred că se poate în Haskell):

x >>= f = case x of
  Nil -> Nil
  x :: xs -> 
    case f(x) of
      instanceOf[List] -> list ++ (xs >>= f)
      notList -> notList :: (xs >>= f)

#18

… implementarea asta fiind corectă din punct de vedere al semnăturii, dar nu al legilor.

Cu alte cuvinte faptul că ai “M a -> (a -> M b) -> M b” este în continuare foarte relevant, chiar dacă nu poți da informația asta compilatorului.


#19

Tare mi-e frică că iarăși vorbim despre lucruri diferite; poate ne mai lămurește @igstan ca data trecută :stuck_out_tongue:

În fine, poate e relevant și postul acesta al lui Roman Cheplyaka în care a definit instanțe de monade pentru Reader și Maybe pentru untyped lambda calculus și a demonstrat legile cu pricina. Spre exemplu, pentru Maybe implementarea ar fi:

return x = λj.λn.jx
a >>= k  = λj.λn.a(λx.kxjn)n

#20

Foarte tare definiția, se folosește de Church encoding, e.g:

nothing =    λn.λj.n
   just = λx.λn.λj.j x

Nu mi se pare extraordinal de util, pentru că nu lucrezi cu astfel de codificări în limbajele dinamice, dar e interesant de dezbătut oricum.