Vlákno názorů k článku Práce se seznamy v jazyce F# od Calculon - K doplnění, v některých jazycích existují typy pro...

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.