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

Coati

Převod List<a> na Vect<a,n>
« kdy: 17. 02. 2023, 00:27:31 »
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.
« Poslední změna: 17. 02. 2023, 08:14:48 od Petr Krčmář »


Re:Vect<a,n>
« Odpověď #1 kdy: 17. 02. 2023, 05:28:50 »
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

  • *****
  • 1 432
    • Zobrazit profil
    • E-mail
Re:Vect<a,n>
« Odpověď #2 kdy: 17. 02. 2023, 07:25:49 »
nejdriv zjistit velikost listu a pak pokracovat na vektor.

Idris

  • *****
  • 2 286
    • Zobrazit profil
    • E-mail
Re:Vect<a,n>
« Odpověď #3 kdy: 17. 02. 2023, 11:43:34 »
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

  • *****
  • 1 432
    • Zobrazit profil
    • E-mail
Re:Převod List<a> na Vect<a,n>
« Odpověď #4 kdy: 17. 02. 2023, 11:59:35 »
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.


Re:Převod List<a> na Vect<a,n>
« Odpověď #5 kdy: 17. 02. 2023, 12:09:16 »
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  ;D
viz minule https://forum.root.cz/index.php?topic=27054.0

Ink

  • *****
  • 655
    • Zobrazit profil
    • E-mail
Re:Převod List<a> na Vect<a,n>
« Odpověď #6 kdy: 17. 02. 2023, 12:34:20 »
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  ;D
viz minule https://forum.root.cz/index.php?topic=27054.0

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

BoneFlute

  • *****
  • 1 981
    • Zobrazit profil
Re:Vect<a,n>
« Odpověď #7 kdy: 17. 02. 2023, 16:35:59 »
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

  • *****
  • 1 981
    • Zobrazit profil
Re:Převod List<a> na Vect<a,n>
« Odpověď #8 kdy: 17. 02. 2023, 16:48:59 »
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

  • *****
  • 655
    • Zobrazit profil
    • E-mail
Re:Převod List<a> na Vect<a,n>
« Odpověď #9 kdy: 17. 02. 2023, 18:04:14 »
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...

Re:Převod List<a> na Vect<a,n>
« Odpověď #10 kdy: 17. 02. 2023, 18:05:07 »
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

  • *****
  • 1 432
    • Zobrazit profil
    • E-mail
Re:Převod List<a> na Vect<a,n>
« Odpověď #11 kdy: 17. 02. 2023, 18:10:20 »
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

  • *****
  • 1 981
    • Zobrazit profil
Re:Převod List<a> na Vect<a,n>
« Odpověď #12 kdy: 17. 02. 2023, 18:46:33 »
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

  • *****
  • 1 432
    • Zobrazit profil
    • E-mail
Re:Převod List<a> na Vect<a,n>
« Odpověď #13 kdy: 17. 02. 2023, 18:53:56 »
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

  • *****
  • 1 981
    • Zobrazit profil
Re:Převod List<a> na Vect<a,n>
« Odpověď #14 kdy: 17. 02. 2023, 19:03:46 »
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.