Fórum Root.cz
Hlavní témata => Vývoj => Téma založeno: Coati 26. 02. 2022, 11:27:14
-
Jak se v runtimu přistupuje k číselným generickým parametrům třeba u Vect<T,N>, když překladač provádí kompletní type erasure? Když jde o konstantu, dosadí ji překladač přímo, ale v některých jazycích N nemusí být známé při překladu, co tam je za trik?
-
Záleží na tom, o jakém jazyku píšete. Když se ptáte takhle obecně, dá se na to odpovědět akorát tak, že se k nim přistupuje úplně stejně, jako k jiným generickým parametrům.
-
úplně stejně, jako k jiným generickým parametrům
K těm to v případě type erasure za běhu nejde vůbec.
-
data Vect : Type -> Nat -> Type where
Nil : Vect _ 0
Cons : a -> Vect a n -> Vect a (n+1)
length : Vect a n -> Nat
length {n} _ = n
Instanci vektoru lze načíst například za běhu ze vstupu pomocí readVect.
Lze vyzkoušet zde: https://learn-idris.net/play
-
úplně stejně, jako k jiným generickým parametrům
K těm to v případě type erasure za běhu nejde vůbec.
No právě.
-
úplně stejně, jako k jiným generickým parametrům
K těm to v případě type erasure za běhu nejde vůbec.
No právě.
Ten kód výše ukazuje, jak se to řeší v případě type erasure. V backendu pro C nebo JS je krásně vidět, jak všechny typy zmizí.
-
data Vect : Type -> Nat -> Type where
Nil : Vect _ 0
Cons : a -> Vect a n -> Vect a (n+1)
length : Vect a n -> Nat
length {n} _ = n
Instanci vektoru lze načíst například za běhu ze vstupu pomocí readVect.
Lze vyzkoušet zde: https://learn-idris.net/play
Ve v2 ten kód nefunguje, potřebná úprava je:length : {n : Nat} -> Vect a n -> Nat
length _ = n
Tady je vidět ještě lépe, jak fungují tzv. implicitní argumenty.
-
Tady je podrobně popsáno, jak se řeší $SUBJ v jazycích s lineárním typovým systémem: https://arxiv.org/pdf/2104.00480.pdf