Je Rust jazyk budoucnosti?

Idris

  • *****
  • 2 286
    • Zobrazit profil
    • E-mail
Re:Je Rust jazyk budoucnosti?
« Odpověď #300 kdy: 05. 12. 2022, 18:36:48 »
Typ chovající se jako funkce. Tomu rozumím. Jak se to liší a v čem je to podobné proti průmyslovým generikám:
Kód: [Vybrat]
type IsEven<T> where T is Nat
?
P.S. Tady bych ještě dodal, že Nat je induktivní typ, což třeba C++ vůbec nemá, takže rozdíl pod pokličkou je. Ale pro programátora se to tváří jako stejná věc.
Buď prosím vysvětli, proč je to zajímavé, že je to induktivní typ, nebo, pokud si myslíš, že to není tak podstatné pro vysvětlení, tak se můžeme přesunout dál.
Domnívám se, že to zajímavé je, protože Nat je součtový typ, takže to je, jako kdyby ten typový parametr byl enum (je to diskrétní typ se dvěma konstruktory). Kdyby to byl Int, bylo by možných hodnot nekonečně mnoho.


BoneFlute

  • *****
  • 1 983
    • Zobrazit profil
Re:Je Rust jazyk budoucnosti?
« Odpověď #301 kdy: 05. 12. 2022, 18:49:08 »
Typ chovající se jako funkce. Tomu rozumím. Jak se to liší a v čem je to podobné proti průmyslovým generikám:
Kód: [Vybrat]
type IsEven<T> where T is Nat
?
P.S. Tady bych ještě dodal, že Nat je induktivní typ, což třeba C++ vůbec nemá, takže rozdíl pod pokličkou je. Ale pro programátora se to tváří jako stejná věc.
Buď prosím vysvětli, proč je to zajímavé, že je to induktivní typ, nebo, pokud si myslíš, že to není tak podstatné pro vysvětlení, tak se můžeme přesunout dál.
Domnívám se, že to zajímavé je, protože Nat je součtový typ, takže to je, jako kdyby ten typový parametr byl enum (je to diskrétní typ se dvěma konstruktory). Kdyby to byl Int, bylo by možných hodnot nekonečně mnoho.

Rozumím. Důsledky mi dochází. Děkuji. Můžem pokračovat.


Idris

  • *****
  • 2 286
    • Zobrazit profil
    • E-mail
Re:Je Rust jazyk budoucnosti?
« Odpověď #302 kdy: 05. 12. 2022, 18:52:24 »
Typ chovající se jako funkce. Tomu rozumím. Jak se to liší a v čem je to podobné proti průmyslovým generikám:
Kód: [Vybrat]
type IsEven<T> where T is Nat
?
P.S. Tady bych ještě dodal, že Nat je induktivní typ, což třeba C++ vůbec nemá, takže rozdíl pod pokličkou je. Ale pro programátora se to tváří jako stejná věc.
Buď prosím vysvětli, proč je to zajímavé, že je to induktivní typ, nebo, pokud si myslíš, že to není tak podstatné pro vysvětlení, tak se můžeme přesunout dál.
Domnívám se, že to zajímavé je, protože Nat je součtový typ, takže to je, jako kdyby ten typový parametr byl enum (je to diskrétní typ se dvěma konstruktory). Kdyby to byl Int, bylo by možných hodnot nekonečně mnoho.
Rozumím. Důsledky mi dochází. Děkuji. Můžem pokračovat.
Fajn. Takže ten první konstruktor, řekněme ZIsEven, je typu IsEven 0. To je zřejmé, ne?

A ten druhý konstruktor má argument typu IsEven, jeho typ je
Kód: [Vybrat]
SuccSuccIsEven : IsEven n -> IsEven (n+2)
Jasné zatím? Otázky?

BoneFlute

  • *****
  • 1 983
    • Zobrazit profil
Re:Je Rust jazyk budoucnosti?
« Odpověď #303 kdy: 05. 12. 2022, 19:07:33 »
Fajn. Takže ten první konstruktor, řekněme ZIsEven, je typu IsEven 0. To je zřejmé, ne?

A ten druhý konstruktor má argument typu IsEven, jeho typ je
Kód: [Vybrat]
SuccSuccIsEven : IsEven n -> IsEven (n+2)
Jasné zatím? Otázky?

Jasné. Chápu-li to správně, tak se to samozřejmě bude chovat rekurzivně, etc. Tak?

Komplet zápis takto?
Kód: [Vybrat]
data IsEven : Nat -> Type where
    ZIsEven  : IsEven 0
    SuccSuccIsEven : IsEven n -> IsEven (n+2)

Říkáš, že Nat je Součtový (diskrétní) typ, takže tam nemůže být nekonečně mnoho čísel. Takže je nějak definováno něco jako NatMax, NatMin? Tedy mohu klidně používat normálně Int, protože stejně ten Int není nekonečnej, ale nějakej automaticky zvětšující Number už bych použít nemohl... Tak?

Ten Type je zadrátovaný klíčový slovo/typ?

Idris

  • *****
  • 2 286
    • Zobrazit profil
    • E-mail
Re:Je Rust jazyk budoucnosti?
« Odpověď #304 kdy: 05. 12. 2022, 19:23:33 »
Kód: [Vybrat]
SuccSuccIsEven : IsEven n -> IsEven (n+2)
Jasné zatím? Otázky?
Jasné. Chápu-li to správně, tak se to samozřejmě bude chovat rekurzivně, etc. Tak?
Jo, tento konstruktor je rekurzivní.

Komplet zápis takto?
Kód: [Vybrat]
data IsEven : Nat -> Type where
    ZIsEven  : IsEven 0
    SuccSuccIsEven : IsEven n -> IsEven (n+2)
Ano.

Říkáš, že Nat je Součtový (diskrétní) typ, takže tam nemůže být nekonečně mnoho čísel. Takže je nějak definováno něco jako NatMax, NatMin?
Nejmenší hodnota je nula, ale jinak to omezené není, těch hodnot je nekonečně (spočetně) mnoho, právě díky rekurzi toho druhého konstruktoru.

Ten Type je zadrátovaný klíčový slovo/typ?
Jo, ten je zvláštní, protože typů pro typy by mělo být nekonečně mnoho (aby nedošlo k něčemu na způsob Russellova paradoxu), jenže zrovna Idris si tu typovou úroveň odvodí sám. Například Lean ji potřebuje explicitně. Nicméně pro naše příklady to není podstatné, je to prostě zabudovaný typ (a slouží také k deklaraci HKT).


BoneFlute

  • *****
  • 1 983
    • Zobrazit profil
Re:Je Rust jazyk budoucnosti?
« Odpověď #305 kdy: 05. 12. 2022, 19:28:13 »
Říkáš, že Nat je Součtový (diskrétní) typ, takže tam nemůže být nekonečně mnoho čísel. Takže je nějak definováno něco jako NatMax, NatMin?
Nejmenší hodnota je nula, ale jinak to omezené není, těch hodnot je nekonečně (spočetně) mnoho, právě díky rekurzi toho druhého konstruktoru.

eee, tak je ten Nat diskrétní, nebo ne? :-)

Chápu to s tou rekurzí. Nechápu proč je podstatné, že Nat je diskrétní, když pak tvrdíš, že není  :o

Idris

  • *****
  • 2 286
    • Zobrazit profil
    • E-mail
Re:Je Rust jazyk budoucnosti?
« Odpověď #306 kdy: 05. 12. 2022, 19:32:31 »
Říkáš, že Nat je Součtový (diskrétní) typ, takže tam nemůže být nekonečně mnoho čísel. Takže je nějak definováno něco jako NatMax, NatMin?
Nejmenší hodnota je nula, ale jinak to omezené není, těch hodnot je nekonečně (spočetně) mnoho, právě díky rekurzi toho druhého konstruktoru.
eee, tak je ten Nat diskrétní, nebo ne? :-)

Chápu to s tou rekurzí. Nechápu proč je podstatné, že Nat je diskrétní, když pak tvrdíš, že není  :o
Jistěže je diskrétní (a také konečný), má jen dva konstruktory, nulu (Z) a následníka (S). Jenže ten druhý je rekurzivní, libovolné přirozené číslo n se vyjádří jako SnZ. Takže hodnot je nekonečně mnoho. Je to takto zřejmé?

Re:Je Rust jazyk budoucnosti?
« Odpověď #307 kdy: 05. 12. 2022, 19:35:32 »
Říkáš, že Nat je Součtový (diskrétní) typ, takže tam nemůže být nekonečně mnoho čísel. Takže je nějak definováno něco jako NatMax, NatMin?
Nejmenší hodnota je nula, ale jinak to omezené není, těch hodnot je nekonečně (spočetně) mnoho, právě díky rekurzi toho druhého konstruktoru.
eee, tak je ten Nat diskrétní, nebo ne? :-)

Chápu to s tou rekurzí. Nechápu proč je podstatné, že Nat je diskrétní, když pak tvrdíš, že není  :o
Jistěže je diskrétní (a také konečný), má jen dva konstruktory, nulu (Z) a následníka (S). Jenže ten druhý je rekurzivní, libovolné přirozené číslo n se vyjádří jako SnZ. Takže hodnot je nekonečně mnoho. Je to takto zřejmé?

Typoonanismus

BoneFlute

  • *****
  • 1 983
    • Zobrazit profil
Re:Je Rust jazyk budoucnosti?
« Odpověď #308 kdy: 05. 12. 2022, 19:40:26 »
Jistěže je diskrétní (a také konečný), má jen dva konstruktory, nulu (Z) a následníka (S). Jenže ten druhý je rekurzivní, libovolné přirozené číslo n se vyjádří jako SnZ. Takže hodnot je nekonečně mnoho. Je to takto zřejmé?

Ano je.

Takže na místo Haskellovského
Kód: [Vybrat]
data Nat = 0,1,..., NatMax
je tam definice

Kód: [Vybrat]
data Nat : where
    Z  : Nat 0
    Succ : Nat n -> Nat (n+1)
nebo něco takového.

Haskell má Number jako buildin rozsah čísla. Zatímco Idris to má definováno vzorečkem.

Asi se chytám.

Idris

  • *****
  • 2 286
    • Zobrazit profil
    • E-mail
Re:Je Rust jazyk budoucnosti?
« Odpověď #309 kdy: 05. 12. 2022, 19:45:49 »
Jistěže je diskrétní (a také konečný), má jen dva konstruktory, nulu (Z) a následníka (S). Jenže ten druhý je rekurzivní, libovolné přirozené číslo n se vyjádří jako SnZ. Takže hodnot je nekonečně mnoho. Je to takto zřejmé?
je tam definice
Kód: [Vybrat]
data Nat : where
    Z  : Nat 0
    Succ : Nat n -> Nat (n+1)
nebo něco takového.
Ano, akorát bez těch typových parametrů. Takto to mají všechny funkcionální jazyky, i třeba OCaml. Prostě Peanova definice :)

Re:Je Rust jazyk budoucnosti?
« Odpověď #310 kdy: 06. 12. 2022, 00:47:59 »
Jestli už máš Idris 2, tak můžeš zkusit tohle:
Kód: [Vybrat]
...
Zkusil jsem. Ten generovaný C kód je naivní interpreter, optimalizace veškeré žádné, každá hodnota by default alokována a reference counted ... nevidím nic o cyklech nebo weak referencích, cykly buď není možné vytvořit, nebo leakují... Reference couting není atomický... I třeba sečtení dvou čísel je alokace nové hodnoty, vždy... Ten typový parametr rozměru se tam prostě zpropaguje jak v C tak i v JS kódu, žádný type-erasure, neměl jsem na ten výrok o type-erasure v první řadě vůbec skočit.

Ááááchjo.

BoneFlute

  • *****
  • 1 983
    • Zobrazit profil
Re:Je Rust jazyk budoucnosti?
« Odpověď #311 kdy: 06. 12. 2022, 04:53:00 »
Ten typový parametr rozměru se tam prostě zpropaguje jak v C tak i v JS kódu, žádný type-erasure, neměl jsem na ten výrok o type-erasure v první řadě vůbec skočit.
Jak zněl ten výrok?
Co z této tvé zkušenosti vyplývá?

Idris

  • *****
  • 2 286
    • Zobrazit profil
    • E-mail
Re:Je Rust jazyk budoucnosti?
« Odpověď #312 kdy: 06. 12. 2022, 05:55:11 »
Co z této tvé zkušenosti vyplývá?
Že Králík neví, co je interpretr ::) Ale aspoň už zjistil, co jsou v Idrisu implicitní parametry.

Re:Je Rust jazyk budoucnosti?
« Odpověď #313 kdy: 06. 12. 2022, 09:19:42 »
Ten typový parametr rozměru se tam prostě zpropaguje jak v C tak i v JS kódu, žádný type-erasure, neměl jsem na ten výrok o type-erasure v první řadě vůbec skočit.
Jak zněl ten výrok?
->
kontrola toho typového parametru pro délku se provádí při překladu a pak se provede type erasure, v době běhu programu tam ten typový parametr vůbec není. Například Idris nebo Lean umí transpilaci do C, kde není runtime pro typy ani GC, veškerou kontrolu oddře překladač a když usoudí, že je kód typově správně, vyplivne výstup bez typových parametrů, ty právě slouží pouze ke statické kontrole.

JS kód vygenerovaný Idrisem:

Kód: [Vybrat]
function Main_getCol($0, $1, $2) {
 const $3 = Data_Nat_isLTE($0, 1000n);
 switch($3.h) {
  case 0: /* Yes */ return Main_getCol1($1, $2);
  default: return Main_getCol2($1, $2);
 }
}

$0 je velikost matice.

V Céčku je kód cca to samý, akorát mnohem výřečnější, protože úplně všechny hodnoty (i funkce) jsou boxovány do typu Value, které pak ten rozhodně-ne-interpretr, no, jaksi interpretuje :D

---

Že Králík neví, co je interpretr ::) Ale aspoň už zjistil, co jsou v Idrisu implicitní parametry.
::)

Především jsem zjistil, že si strašně vymýšlíš. Také jsem zjistil, že Idris je jen jakési experimentální skriptovadlo - měl jsem dříve představu, že to je kompilovaný jazyk jako Haskell.

Btw. v této přednášce Simon Peyton Jones mluví o možnostech linearity v Haskellu a také trochu o Rustu, borrowing/ownership označuje jako "Linearity on the Kinds". Asi by to chtělo mu dát vědět, že to má špatně, že uživatel Idris prohlásil, že borrowing/ownership nemá s typovým systémem vůbec nic společného...

Idris

  • *****
  • 2 286
    • Zobrazit profil
    • E-mail
Re:Je Rust jazyk budoucnosti?
« Odpověď #314 kdy: 06. 12. 2022, 09:42:52 »
Také jsem zjistil, že Idris [...] - měl jsem dříve představu, že to je kompilovaný jazyk jako Haskell.
Je kompilovaný, ty si to pleteš a asi myslíš, že generuje přímo nativní kód. To je ovšem tvůj problém, nikdo to tady netvrdil. Naopak ti bylo řečeno, že má různé backendy (C, JS, ...). Defaultně používá Scheme (Chez).

Btw. v této přednášce Simon Peyton Jones mluví o možnostech linearity v Haskellu a také trochu o Rustu, borrowing/ownership označuje jako "Linearity on the Kinds".
Ale to je velmi trefné, linearita je prostě určitá sémantika předávání argumentů (hezky to má například Mercury, viz seriál zde na Rootu, v Rustu to je v podstatě move sémantika). Move sémantika není záležitost typového systému, ale v kombinaci s ním (v Rustu jde zejména o reference, to asi víš, co je) zaručuje paměťovou bezpečnost. BoneFlute ti to možná vysvětlí, má s tebou evidentně větší trpělivost ;)

P.S. Máš malé nevýznamné plus za ten odkaz :)