Je Rust jazyk budoucnosti?

[BoneFlute]

Chceš na to ještě nějak navázat? Otázky k tomuto konkrétnímu příkladu?

Kód: [Vybrat]

data IsEven : Nat -> Type where
    ZIsEven  : IsEven 0
    SuccSuccIsEven : IsEven n -> IsEven (n+2)


sumx : IsEven -> IsEven -> IsEven
-- sumx : Int -> Int -> Int
sumx x y = x * y


main : IO ()
main = putStrLn $ "Hello: " ++ (show (sumx 2 4))

Ještě mi něco schází vědět?: "Mismatch between: Nat -> Type and Type."

[Reklama]

[BoneFlute]

Takže ve výsledku jsem fanoušek přístupu, kdy se abstrakce vyvíjí trochu pomaleji, návrh jazyka zůstává nohama trochu více na zemi* a zároveň s tím se vyvíjí rovnou i schopnost produkovat pokudmožno optimální kód pro reálná CPU, protože to umožňuje ty zkušenosti s generováním strojového kódu reflektovat do návrhu těch abstrakcí, do návrhu IR reprezentací atd.

To je jen jedna metrika: optimalizovaný kód. Java nám ale kdysi ukázala, že v mnoha případech po optimalizovaném kódu na rychlost není taková poptávka jak bychom si možná přály. Zatímco po bezpečné kódu ano (Scala). A abych byl hodně cynický, tak ona možná není nijak zvláštní poptávka ani po bezpečném kódu (Clojure, C#, JS) 

[Idris]

Kód: [Vybrat]

data IsEven : Nat -> Type where
    ZIsEven  : IsEven 0
    SuccSuccIsEven : IsEven n -> IsEven (n+2)

sumx : IsEven -> IsEven -> IsEven
-- sumx : Int -> Int -> Int
sumx x y = x * y

main : IO ()
main = putStrLn $ "Hello: " ++ (show (sumx 2 4))
Ještě mi něco schází vědět?: "Mismatch between: Nat -> Type and Type."

IsEven musí mít typový parametr. A je to jen kontrakt, že ten parametr je sudé číslo. Nějak takto to bude fungovat:

Kód: [Vybrat]

data IsEven : Nat -> Type where
    ZIsEven  : IsEven 0
    SuccSuccIsEven : IsEven n -> IsEven (2+n)

sumx : (n : Nat) -> {auto 0 prf1 : IsEven n} -> (m : Nat) -> {auto 0 prf2 : IsEven m} -> Nat
sumx n m = n + m


[BoneFlute]

IsEven musí mít typový parametr. A je to jen kontrakt, že ten parametr je sudé číslo. Nějak takto to bude fungovat:

Kód: [Vybrat]

data IsEven : Nat -> Type where
    ZIsEven  : IsEven 0
    SuccSuccIsEven : IsEven n -> IsEven (2+n)

sumx : (n : Nat) -> {auto 0 prf1 : IsEven n} -> (m : Nat) -> {auto 0 prf2 : IsEven m} -> Nat
sumx n m = n + m


No tak to je teda hnusný zápis  Pak mi musíš vysvětlit, proč to tam je.

Bohužel: "Can't find an implementation for IsEven 2."

[Idris]

IsEven musí mít typový parametr. A je to jen kontrakt, že ten parametr je sudé číslo. Nějak takto to bude fungovat:

Kód: [Vybrat]

data IsEven : Nat -> Type where
    ZIsEven  : IsEven 0
    SuccSuccIsEven : IsEven n -> IsEven (2+n)

sumx : (n : Nat) -> {auto 0 prf1 : IsEven n} -> (m : Nat) -> {auto 0 prf2 : IsEven m} -> Nat
sumx n m = n + m


No tak to je teda hnusný zápis  Pak mi musíš vysvětlit, proč to tam je.

Bohužel: "Can't find an implementation for IsEven 2."

Jakou máš verzi Idrisu? Funguje to v 0.6.0.

[Reklama]

[Králík]

Co znamená ta 0 mezi `auto` a jménem implicitního argumentu?

[Idris]

Co znamená ta 0 mezi `auto` a jménem implicitního argumentu?

To je multiplicita (viz kvantitativní typový systém). Nula znamená erasure

[Idris]

Co znamená ta 0 mezi `auto` a jménem implicitního argumentu?

https://idris2.readthedocs.io/en/latest/tutorial/multiplicities.html

[BoneFlute]

IsEven musí mít typový parametr. A je to jen kontrakt, že ten parametr je sudé číslo. Nějak takto to bude fungovat:

Kód: [Vybrat]

data IsEven : Nat -> Type where
    ZIsEven  : IsEven 0
    SuccSuccIsEven : IsEven n -> IsEven (2+n)

sumx : (n : Nat) -> {auto 0 prf1 : IsEven n} -> (m : Nat) -> {auto 0 prf2 : IsEven m} -> Nat
sumx n m = n + m


No tak to je teda hnusný zápis  Pak mi musíš vysvětlit, proč to tam je.

Bohužel: "Can't find an implementation for IsEven 2."

Jakou máš verzi Idrisu? Funguje to v 0.6.0.

idris2 --version # 0.6.0
Z idris2-0.6.0.tgz, stažený z webu, kompiluju na Fedoře.

[Idris]

IsEven musí mít typový parametr. A je to jen kontrakt, že ten parametr je sudé číslo. Nějak takto to bude fungovat:

Kód: [Vybrat]

data IsEven : Nat -> Type where
    ZIsEven  : IsEven 0
    SuccSuccIsEven : IsEven n -> IsEven (2+n)

sumx : (n : Nat) -> {auto 0 prf1 : IsEven n} -> (m : Nat) -> {auto 0 prf2 : IsEven m} -> Nat
sumx n m = n + m


No tak to je teda hnusný zápis  Pak mi musíš vysvětlit, proč to tam je.

Bohužel: "Can't find an implementation for IsEven 2."

Jakou máš verzi Idrisu? Funguje to v 0.6.0.

idris2 --version # 0.6.0
Z idris2-0.6.0.tgz, stažený z webu, kompiluju na Fedoře.

Tam ten kód funguje, zkus to zkopírovat ještě jednou do zdrojáku.

[BoneFlute]

Tam ten kód funguje, zkus to zkopírovat ještě jednou do zdrojáku.

Kód: [Vybrat]

SuccSuccIsEven : IsEven n -> IsEven (2+n) -- fungujeversus

Kód: [Vybrat]

SuccSuccIsEven : IsEven n -> IsEven (n+2) -- nefunguje

Tak mám spousta více či méně blbejch otázek:

1/ proč tam musím uvádět {auto 0 prf1 : IsEven n} ?
2/ proč je to mezi šipkama? Ta funkce má jen tři parametry, ne pět.
3/ co to vlastně to {auto 0 prf1 : IsEven n} říká?
4/ proč tam ten prf1 musí být, když tam nikde nefiguruje? Proč musí být různý? prf1 a prf2

[Králík]

No, a já se zajímám, kde ta hranice je.

Jo takhle V pohodě, už chápu, hmm, ale je to široká otázka... Ale zkusim...

Memory leakům Rust obecně nezabrání. Zajistit invarianty jako třeba to sudé číslo nebo neprázdný string bude umět pomocí newtype, tj. asi podobně jako Haskell. Podstatné omezení aktuálního Rustu je, že nemá specializaci generik. Pracuje se na tom, existují experimentální implementace a minimální subset, který je i celkem použitelný, ale není to hotové a plně sound.

Přemýšlím, co dál, mám nějak komentovat async Rust? Pozitivum určitě je, že async podpora je celkem minimální, definuje pouze základní typy pro reprezentaci asnyc funkcí (semi-korutin) a runtimes jsou pak implementované v externích knihovnách.

Docela cool featura jsou proc-makra, tj. efektivně plugin do kompilátoru, který je použitelný jako jakákoli knihovna. Proc-makrem se dá udělat hodně... Tady je příklad, kde proc-macro během překladu parsuje a verifikuje SQL kód.

To je jen jedna metrika: optimalizovaný kód. Java nám ale kdysi ukázala, že v mnoha případech po optimalizovaném kódu na rychlost není taková poptávka jak bychom si možná přály. Zatímco po bezpečné kódu ano (Scala). A abych byl hodně cynický, tak ona možná není nijak zvláštní poptávka ani po bezpečném kódu (Clojure, C#, JS) 

Ano, přesně tak, je to jedna metrika a můj osobní pohled... Nemám v úmyslu ho vydávat za obecně závazný

[Králík]

Co znamená ta 0 mezi `auto` a jménem implicitního argumentu?

To je multiplicita (viz kvantitativní typový systém). Nula znamená erasure

Aha, ok. Dalo by se to principelně doplnit syntaxí s anonymním argumentem, něco jako `auto _ : IsEven n`? Anonymní arugment by nešlo ve funkci použít, tj. efektivně multiplicita 0. Edit: Resp. asi lepší syntaxe by byla `auto 0: IsEven n`.

[Idris]

Co znamená ta 0 mezi `auto` a jménem implicitního argumentu?

To je multiplicita (viz kvantitativní typový systém). Nula znamená erasure

Aha, ok. Dalo by se to principelně doplnit syntaxí s anonymním argumentem, něco jako `auto _ : IsEven n`? Anonymní arugment by nešlo ve funkci použít, tj. efektivně multiplicita 0. Edit: Resp. asi lepší syntaxe by byla `auto 0: IsEven n`.

Jo, to jde.

[Idris]

Tak mám spousta více či méně blbejch otázek:

1/ proč tam musím uvádět {auto 0 prf1 : IsEven n} ?
2/ proč je to mezi šipkama? Ta funkce má jen tři parametry, ne pět.
3/ co to vlastně to {auto 0 prf1 : IsEven n} říká?
4/ proč tam ten prf1 musí být, když tam nikde nefiguruje? Proč musí být různý? prf1 a prf2

1. To jsou prerekvizity, které chceš (sudost argumentů). To "auto" znamená, že si to má překladač ověřit sám.
2. To je jen konvence, implicitní parametry můžou být kdekoliv. Ta funkce má dva parametry a dvě prerekvizity.
3. IsEven n říká, že n je zaručeně sudé. A prf1/prf2 je prostě jméno té prerekvizity.
4. Jsou různé, protože máš dva vstupní parametry, které chceš mít sudé. Být tam musí, aby sis vynutil tu sudost (kdyby se to nepředávalo, na vstupu by mohlo být libovolné číslo).

Kdybych tam cpal čísla ze vstupu, musel bych si to ověření sudosti (prfX) vyrobit sám a předat ho explicitně.