Je Rust jazyk budoucnosti?

[Idris]

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] Rozbalit


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.

[Reklama]

[BoneFlute]

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] Rozbalit


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]

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] Rozbalit


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] Rozbalit


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

Jasné zatím? Otázky?

[BoneFlute]

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] Rozbalit


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] Rozbalit


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]

Kód [Vybrat] Rozbalit


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] Rozbalit


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).

[Reklama]

[BoneFlute]

Ří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í 

[Idris]

Ří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í 

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 SⁿZ. Takže hodnot je nekonečně mnoho. Je to takto zřejmé?

[Wavelet]

Ří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í 

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 SⁿZ. Takže hodnot je nekonečně mnoho. Je to takto zřejmé?

Typoonanismus

[BoneFlute]

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 SⁿZ. Takže hodnot je nekonečně mnoho. Je to takto zřejmé?

Ano je.

Takže na místo Haskellovského

Kód [Vybrat] Rozbalit

data Nat = 0,1,..., NatMax

je tam definice

Kód [Vybrat] Rozbalit

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]

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 SⁿZ. Takže hodnot je nekonečně mnoho. Je to takto zřejmé?

je tam definice

Kód [Vybrat] Rozbalit

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

[Králík]

Jestli už máš Idris 2, tak můžeš zkusit tohle:

Kód [Vybrat] Rozbalit


...


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]

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]

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.

[Králík]

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] Rozbalit

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

---

Ž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]

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