Převod List<a> na Vect<a,n>

[Coati]

Jak můžu napsat funkci převádějící List<a> na Vect<a,n> (kde n je, logicky, velikost vektoru). Překladač hlásí, že nezná n, to ale nemusí být známo v době překladu.

[Reklama]

[snugar_i]

Sice jsi nenapsal ani v jakým jazyce se snažíš to udělat (nebo jsem slepej), takže můžeme jenom hádat, ale tipnul bych, že to přesně z tohohle důvodu nejde - Vect<a, n> prostě potřebuje v době překladu vědět, kolik je n, protože Vect<a, 4> má jinou implementaci než Vect<a, 5>. Takže snad jedině přes velikej if podle velikosti Listu.

[alex6bbc]

nejdriv zjistit velikost listu a pak pokracovat na vektor.

[Idris]

nejde - Vect<a, n> prostě potřebuje v době překladu vědět, kolik je n, protože Vect<a, 4> má jinou implementaci než Vect<a, 5>. Takže snad jedině přes velikej if podle velikosti Listu.

Ten parametr n nemusí mít známou hodnotu, pokud jde v jazyce mít tento typ:

Kód: [Vybrat]

structure Sigma {α : Type u} (β : α → Type v) where
  fst : α
  snd : β fst
V haskelloidních jazycích to bývá nějak takto:

Kód: [Vybrat]

data DPair : (a : Type) -> (p : a -> Type) -> Type where
   MkDPair : {p : a -> Type} -> (x : a) -> p x -> DPair a p
Pak jde ta funkce napsat tak, aby fungovala za běhu (kdy se ten seznam, a tedy i n, načte například ze souboru nebo je po spuštění programu zadá uživatel).

[alex6bbc]

nebo zacit s nejakou velikosti na zacatku a kdyz by pridavani presahlo velikost, tak udelat novy vetsi vektor a stary vektor prekopirovat a pridat novou hodnotu. to je ale uz heuristika.

[Reklama]

[Wavelet]

Zdá se mi to nebo si tu Idris pokládá zdánlivě triviální otázky na které si odborně odpovídá pod jiným účtem 
viz minule https://forum.root.cz/index.php?topic=27054.0

[Ink]

Zdá se mi to nebo si tu Idris pokládá zdánlivě triviální otázky na které si odborně odpovídá pod jiným účtem 
viz minule https://forum.root.cz/index.php?topic=27054.0

To je zajímavá hypotéza...

[BoneFlute]

nejde - Vect<a, n> prostě potřebuje v době překladu vědět, kolik je n, protože Vect<a, 4> má jinou implementaci než Vect<a, 5>. Takže snad jedině přes velikej if podle velikosti Listu.

Ten parametr n nemusí mít známou hodnotu, pokud jde v jazyce mít tento typ:

Kód: [Vybrat]

structure Sigma {α : Type u} (β : α → Type v) where
  fst : α
  snd : β fst
V haskelloidních jazycích to bývá nějak takto:

Kód: [Vybrat]

data DPair : (a : Type) -> (p : a -> Type) -> Type where
   MkDPair : {p : a -> Type} -> (x : a) -> p x -> DPair a p
Pak jde ta funkce napsat tak, aby fungovala za běhu (kdy se ten seznam, a tedy i n, načte například ze souboru nebo je po spuštění programu zadá uživatel).

Jaký to má potom praktický efekt?

Mám funkci:

Kód: [Vybrat]

format x : String
...
format x : Int
...
formatAll xs : [String | Int]
...

loadFromFile File -> Error [String | Int], ErrorState
    ...
   
Načtu ze souboru, a obsah musím převést do konečně známého tvaru. Pokud tam budu posílat boolean, tak zmršit na int. Pokud tam mám Date, tak nevím.

Jak se bude chovat kód, ve kterém formatAll obsahuje kolekci, jejíž signaturu znám až po načtení souboru? Půjde to korektně přeložit? A když to načte bool, nebo Date, co se stane?

[BoneFlute]

Aby nedošlo k omylu, já to zadání chápu. Jen jsem ho zjednodušil.

Obecně v jazycích se předpokládají kolekce jako nekonečné. Tudíž proč někde uchovávat délku kolekce? Třeba proto, že mám funkce, které dokáží zpracovat jen konkrétní délku - což je můj příspěvek/dotaz. A nebo proto, že mám různé specializované funkce pro různé délky. Tak pak nevím proč to rvát do typu, když se můžu zeptat v nějakém switchi.

K čemu je zajímavé, že je ta délka součástí typu? Jaké to má praktické použití?

[Ink]

Aby nedošlo k omylu, já to zadání chápu. Jen jsem ho zjednodušil.

Obecně v jazycích se předpokládají kolekce jako nekonečné. Tudíž proč někde uchovávat délku kolekce? Třeba proto, že mám funkce, které dokáží zpracovat jen konkrétní délku - což je můj příspěvek/dotaz. A nebo proto, že mám různé specializované funkce pro různé délky. Tak pak nevím proč to rvát do typu, když se můžu zeptat v nějakém switchi.

K čemu je zajímavé, že je ta délka součástí typu? Jaké to má praktické použití?

To má smysl při optimalizacích. Třeba Rust má vector ("nekonečný") a array, kde je délka součástí typu. Dává to perfektní smysl, stejně jako skutečnost, že to je dáno při kompilaci natvrdo. Samozřejmě si dovedu představit i nějakou realtimovou "oblast", kde se dynamicky vytvoří alokace řádků pevné délky. Ale je to taková specialitka...

[dfxxfd]

Ja to chápem tak, že pamäť pre vektor sa alokuje ako počet dát krát veľkosť dát, takže musia byť dáta za sebou v pamäti.

Nekonečná kolekcia je niečo ako zreťazený zoznam a má porozhadzované prvky v pamäti a ešte prvý prvok musí mať smerník na samotné dáta a smerník na druhý prvok, druhý prvok má smerník na svoje dáta a smerník na ďalší prvok, atď. Posledný prvok má smerník na ďalší prvok nastavený na Null. Takže sa dajú ľahko pridať ďalšie dáta, stačí správne ponastavovať smerníky na ďalší prvok v predchádzajúcom a pridávanom prvku.

[alex6bbc]

kdyz mas delku kolekce primo v typu/objektu tak pri kazdem add/delete automaticky upravujes hodnotu delky. jinak si musis udelat (nekonecnou) smycku a delku spocitat.

[BoneFlute]

kdyz mas delku kolekce primo v typu/objektu tak pri kazdem add/delete automaticky upravujes hodnotu delky. jinak si musis udelat (nekonecnou) smycku a delku spocitat.

Takže cheš říct, že když mám:

Kód: [Vybrat]

parseList : String -> [Int]
tak ten kompilátor si nemůže vytvořit paměťovou buňku ve které bude jednak ta kolekce čísel ale i informace o počtu?

[alex6bbc]

kdyz mas delku kolekce primo v typu/objektu tak pri kazdem add/delete automaticky upravujes hodnotu delky. jinak si musis udelat (nekonecnou) smycku a delku spocitat.

Takže cheš říct, že když mám:

Kód: [Vybrat]

parseList : String -> [Int]
tak ten kompilátor si nemůže vytvořit paměťovou buňku ve které bude jednak ta kolekce čísel ale i informace o počtu?

proto se mi libi Go a dalsi jazyky, ktere delku vektoru schovavaji v typu a je to pro bezpecnost; proto se mi libi C a assembler kde to nikdo nehlida a inteligent musi hlidat sam.

[BoneFlute]

kdyz mas delku kolekce primo v typu/objektu tak pri kazdem add/delete automaticky upravujes hodnotu delky. jinak si musis udelat (nekonecnou) smycku a delku spocitat.

Takže cheš říct, že když mám:

Kód: [Vybrat]

parseList : String -> [Int]
tak ten kompilátor si nemůže vytvořit paměťovou buňku ve které bude jednak ta kolekce čísel ale i informace o počtu?

proto se mi libi Go a dalsi jazyky, ktere delku vektoru schovavaji v typu a je to pro bezpecnost; proto se mi libi C a assembler kde to nikdo nehlida a inteligent musi hlidat sam.

Asi nerozumím. Kde v tom mám hledat odpověď na mou námitku?

Já chci, aby mi kompilátor hlídal. Čím víc, tím lépe. Tady se ale bavíme o tom, proč dávat do typu něco co nepotřebuji a nejedná se o nic, co by měl kompilátor hlídat.