Je Rust jazyk budoucnosti?

[listoper]

Ma Guarded patterns a destructuring (aspon ve switch):
...

No.. slušelo by se říct, že je to "preview feature" v nejnovější JDK 19 (tj. běžně se to zatím použít nedá a možná to nakonec ani nebude vypadat takhle) a funguje to jenom na recordy a jen ve switchi (což jsi teda napsal) - ve srovnání s tím, co umí třeba jenom Scala, je to stále úsměvný. Btw vůbec nechápu, proč je tam ten Supplier, zbytečně to ten příklad komplikuje, proč to neni jenom

Jo pravda... nedavno sem si tim hral a mezitim sem zapomel, ze mam zapnute preview features.
Nicmene s tim when je to uz asi treti verze preview (predtim bylo myslim &&) tak uz docela verim, ze to tak zustane...

Ty lambdy jsem tam dal, protoze je to expression switch a ja chtel ukazat ze na zaklade pattern matchingu muzu volat funkce a ne jen vracet string...

A ten pattern matching funguje ne jen na recordy:

Kód: [Vybrat]

        var objs = Arrays.asList(
                Optional.of("some string"),
                Optional.of(10),
                Optional.empty()
        );

        objs.stream()
                .map(i -> switch (i){
                    case Optional o when o.isPresent() && o.get() instanceof String -> "I have a string";
                    case Optional o when o.isPresent() && o.get() instanceof Integer -> "I have an Integer";
                    default -> "I don't know what I have";
                })
                .forEach(System.out::println);

Ten destructuring zatim as ano, ale support je taky na ceste

[Reklama]

[Idris]

Jsou náročné na čas výpočtu v době překladu, za běhu ne.

Ano, ano, sorry.
A platí o opak, že za běhu by to mělo být rychlejší […] teoreticky. Což je taky smutné - takovej nevyužitej potenciál.

Tohle mi vrtalo hlavou, tak jsem zkusil kus reálně používaného kódu přepsat do (čistě funkcionálního) Leanu a ejhle, jsme s rychlostí na úrovni Rustu. Není to sice (formálně mnohem silnějším) typovým systémem, ale to by bylo nadlouho.

Jestli ses na Lean zatím nekoukal, tak doporučuji aspoň letmé seznámeni. Má například “locally imperative code blocks”

[Idris]

Jsou náročné na čas výpočtu v době překladu, za běhu ne.

Ano, ano, sorry.
A platí o opak, že za běhu by to mělo být rychlejší […] teoreticky. Což je taky smutné - takovej nevyužitej potenciál.

Tohle mi vrtalo hlavou, tak jsem zkusil kus reálně používaného kódu přepsat do (čistě funkcionálního) Leanu a ejhle, jsme s rychlostí na úrovni Rustu. Není to sice (formálně mnohem silnějším) typovým systémem, ale to by bylo nadlouho.

Jestli ses na Lean zatím nekoukal, tak doporučuji aspoň letmé seznámeni. Má například “locally imperative code blocks”

Doplnění: V Idrisu jsem doimplementoval FBIP pro pole a hurá sláva, rychlost se limitně blíží verzi v Leanu. Ten Chez je fakt raketa No nic, dám si Guinness a pak jdu slavit

[Králík]

A ten kus kódu by byl?

[APhacker_mob]

A ten kus kódu by byl?

 Toho se od Idrise nedockas.

[Reklama]

[Idris]

A ten kus kódu by byl?

Kód: [Vybrat]

inductive Edge : Type where
| mkEdge : Nat -> Nat -> String -> Nat -> List Edge -> Edge

def Edge.left : Edge -> Nat
| mkEdge left _ _ _ _ => left

def Edge.right : Edge -> Nat
| mkEdge _ right _ _ _ => right

def Edge.category : Edge -> String
| mkEdge _ _ category _ _ => category

def Edge.level : Edge -> Nat
| mkEdge _ _ _ level _ => level

def Edge.children : Edge -> List Edge
| mkEdge _ _ _ _ children => children

partial def Edge.tree (edge : Edge) : String :=
  edge.category ++
  if edge.children.isEmpty then "" else
  "(" ++ (edge.children.map fun e => e.tree).foldl (fun x y => x ++ (if x == "" then "" else ",") ++ y) "" ++ ")"

structure Chart where
  edges : Array (List Edge)

def mkChart (len : Nat) : Chart := { edges := mkArray len [] }

def addEdge (chart : Chart) (edge : Edge) : Chart :=
  let idx := edge.left
  { chart with edges := chart.edges.set! idx (edge :: chart.edges[idx]!) }

def addEdges (chart : Chart) : List Edge -> Chart
| [] => chart
| e :: es => addEdges (addEdge chart e) es

structure Rule where
  lhs : String
  rhs : List String

mutual
  partial def applyRule'' (lhs : String) (rhs : List String) (chart : Chart) (start : Nat) (maxLevel : Nat) (children : List Edge) (edge : Edge) (level : Nat) : List Edge :=
    match rhs with
    | r :: rs =>
      if r == edge.category then
        let maxLevel := if edge.level > maxLevel then edge.level else maxLevel
        if rs == [] then
          if maxLevel == level then
            [.mkEdge start edge.right lhs (level+1) children.reverse]
          else []
        else if edge.right < chart.edges.size then
          applyRule' lhs rs chart chart.edges[edge.right]! start maxLevel children level
        else []
      else []
    | [] => []

  partial def applyRule' (lhs : String) (rhs : List String) (chart : Chart) (edges : List Edge) (start : Nat) (maxLevel : Nat) (children : List Edge) (level : Nat) : List Edge :=
    match edges with
    | [] => []
    | e :: es => applyRule'' lhs rhs chart start maxLevel (e :: children) e level ++ applyRule' lhs rhs chart es start maxLevel children level
end

partial def applyRule (rule : Rule) (chart : Chart) (idx : Nat) (level : Nat) : List Edge :=
  if idx == chart.edges.size then [] else
  applyRule' rule.lhs rule.rhs chart chart.edges[idx]! idx 0 [] level ++ applyRule rule chart (idx+1) level

def applyRules'' (rules : List Rule) (chart: Chart) (level : Nat) : List Edge :=
  match rules with
  | [] => []
  | r :: rs => applyRule r chart 0 level ++ applyRules'' rs chart level

partial def applyRules' (rules : List Rule) (chart: Chart) (level : Nat) : Chart :=
  let newEdges := applyRules'' rules chart level
  if newEdges.isEmpty then chart else applyRules' rules (addEdges chart newEdges) (level+1)

def applyRules (rules : List Rule) (chart: Chart) : Chart :=
  applyRules' rules chart 0


[Králík]

Dík, ale myslel jsem spíš v Rustu.

Jinak nedávno kolega v práci ukazoval zajímavou vlastnost const funkcí v Rustu - je možné v nich psát asserty, a tím pádem staticky verifikovat některé invarianty. Ukazoval, že může vytvořit pole statické velikosti, protlačit to skrz nějaký 3rd party kód jako slice (dynamická velikost) a na druhém konci zkonvertovat zpátky na původní typ (konstantní velikost), s tím, že kompilátor velikost ověří staticky, nemusí se dělat runtime check.

[Idris]

Jinak nedávno kolega v práci ukazoval zajímavou vlastnost const funkcí v Rustu - je možné v nich psát asserty, a tím pádem staticky verifikovat některé invarianty. Ukazoval, že může vytvořit pole statické velikosti, protlačit to skrz nějaký 3rd party kód jako slice (dynamická velikost) a na druhém konci zkonvertovat zpátky na původní typ (konstantní velikost), s tím, že kompilátor velikost ověří staticky, nemusí se dělat runtime check.

No vidíš, to je přesně ono, ověřování invariantů. Rozdíl je jen v tom, že v jazycích jako Idris či Lean (nebo SPARK, ale tam se používá jiná metoda) překladač provede verifikace při překladu (nemusí se dělat runtime check), i když velikost není konstantní. (Už to asi nechceme hlouběji rozebírat, ale umožňují to sigma typy. Jinak jo, v Rustu se dá s generickými parametry taky dělat psí kusy a časem třeba přidají i něco à la Lean, nejen typy, ale i plnohodnotnou funkcionální sémantiku - Swift už ji nějakou dobu má, takže je ověřené, že to jde i v tomto typu jazyků.)

[Idris]

P.S. BTW zajímalo by mne, zda by šlo v Rustu nějak zprovoznit toto: https://ericniebler.com/2013/07/16/f-algebras-and-c/ 

[Králík]

No vidíš, to je přesně ono, ověřování invariantů. Rozdíl je jen v tom, že v jazycích jako Idris či Lean (nebo SPARK, ale tam se používá jiná metoda) překladač provede verifikace při překladu (nemusí se dělat runtime check), i když velikost není konstantní. (Už to asi nechceme hlouběji rozebírat, ale umožňují to sigma typy. Jinak jo, v Rustu se dá s generickými parametry taky dělat psí kusy a časem třeba přidají i něco à la Lean, nejen typy, ale i plnohodnotnou funkcionální sémantiku

Tak počítám, že tohle by se dalo udělat i s dynamickým polem, ono je celkem jedno, jak ten invariant vyrobim. Ale nezkoušel jsem si to zatim. Jo, vim co jsou dependent types. U Rustu postup směrem k něčemu takovému nebo k HKTs moc nečekej, přeci jen, je to jazyk určený pro reálný, praktický engineering, ne pro postgraduální bádání apod. Když už, tak se spíš teď mudruje nad efekty, resp. specificky control-flow efekty, kvůli error handlingu, generátorům, async streamům apod. Opět ale nečekej nějaký těžce obecný systém, pravděpodobně by to přinejlepším byl opět nějaký subset, se zaměřením na zero-costness, ergnomii a nepříliš strmou učící křivku spíš než krásy typových systémů.

Swift už ji nějakou dobu má, takže je ověřené, že to jde i v tomto typu jazyků.

Jakou featuru Swiftu máš na mysli? Jinak Swift není stejný typ jazyka, nezaměřuje se na zero-cost abstrakce, má runtime, OOP s implicitním dynamic dispatchem,...

P.S. BTW zajímalo by mne, zda by šlo v Rustu nějak zprovoznit toto: https://ericniebler.com/2013/07/16/f-algebras-and-c/ 

Čistě typovým systémem by to drhlo, v Rustu neuděláš ekvivalent template<template<typename> class F>
struct Fix, takže by se musela třeba napsat nějaká traita a tu pak implementovat pro typy, které bys chtěl fixovat.  S makrama by to mělo být bez problému. Ono koneckonců v tom C++ je to trochu švindl, protože ty templaty jsou duck typing, žejo...

[Králík]

Jo a taky lepší podpora self-referential types - to by Rustu pomohlo víc než jakékoli další FP featury...

[Idris]

Jakou featuru Swiftu máš na mysli?

Myslel jsem klasický FBIP. Ale v Rustu by to asi nebylo žádné terno, když nad tím tak přemýšlím.

[Idris]

P.S. BTW zajímalo by mne, zda by šlo v Rustu nějak zprovoznit toto: https://ericniebler.com/2013/07/16/f-algebras-and-c/ 

Čistě typovým systémem by to drhlo, v Rustu neuděláš ekvivalent template<template<typename> class F>
struct Fix

Jasně, to je právě HKT. Tak ale možná přes GAT?

[Idris]

Jo a taky lepší podpora self-referential types - to by Rustu pomohlo víc než jakékoli další FP featury...

Nejsou tohle náhodou induktivní typy?

[Idris]

Jo, vim co jsou dependent types. U Rustu postup směrem k něčemu takovému nebo k HKTs moc nečekej, přeci jen, je to jazyk určený pro reálný, praktický engineering

Jasně, to je fajn, Rust je poměrně low level, má svou upřednostňovanou oblast nasazení, ale když už má třeba GAT, což je docela šílenost, tak k lepšímu typovému systému je už jen malý krůček. Například Lean se překládá do C++, proč by se nemohl překládat do Rustu?