Názory k článku Práce se seznamy v jazyce F#

„V první řadě se jedná o typ Option a typ Result, což jsou v podstatě monády”

Hehe

hmm a jsou? wraping+unwraping to ma, ale jestli to staci na zarazeni...

Ale jo, jsou (dá se polemizovat o morfismech), mně se jen líbila ta poznámka za tím ("nelekejte se").

Akorát teda (un)wrapping s tím zařazením nijak nesouvisí.

jj nelekejme se. Možná je teorie okolo monád hodně divoká, ale jejich praktické použití je fajn (jeden z nejlepších návrhových vzorů IMHO).

Zas tak divoká není, jsou horší :)

Myslím, že spíš než seznamy teď ve funkcionálním programování letí pole. Například Lean má #[1, 2, 3] s přístupem O(1).

Nebo vektory v Clojure, kde je pristup nejakych log_32 (N), tedy vlastne taky O(1) :)

Hezký logaritmus.

No v podstate je to plocha struktura a soucasne nabizi rozumne sdileni hodnot (jestli je na Clojure neco elegantniho, tak prave vektory a mapy, jak vypadaji uvnitr).

Umožňuje to structural sharing? Asi předpokládám, že ano.

Má to různé optimalizace. Například l := l.push 1234 prostě jen přidá prvek in situ, pokud na ten seznam existuje jen jedna reference.

K doplnění, v některých jazycích existují typy pro seznamy nebo pole, které staticky kontrolují délku. Idris:

data Vect : Nat -> (a : Type) -> Type where
    Nil : Vect 0 a
    Cons : a -> Vect n a -> Vect (S n) a

Lean:

def Vector (n : Nat) (α : Type u) := { arr : Array α // arr.size = n }

No né, já už to dokážu přečíst. To je super.

K tomu Leanu, to tam museli dávat // ? To tam nemohli dát něco "normálnějšího", třeba čárku nebo středník?

To nevím, asi tam mohli dát něco jiného. V Leanu si člověk může přidat do gramatiky jazyky vlastní pravidla, takže to jde předefinovat.

Akorát si teda nepřej vidět, jak se definuje push nebo set. Nebo co se musí dělat, aby fungovalo pro takové pole "let mut".

Tak po těch letech zdejších "dependent-types" přestřelek se ani nedivím :D

BoneFlute se o to zajímá roky, akorát tehdy ještě nebyl Lean 4, který je přece jen čitelnější (a praktičtější pro běh).

"No né, já už to dokážu přečíst. To je super."

Tady je k tomu pár funkcí.

def Vector (n : Nat) (α : Type u) := { arr : Array α // arr.size = n }

def Vector.get (v : Vector n α) (i : Fin n) : α :=
  v.val.get (v.property.symm  i)

def Vector.set (v : Vector n α) (i : Fin n) (x : α) : Vector n α :=
  let arr := v.val.set (v.property.symm  i) x
  let h := v.val.size_set (v.property.symm  i) x
  ⟨arr, v.property  h⟩

def Vector.push (v : Vector n α) (x : α) : Vector (n+1) α :=
  let arr := v.val.push x
  let h := v.val.size_push x
  ⟨arr, v.property  h⟩

Nie je to náhodou Lean 3? Linter mi nezoberie v.property.symm.

Je to Lean 4, Root umazal trojúhelníčky (tam, kde je dvojí mezera). Je to konstrukce “rewrite x in y” z Idrisu.

27. 9. 2023, 20:00 editováno autorem komentáře

BTW, nechce sa vám k Leanu napísať článok? :)

To by bylo na celou sérii. A je k němu dost dobrá dokumentace.

Doplnenie. Drvivá väčšina funkcií sa nachádza v module List.
https://fsharp.github.io/fsharp-core-docs/reference/fsharp-collections-listmodule.html.

Napr. funkcie pre sortovanie:

let nums = [ -1; 6; -2; 3; 0; -4; 5; 1; 2 ]

nums |> List.sort |> printfn "%A"
nums |> List.sortDescending |> printfn "%A"

nums |> List.sortBy (abs) |> printfn "%A"
nums |> List.sortByDescending (abs) |> printfn "%A"

Na inicializáciu môžeme napríklad použiť List.init.

List.init 5 (fun e -> e * e)

F# má naozaj bohatú syntax na definovanie zoznamov pomocou list comprehensions. Základom sú range a generátory. Môžeme použiť viaceré podmienky a for cykly.

let vals = [ -1; 0; 2; -2; 1; 3; 4; -6 ]

let pos =
    [ for e in vals do
          if e > 0 then yield e ]

printfn "%A" pos

printfn "---------------------------------"

[ for e in 1 .. 100 -> e * e ] |> printfn "%A"


printfn "---------------------------------"

[ for a in 1 .. 100 do
    if a % 3 = 0 && a % 5 = 0 then yield a] |> printfn "%A"

printfn "---------------------------------"

let vals3 =
    [ for x in 1 .. 3 do
          for y in 1 .. 10 -> x, y ]

printfn "%A" vals3

Zvláda to aj vnorené let výrazy.

let vals = [ 1; -2; -3; 4; 5 ]

[ for v in vals do
      let f = fun e -> e > 0
      if f(v) then yield v ] |> printfn "%A"

Dokonca tam môžeme vnoriť aj match pattern.

let res =
    [ for e in 1..100 do
          match e with
          | e when e % 3 = 0 -> yield "fizz"
          | e when e % 5 = 0 -> yield "buzz"
          | e when e % 15 = 0 -> yield "fizzbuzz"
          | _ -> yield (string e) ]


printfn "%A" res

26. 9. 2023, 13:15 editováno autorem komentáře

se mi to libi, je to python-like, ale typove inferovany. nice|

Prostě příčetný zápis. Podobně se pracuje s dataframy.

Poznámka: o speciální případ se zde jedná z toho důvodu, že programovací jazyk F# nedokáže z prázdného seznamu odvodit typ prvků.

Ten typ odvodil, dokáže to. Akorát nějaké hodnoty v F#, OCamlu, Standard ML mají nekonečně mnoho typů, tak kompilátor odvodí ten nejobecnější (všechny ostatní typy z něj jde dostat dosazením za typovou proměnnou).

Podobně třeba pro seznam [None] odvodí 'a option list. Hodnoty, kterými v ML jsou i funkce (nesmí být aplikované) mohou mít generické typy.

26. 9. 2023, 15:39 editováno autorem komentáře

Zajímavé, třeba Rust si umí pomocí unifikace odvodit typy často, ale vždy vyžaduje konkrétní.

Co máš přesně na mysli?

Co píšu, v Rustu je inference typů příkladná, ale všechny typové proměnné musí být vázané.

Jasně, díky za upozornění. Já to myslel tak, že neodvodí konrétní typ prvků, akorát jsem to napsal moc obecně. Ono to není nic proti ničemu, prostě někdy vyjde alfa list atd. a pořád máme možnost to specifikovat explicitně (akorát to prakticky není potřeba).