Portál AbcLinuxu, 26. dubna 2024 22:11
x typ S a je-li S podtyp T, pak x má typ T. To znamená, že kdykoliv je požadována hodnota typu T lze dát i hodnotu typu S. Klasické algoritmy typové inference jsou založeny na unifikaci – pokud je někde požadována hodnota typu T a dávám-li tam hodnotu typu T0, tak se oba typy unifikují (za proměnné v typech T a T0 se dosadí, aby typy byly shodné). Kvůli subsumci však tento postup nejde použít (např. T = Zvíře a S = Pes – v typech Zvíře a Pes nejsou žádné proměnné a nejde je unifikovat).
Jinak řečeno raději bych při typové inferenci řešil rovnosti než nerovnosti.
Předpokládejme:
class Zvíře { void jez(); }
class Pes { void jez(); void štěkej(); void vrč(); }
Chtěl bych napsat funkci, která jako argument bude moci mít hodnoty typu Zvíře i Pes, ale nechci tam mít pravidlo subsumce. Taková funkce bude mít typ
void f({ jez(); ... } zvíře);
Typ parametru zvíře říká, že hodnota musí mít metodu jez a může mít i nějaké další metody. Tři tečky jsou ve skutečnosti anonymní řádková proměnná, do níž se při unifikaci může dosadit (metody / jiná proměnná). Cíle jsme tedy dosáhli bez subsumce. Použití řádkových proměnných se říká řádkový polymorfismus.
Díký řádkovému polymorfismu máme něco jako podtypy do šířky, chybí ale podtypy do hloubky – metody musí mít shodné typy – nemohou to být podtypy.
Kvůli subsumci však tento postup nejde použít (např. T = Zvíře a S = Pes – v typech Zvíře a Pes nejsou žádné proměnné a nejde je unifikovat).Prijde mi, ze S je podtyp T musi z neceho vyplynout. V normalnim Pythonu to vyplyne z toho: Pes obsahuje metodu vrc(). Proc nemuze proste ten algoritmus typove inference pouzit tenhle fakt? Asi mi porad unika ten rozdil mezi radkovym a strukturalnim podtypovym polymorfismem. (Nominalni je - chapu-li to spravne - ze se explicitne deklaruje treba ze Pes je podtrida Zvirete). IMHO, podminkou typoveho systemu v Pythonu ma byt to, aby dnes validni programy v Pythonu (ve smyslu bezi to korektne na vsech vstupech) bylo mozne otypovat tak, aby neselhaly na typovou chybu po zavedeni typove kontroly. Pokud radkovy polymorfismus omezi, co se da dnes delat, je to proste spatny napad tam takovou vec davat. Priznam se, ze nejsem moc velky zastance statickeho typovani, jako cile. Staticke typy (zvlast pokud je chceme mit rozhodnutelne) jsou totiz vzdy jen aproximace toho, co se skutecne stane. Podle me dost programatoru ponekud popira praktickou realitu, v ktere je typovy dynamismus temer vzdy nevyhnutelny (ve smyslu - pokud to budeme chtit napsat typove korektne, bude to bud dost pres ruku, nebo se typove kontroly v danem pripade beztak vzdame). Ti, co to nepopiraji, prijali extremne dynamicky typovane jazyky jako Lisp, Forth nebo Python; prave proto, ze je nesvazuje (rozhodnutelny) typovy system.
Priznam se, ze nejsem moc velky zastance statickeho typovani, jako cile. Staticke typy (zvlast pokud je chceme mit rozhodnutelne) jsou totiz vzdy jen aproximace toho, co se skutecne stane. Podle me dost programatoru ponekud popira praktickou realitu, v ktere je typovy dynamismus temer vzdy nevyhnutelny.Ono take staticke typovani neni cil, je to prostredek. Dale IMHO neni rozumne se koukat na staticke a dynamicke typovani jako na alternativy, spis se jedna o koncepty, ktere se vzajemne doplnuji (i kdyz je pravda, ze existuji jazyky z obou konci spektra, at uz takove, ktere staticke typy nemaji, tak takove, ktere maji tak striktni staticky typovy system, ze vse, co by jinak resily dynamicke typy, je uz rozhodnuto staticky).
Ti, co to nepopiraji, prijali extremne dynamicky typovane jazyky jako Lisp, Forth nebo Python; prave proto, ze je nesvazuje (rozhodnutelny) typovy system.Predstav si, ze mas funkci v programu a chces na zaklade lokalni informace (vidis jen samotnou funkci) overit jeji korektnost. Pak potrebujes vedet, co se od te funkce ocekava, minimalne co volany muze predpokladat o argumentech a co naopak volajici muze ocekavat o navratove hodnote. To muzes bud jen napsat do komentaru, nebo to explicitne formulovat pomoci assertu na zacatku a konci funkce. Na (staticky) typovy system pak muzes pohlizet jako na mechanismus, ktery nektere ty asserty umozni vyhodnotit staticky (pokud je lze overit staticky, tak je automaticky vyradit z kodu, pokud ne, tak pripadne vynadat). Druhy uzitecny aspekt statickeho (nebo mozna bych to spis nazval 'lexikalniho') typoveho systemu je to, ze umoznuje explicitne popsat lexikalni kontext. Kdy na ten samy objekt (s jednim dynamickym typem) je mozne pohlizet ruznymi pohledy (ryznymi lexikalnimi typy). Napr. v Lispu dynamicky typovy system nerozlisi asociacni list, obecny list ci obecnou strukturu tvorenou pary. V C-like jazyku zas je mozne plynule prechazet mezi unsigned a signed pohledem na cislo, ci je mozne chapat ten samy string "12345" jako pole bajtu, genericky zero-terminated string, ci jako dekadicky kodovane 'dlouhe cislo'. S trochou nadsazky se na to da algebraicky podivat tak, ze objekty (se svymi dynamickymi typy) tvori nosnou mnozinu a ruzne staticke typy pak tvori ruzne algebraicke struktury na te nosne mnozine (ci na jejich podmnozinach). V Lispu nebo v C se to vetsinou resi tak, ze ty funkce pracujici z danou strukturou maji spolecny prefix (napr. assoc-* ci list-*, ci memcmp vs strcmp), jenze pak se clovek pri psani kodu v obou jazycich uprefixuje, pritom informace o aktualnim pohledu je obvykle znama z kontextu a je prirozene ji asociovat s lexikalni promennou, pres kterou se k objektu pristupuje.
Asi mi porad unika ten rozdil mezi radkovym a strukturalnim podtypovym polymorfismem.Příklad z OCamlu:
class foo = object method f = 1 method g = 1 end class bar = object method f = 10 method g = "" end let h xs = (List.hd xs)#f + 1Automaticky odvozené typy:
class foo : object method f : int method g : int end class bar : object method f : int method g : string end val h : < f : int; .. > list -> intFunkce
h bere seznam objektů, jenž mají metodu f a nějaké další metody. Dvě tečky jsou řádková proměnná. Zkusím-li funkci h použít se seznamem [new foo; new bar], dostanu chybu:
Error: This expression has type bar but an expression was expected of type
foo
Types for method g are incompatible
Problém je, že kompilátor do řádkové proměnné dosadil metodu g z foo a požaduje seznam objektů typu < f : int; g: int >. S řádkovým polymorfismem tohle nejde otypovat – do řákové proměnné nejde dosadit, aby výsledný typ byl foo a zároveň bar. Pro tyto případy má OCaml explicitní přetypování, lze tedy napsat [(new foo :> < f : int >); (new bar :> < f : int >)].
Totéž v systému se strukturálním podtypovým polymorfismem: Funkce h by nejspíše měla typ < f : int > list -> int. Pokud seznamy obsahují hodnoty jednoho typu, použitím subsumce dostane kompilátor new bar : < f : int > a new foo : < f : int >. Příklad tedy projde typovou kontrolou.
pokud je někde požadována hodnota typu T a dávám-li tam hodnotu typu T0, tak se oba typy unifikují (za proměnné v typech T a T0 se dosadí, aby typy byly shodné). Kvůli subsumci však tento postup nejde použít (např. T = Zvíře a S = Pes – v typech Zvíře a Pes nejsou žádné proměnné a nejde je unifikovat).Nevim, co o tom rika teorie, ale me dava daleko vetsi smysl to chapat jako logickou resoluci nez jen jako unifikaci. Takze v takovem pripade potrebuji automaticky odvodit Zvire(v) z faktu Pes(v) a pravidla Pes(X)->Zvire(X).
Typ parametru zvíře říká, že hodnota musí mít metodu jez a může mít i nějaké další metody.To me prijde, ze jsem jen nahradil obecny fakt (v splnuje typ 'vrcable') za konkretni fakt (v ma metodu vrc). Toho sameho bych mohl obdobne dosahnout na urovni typu (objekty/tridy by explicitne znaly vsechny typy, ktere splnuji, a funkce by mohla definovat konjunkci pozadovanych typu pro argument).
To me prijde, ze jsem jen nahradil obecny fakt (v splnuje typ 'vrcable') za konkretni fakt (v ma metodu vrc). Toho sameho bych mohl obdobne dosahnout na urovni typu (objekty/tridy by explicitne znaly vsechny typy, ktere splnuji, a funkce by mohla definovat konjunkci pozadovanych typu pro argument).V typových systémech s průnikovými typy se tohle někdy dělá. Takové systémy pak nepotřebují obecné záznamy/objekty, stačí typ pro záznam/objekt s jedním polem/metodou – záznamy/objekty s více poli/metodami se získají jako průnik.
Nevim, co o tom rika teorie, ale me dava daleko vetsi smysl to chapat jako logickou resoluci nez jen jako unifikaci. Takze v takovem pripade potrebuji automaticky odvodit Zvire(v) z faktu Pes(v) a pravidla Pes(X)->Zvire(X).Měla by to být především rozhodovací procedura. Pro jednoduché typové systémy s podtypovým polymorfismem takové existují. Jak se ale dostanete na úroveň Javy, tak se situace komplikuje – viz Mazurak, Zdancewic: Type Inference for Java 5 Wildcards, F-Bounds, and Undecidability.
Měla by to být především rozhodovací procedura.Je otazka, jestli tenhle pozadavek je opravdu vyznamny. Negativni odpoved (tedy ze kompilator se pri validaci typoveho vyrazu obecne muze zacyklit a sezrat zdroje) je sice neprijmemna, ale prakticky se to zas tak nelisi od situace, kdy mame jazyk s turingovsky uplnym makrojazykem (coz ma treba Lisp), kde se vyrazy v nem take mohou zacyklit pri kompilaci. IMHO pozadavek na rozhodnutelnost je zbytecne omezujici, expresivnost typoveho systemu je IMHO dulezitejsi nez rozhodnutelnost. Spis nez obecna teoreticka rozhodnutelnost je treba, aby typovy system mel 'smysluplnou operacni semantiku', tedy aby programator rozumel tomu, jak se konkretni typovy vyraz bude 'vyhodnocovat' a mohl zvolit takove typove vyrazy, ktere se efektivne vyhodnoti a vyhnout se tem, ktere by se zacyklily.
void f({ jez(); ... } zvíře);
měl chtít? Pak by mi do té funkce mohlo projít i něco takového:
class VodníDílo { void jez(); }
2. Mě by se více líbilo řešení zadaného problému takto:
void f(Zvire | Pes zvíře)V čem je to horší/lepší? Nebo jen blbý příklad?
Moc tomu neverim, kdyz se zatim ani poradne nepreslo na Python 3. Nevidim ani duvod pro vznik dalsiho python-like jazyka, kdyz oblasti kriticke na rychlost zpracovani jsou uz obsazeny jinymy nastroji a jazyky.
14.8.2014 23:02
Bystroushaak | skóre: 36
| blog: Bystroushaakův blog
| Praha
Volitelný typový systém ani nemusí být správný (viz kovariantní generiky v Dartu)Kovariantní generika v Dartu, aneb když programy, co jsou v podstatě v pořádku nefungují (v checked módu). Volání
start
abstract class Zvire { void jez(); }
class Pes extends Zvire { void jez() { print("Pes"); } }
abstract class Krmic<A> { void nakrm(A a); }
class ZvireKrmic extends Krmic<Zvire> {
void nakrm(Zvire z) { z.jez(); }
}
void f(Krmic<Pes> k, Pes p) {
k.nakrm(p);
}
void start() {
f(new ZvireKrmic(), new Pes());
}
vyhodí výjimku
Breaking on exception: type 'ZvireKrmic' is not a subtype of type 'Krmic<Pes>' of 'k'.Zatímco obdobný program ve Scale normálně funguje (
Krmic je kontravariantní v A).
abstract class Zvire { def jez: Unit }
class Pes extends Zvire { def jez = println("Pes") }
abstract class Krmic[-A] { def nakrm(a: A): Unit }
class ZvireKrmic extends Krmic[Zvire] {
def nakrm(z: Zvire) = z.jez
}
def f(k: Krmic[Pes], p: Pes) = k.nakrm(p)
def start = f(new ZvireKrmic, new Pes)
__repr__ nebo cmp může statický typový systém povolit pro každé objekty a chování při spuštění programu může zůstat stejné.
Jeden z diskutujících, ivoras, psal:
By adding static types, the focus of the language would move to a different niche, which would probably be already occupied by some competitor language(s) which do(es) types much better.Myslím, že je stále dost volného prostoru – například kombinování více typových systémů v jednom programu/jazyce.
Tiskni
Sdílej:
ISSN 1214-1267, (c) 1999-2007 Stickfish s.r.o.