Vlákno názorů k článku Práce s nekonečnými sekvencemi v knihovně funcy od Calculon - Pro Waveleta verze v Leanu: structure Sequence (α :...

Pro Waveleta verze v Leanu:

structure Sequence (α : Type u) where
  value : α
  next : α -> α

instance : Stream (Sequence α) α where
  next? seq := some ⟨seq.value, ⟨seq.next seq.value, seq.next⟩⟩

def take (n : Nat) (seq : Sequence α) : Array α := Id.run <| do
  let mut i := 0
  let mut arr := #[]
  for x in seq do
    arr := arr.push x
    i := i + 1
    if i == n then break
  arr

def main : IO Unit := do
  let seq := Sequence.mk ⟨0, 1⟩ fun (x : Nat × Nat) => ⟨x.snd, x.fst + x.snd⟩
  let arr := take 20 seq
  IO.println s!"{arr.map (·.fst)}"

13. 9. 2023, 19:46 editováno autorem komentáře

Fúha, to je na pár riadkoch zadefinovaný komplet vlastný kód...

13. 9. 2023, 21:04 editováno autorem komentáře

Tady je trochu lepší varianta:

structure Sequence (α : Type u) where
  value : α
  next : α  α

instance : Stream (Sequence α) α where
  next? seq := some ⟨seq.value, ⟨seq.next seq.value, seq.next⟩⟩

def take (n : Nat) (seq : Sequence α) : Sigma fun n => Vector n α := Id.run do
  if let isTrue h := n.decEq 0 then return ⟨0, ⟨#[], rfl⟩⟩
  let mut p := #[].toVector
  let push (p : Sigma fun n => Vector n α) (x : α) : Sigma fun n => Vector n α :=
    let ⟨n, v⟩ := p
    let r := v.push x
    ⟨n+1, r⟩
  for x in seq do
    p := push p x
    if let isTrue h := p.snd.size.decEq n then return ⟨n, h  p.snd⟩
  return ⟨p.snd.size, p.snd⟩

def main : IO Unit := do
  let seq := Sequence.mk ⟨0, 1⟩ fun (x : Nat × Nat) => ⟨x.snd, x.fst + x.snd⟩
  let stdin <- IO.getStdin
  IO.print "How many Fibonacci numbers do you want to generate? "
  let some n := (<- stdin.getLine).trim.toNat? | IO.eprintln "You need to enter a natural number."
  let ⟨_, v⟩ := take n seq
  let v := v.map (·.fst)
  IO.println s!"{v}"
  IO.print "Enter the index of an element: "
  let some n := (<- stdin.getLine).trim.toNat? | IO.eprintln "You need to enter a natural number."
  let some n := n.finFromNat? v.size | IO.eprintln "The index is out of bounds."
  IO.println s!"{v.get n}"

Síce to sem asi nepatrí, ale ja som zas pred časom zakopol o toto:

Beyond functional programming: a taste of Verse. Simon Peyton Jones & Tim Sweeney | Lambda Days 2023

https://www.youtube.com/watch?v=OJv8rFap0Nw

Tohle je zajímavý talk. Pamatuju si, že Sweeney delal na tomhle "vlastnim" jazyce, ale pak uz poznali, ze maji limity a potrebovali teorii, tak najmuli Jonese. Problem je že syntakticky to je dost podivne pro vyvojare co jen skriptuji bezne v jinych hernich enginech -- proste funkconalni no. Rozhodne to neco podstatneho resi v jejich domene na kterou je to presne usite. Takze to muze mit i uspech -- narozdil od bambilionu obecnych jazyku. V tomhle je zajimavy treba i GOAL od Naughty Dogs.

Díky, právě jsem začal poslouchat, je to zajímavé.

Jo, vzhledem k tomu, ze Unity is dead, tak se budou muset rekvalifikovat na Unreal a funcionalni programovani. Pokud tedy nemigruji na Godot, coz asi dava vetsi smysl (a je to vic cool). Ale to zase minou to funkcionalni programovani :D

https://www.youtube.com/watch?v=KTWHdLZZdGw

16. 9. 2023, 20:53 editováno autorem komentáře