Příspěvky

196

Vývoj / Re:Je Rust jazyk budoucnosti?

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

197

Vývoj / Re:Je Rust jazyk budoucnosti?

« 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?

198

Vývoj / Re:Je Rust jazyk budoucnosti?

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

199

Vývoj / Re:Je Rust jazyk budoucnosti?

« kdy: 05. 12. 2022, 18:17:03 »

Já vím přesně co je vtable, ať už v originále, nebo v tvém použití.

Co mě mate je type-erased metoda. Měl jsem za to, že type erased je chování, kdy za určitých okolností ztrácíme informaci o typu (respektive je nám zabráněno se k ní dostat). Wiki tvrdí toto: In programming languages, type erasure is the load-time process by which explicit type annotations are removed from a program, before it is executed at run-time.

Dobře, tak nějaký konkrétní příklad, třeba Javu, ať je to jednoduchý - dejme tomu, že definuješ generickou funkci static <T> void writeAsString(T object) {} která vezme object, zavolá toString() a výsledek někam zapíše. Při kompilaci z toho java ty typy odstraní a vytvoří něco jako (ne doslova) void writeAsString(Object object) ... kód tý metody tedy při volání neví, jakej typ má argument, takže metodu toString() musí volat přes vtable, nemůže ji volat přímo.

A jak by toto vypadalo v Idrisu?

200

Vývoj / Re:Je Rust jazyk budoucnosti?

« kdy: 05. 12. 2022, 18:14:16 »

To je ale specielní případ, kdy jsi funkci `col` inlinoval do volající funkce.

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

Kód: [Vybrat]

import Data.Fin
import Data.Nat
import Data.Vect

data Matrix : Nat -> Nat -> Type -> Type where
  MkMatrix : (n : Nat) -> (m : Nat) -> Ptr a -> Matrix n m a

total getCol1 : Matrix n m a -> Fin m -> Vect n a
getCol1 mat col = ?r1

total getCol2 : Matrix n m a -> Fin m -> Vect n a
getCol2 mat col = ?r2

total getCol : {m : Nat} -> Matrix n m a -> Fin m -> Vect n a
getCol mat col = case isLTE m 1000 of
                   Yes _ => getCol1 mat col
                   _ => getCol2 mat col

201

Vývoj / Re:Je Rust jazyk budoucnosti?

« kdy: 05. 12. 2022, 17:54:28 »

Na co by mi v run-time byly typy, když je nepoužívám - proč mít vtable, když jsem typy odrbal = type erasure.

Type-erased metoda neví, jaký typ ji přichází jako argument - proto se tomu říká type erasure. Tím pádem neví, jak konkrétně danou operaci nad tim argumentem provést. Buďto si může ten typ přečíst z nějakého tagu a udělat tu vidličku, anebo si přečte z vtable adresu konkrétní imeplementace a tu zavolá.

Přijde mi, že tě koncept vtable mate - vtable není typ.

BoneFlute má pravdu, a pokud nebudeme používat typové třídy (což pro uvedené příklady nepotřebujeme), tak nikde žádná (analogie) vtable nebude.

202

Vývoj / Re:Je Rust jazyk budoucnosti?

« kdy: 05. 12. 2022, 17:50:11 »

Načtu matici ze souboru.
Zjistím velikost matice, podle toho vyberu buď reprezentaci (nikoliv typ) A, nebo reprezentaci B.
Pokud je to A pošlu to "uličkou" A. Pokud je to B pošlu to uličkou B.

Konkretizuj to prosím. Představ si, že seš metoda `col`. Na základě čeho uděláš to rozhodnutí, kterou uličkou poslat maticová data?

Nejseš žádná metoda. Nic takové není.

Ve funkci načítání matice ze souboru je podmínka, která zjistí velikost dat. Pokud je to větší jak požadovaná podmínka (IF, SWITCH), tak provede větev, kde funkci col_optimalized předá získané data (surový pole bytů), pokud je menší, předá data funkci col_unoptimalized. Nikde žádné typy, nikde žádné tagy, nikde žádné vtable.

Já bych to asi rozhodoval až v col pomocí isLTE, podle mě to povede ke kratšímu kódu.

203

Vývoj / Re:Je Rust jazyk budoucnosti?

« kdy: 05. 12. 2022, 17:47:00 »

Tagují se součtové typy, to s typovými parametry vůbec nesouvisí.

Ano, přesně tak, v případě nepoužití vtable je ten typ efektivně konvertován na součtový, tj. v tom příkladu s maticí s prahem velikosti pro jinou reprezentaci to efektivně bude součtový typ obsahující dvě varianty - malá a velká matice.

Ne, nebude (pokud se pořád bavíme o Idrisu/Leanu).

204

Vývoj / Re:Je Rust jazyk budoucnosti?

« kdy: 05. 12. 2022, 17:44:45 »

Načtu matici ze souboru.
Zjistím velikost matice, podle toho vyberu buď reprezentaci (nikoliv typ) A, nebo reprezentaci B.
Pokud je to A pošlu to "uličkou" A. Pokud je to B pošlu to uličkou B.

Konkretizuj to prosím. Představ si, že seš metoda `col`. Na základě čeho uděláš to rozhodnutí, kterou uličkou poslat maticová data?

Nechcete si to psát přímo v kódu? Třeba tady: https://learn-idris.net/play

205

Vývoj / Re:Je Rust jazyk budoucnosti?

« kdy: 05. 12. 2022, 17:43:18 »

Není podstatné, že Lua je dynamický jazyk. Chtěl jsem tím uvést, že když jsem se kouknul do toho zdrojáku, tak tam žádné typové informace, které tvrdíš, že tam musí zůstat aby něco, nebyly.

Jak jsi poznal, že tam nebyly typové informace? V jazyce jako Lua má každá hodnota runtime typovou informaci, tak fungují dynamicky typované jazyky, tzn. ty typy tam nemohly nebýt

Na vstupu bylo x = Red. V lue bylo x = 1. To považuji, že tam ten Red není.

Aby tohle fungovalo, musí být ta hodnota boxovaná (na-alokovaná na heapu a schovaná za, efektivně, pointer) a operace na ní se provádí přes dynamic dispatch (bude tam nějaký ekvivalent v-table), jinak by nebylo možné provést type erasure.

Teda, já jsem to vždycky chápal tak, že type erasure je způsob, jak typy odrbat. Kde by tam jako měla být schovaná vtable? A proč? Ve skutečnosti tam tu vtable potřebuješ v případě, kdy nechceš dělat type erasure...

Dobře, tak mějme ten příklad s maticí. Dejme tomu, že od nějaké velikosti Thr (jako threshold) používá implementace matice nějakou vymakanou reprezentaci v paměti kvůli ušetření místa pro velké matice. Ok? Teď dejme tomu, že máme operaci `col` na matici, která vrátí daný sloupec jako vektor. Tahle operace bude muset fungovat různě v závislosti na Thr, z úsporné reprezentace se čte sloupec jinak než z jednoduché.

Tak, a teď, ty napíšeš program, který načte matici ze souboru a bude chtít číst sloupce. Pokud by ta typová informace - v tomto případě velikost matice - byla komplet odstraněna, metoda `col` by neměla jak poznat, jak je konkrétní matice v paměti reprezentována, a tedy jak extrahovat sloupec. Proto bude muset ta matice si s sebou tu informaci vzít a držet si ji během runtime, buďto to může být nějaký tag, podle kterého udělá ta metoda `col` vidličku, anebo si s sebout vezme vtable, která bude u různých konkrétních hodnoty ukazovat na různé implementace `col`. Řešení s vtable je obecnější - těch typových parametrů může být více, chování se může v závislosti na nich více lišit.

V jazyce jako Rust nebo C++ tohle není potřeba, protože kompilátor zná dopředu všechny instanciace a provede monomofrizaci, ie. v podstatě z toho udělá různé typy s různými metodami, ale cena za to je, že není možné vytvořit tu hodnotu at runtime.

Načtu matici ze souboru.
Zjistím velikost matice, podle toho vyberu buď reprezentaci (nikoliv typ) A, nebo reprezentaci B.
Pokud je to A pošlu to "uličkou" A. Pokud je to B pošlu to uličkou B.

V tomto případě tam nikde není třeba uchovávat informaci o typu, ani v tagu, ani nikde.

Ale budiž, blbej případ.

Problém není v tom, že by informace nemohla být v runtimu, že by tam nemohl být nějaký tag, nebo co já vím. Ty tvrdíž, že tam být musí, zatímco v Rustu být nemusí. Ale vůbec mi nedochází, kde to musení vidíš.

Představ si lepší překlad:

Kód: [Vybrat]

type Matice a = GenericMatice a | OptimalizedMatice a
let xs : [Matice] = parseFromFile(f)

out = map format xs
where
   format x = case (type x):
      GenericMatice m -> formatGenericMatice m
      OptimalizedMatice m -> formatOptimalizedMatice m

Toto je první příklad, kde by mě napadlo, že by se hodilo type erasured nemít. A určitě se shodnem, že to některé jazyky takto můžou, přidat tam ty tagy, použít. Jiné jazyky něco takové zakážou. A některé jazyky (nebo ty samé, ale prostě si usmysleli) to zoptimalizují tak, že tam budou dvě "uličky" (v tomto případě si to nedokážu úplně představit, ale to není argument - stejně tak nedokážu najít "důkaz", proč by to nemělo jít). Pak tam v rámci optimalizace nebude vůbec žádná informace o typu.

Informace o typu tam nebude nikdy. Idris a spol. mají kvantitativní typový systém a tzv. implicitní argumenty. To jsme ale hodně odbočili. Jinak pro ten příklad s maticí by se asi použil typ LTE, není nutné psát součtový typ, to je boilerplate. Ale jak říkám, to jsme odbočili k úplně jinému tématu.

206

Vývoj / Re:Je Rust jazyk budoucnosti?

« kdy: 05. 12. 2022, 17:35:15 »

Jazyky jako Idris a Lean (a pár dalších) dělají type erasure a vtables v generovaném kódu taky nepoužívají.

No ano, protože ty hodnoty tagují, jak jsem viděl (v kódu všude velké switche na tagy).

Idris2 se mi instaluje, jak si z něj vygeneruju C kód pomocí 'refc' backendu?

Tagují se součtové typy, to s typovými parametry vůbec nesouvisí.

Dal bych --codegen refc.

207

Vývoj / Re:Je Rust jazyk budoucnosti?

« kdy: 05. 12. 2022, 17:31:22 »

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.

208

Vývoj / Re:Je Rust jazyk budoucnosti?

« kdy: 05. 12. 2022, 17:26:08 »

Na co by mi proboha prosím byl vtable, pokud nedělám type erasure? Přesně z toho důvodu, že jazyky jako C++ nebo Rust nedělají type erasure generik (místo toho monomofrigzují) nepotřebují vtables, narozdíl třeba od Javy.

Jazyky jako Idris a Lean (a pár dalších) dělají type erasure a vtables v generovaném kódu taky nepoužívají.

209

Vývoj / Re:Je Rust jazyk budoucnosti?

« kdy: 05. 12. 2022, 17:20:47 »

Jinak podíval jsem se na C výstup Idris kompilátoru a je to prostě VM (verze idris je u mě 1.3.4). Toto je funkce alokující hodnotu, okopírováno z Idris runtime:

Kód: [Vybrat]

static inline Con * allocConF(VM * vm, uint32_t tag, uint16_t arity, int outer) { ... }

Hádejte, co je `tag`

Není to to, co si myslíš. A Idris 1 dávno není podporován, smysl dává jen použití jen Idrisu 2 (relevantní backend je "refc").

210

Vývoj / Re:Je Rust jazyk budoucnosti?

« kdy: 05. 12. 2022, 17:10:47 »

Aby tohle fungovalo, musí být ta hodnota boxovaná (na-alokovaná na heapu a schovaná za, efektivně, pointer) a operace na ní se provádí přes dynamic dispatch (bude tam nějaký ekvivalent v-table), jinak by nebylo možné provést type erasure.

Teda, já jsem to vždycky chápal tak, že type erasure je způsob, jak typy odrbat. Kde by tam jako měla být schovaná vtable? A proč? Ve skutečnosti tam tu vtable potřebuješ v případě, kdy nechceš dělat type erasure...

Já té formulaci asi nerozumím.

Tak tak. Ta formulace je blábol, nedává to vůbec smysl.