Python konverguje k ML (diskuse)

[JS1]

Nejsem si jisty, jestli jsem spravne pochopil ten rozdil (mezi radkovym a podtypovym polymorfismem), ale u Pythonu mi prijde ten radkovy polymorfismus prirozenejsi. Funkce se odjakziva v Pythonu chovaji genericky, to znamena, nezalezi jim na konkretnich deklarovanych typech parametru, ale na tom, jake operace nad nimi lze provadet.

[Radek Miček]

Je rozdíl mezi řádkovým, podtypovým strukturálním a podtypovým nominálním polymorfismem.

V podtypovém polymorfismu je klíčové pravidlo subsumce: Má-li 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.

[JS1]

Tomuhle nerozumim:

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.

[Ondrej Santiago Zajicek]

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.

[sarimak]

Nestacila by na to ale existujici abstraktni bazova trida?

Pokud tedy metoda/funkce potrebuje nutne vedet, jake typove-specificke chovani ma zvolit, pouzije test na isinstance(). Tam kde neni potreba explicitne resit typ, pouzije se stavajici duck typing. Jelikoz umele pridat abstraktniho predka muzu kolikrat chci, zajistim tim vyse popisovane lexikalni typy.

[Radek Miček]

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 + 1

Automaticky 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 -> int

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

[JS1]

Aha, dik za vysvetleni. Takze ja na to koukam trochu prakticky, a pripada mi, ze pokud tenhle priklad projde typovou kontrolou, je to v poradku. Z toho vyplyva, jestli jsem nasi diskusi spravne pochopil, ze s tebou nesouhlasim, a jsem zastance toho, aby v Pythonu byl strukturalni podtypovy polymorfismus spis nez ten radkovy. Jinak v podstate Ondrej Zajicek niz napsat lepe to, co jsem si tak nejak myslel, kdyz jsem na tebe poprve reagoval.

[Ondrej Santiago Zajicek]

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

[Radek Miček]

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.

[Ondrej 'SanTiago' Zajicek]

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.

[tacoberu]

Můžu dvě otázky?

1. Proč bych něco takového, jako je:

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?

[pavel]

Kolikaty to uz bude pokus, jak odstranit koncepcni omyl nebo omezeni Pythonu ? Cython, mypy, Nuitka, Numba - variace na stejne tema a zatim se nic z toho nechytilo nebo neopustilo experimentalni stav.

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.

[Bystroushaak]

Mě se to docela líbí. Ty anotace tam jsou už teď, jen se trochu mění jejich syntaxe, ale tak, aby to bylo zpětně kompatibilní.

[x]

Volitelný typový systém nepotřebuje inferenci. Volitelný typový systém ani nemusí být správný (viz kovariantní generiky v Dartu), to je celá pointa té volitelnosti. Musí být jenom užitečný, zbytek jsou akademické řečičky.

[Radek Miček]

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)

[x]

Dejte ten první program normálnímu programátorovi a pravděpodobně vám řekne: "to volání f(new ZvireKrmic(), new Pes()) je špatně, ne? Přece ZvireKrmic, což je Krmic<Zvire>, nemůže být Krmic<Pes>..."

No ano, my víme že může, protože to zvíře se tam vyskytuje jenom v kontravariantní pozici, jenže to odporuje běžné programátorské intuici. A to je přesně to, o čem si s volitelným typovým systémem můžete aspoň dovolit uvažovat.

[Ondrej 'SanTiago' Zajicek]

Ja bych rekl, ze normalni programator, aniz by cokoliv vedel o kovariantnich a kontravariantnich pozicich v generikach a teorii typovych systemu, by minimalne mel postrehnout to a zamyslet se nad tim, ze ten prvni priklad je semanticky korektni, zatimco bezny priklad dosazeni predka na misto, kde se ocekava potomek, je obecne semanticky nekorektni. A takova uvaha by mela zvitezit nad (spatnou) intuici.

[erzsebe]

a ML je co?

[Ondra]

ML (puvode zkratka za metalanguage) je programovaci jazyk, ktery na zacatku 70. let vytvoril Robin Milner. Na svoji dobu (ktera v podstate trva do ted) byl velmi pokrokovy a postupem casu se jim nechavaji inspirovat jakyzy, at uz nove, nebo nove verze tech stavajicich.

Odtud ta konvergence, i kdyz nekdy je kolem tohoto pokroku zbytecne vic kecu, remcani a vymluv, nez by bylo zdravo, a ta konvergence by mohla byt rychlejsi (alespon z meho pohledu).

Wikipedia: ML (programming language)

[xxar3s]

Este doplnim kolegu ze ML je aj rodina jazykov, ktore maju povod v ML.

Najrozsirenejsi ML jazyk je F# (podla tiobe).

Ps. Nechapem aky zmysel ma prerobit python na ML a nepouzit radsej priamo niektory ML jazyk.

[JS1]

Mozna trochu pozde, ale tady je zajimavy blogpost k tematu (a diskuse na HN).

TLDR: Semantika typu v Pythonu je dost nejasna a je otazka, jestli to neni vlastne vyhoda.

[Radek Miček]

V tom, že by se podivná chování měla opravit souhlasím s autorem blogu. Ale na rozdíl od něj si myslím, že tato podivná chování nepředstavují překážku pro zavedení statického typového systému. Například volání __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.

[UFAAUTO789]

ufa789 เว็บแทงบอลที่ใหญ่ และการเงินมั่นคงที่สุด สล็อตออนไลน์ ไม่มีขั้นต่ำ ใช้ทุนน้อย เล่นได้ทุกเกม

[ufabet]

Excellent beat ! I wish to apprentice while you amend your website, how could i subscribe for a blog site? The account helped me a acceptable deal. I had been a little bit acquainted of this your broadcast provided bright clear idea. ufabet

[BETFLIXSUPERVIP]

site! I truly love how it is easy on my eyes and the data are well written. I am wondering how I could be notified when a new post has been made. I’ve subscribed to your RSS feed which must do the trick! Have a great dayทางเข้า betflix