Příspěvky

1456

Vývoj / Re:Python - volání funkce z proměnné

« kdy: 10. 05. 2018, 19:09:16 »

- máš-li název funkce, hledáš v patřičném slovníku
- znáš-li funkci, a jen ji chceš předávat, tak ji normálně použiješ, ale bez závorek
- funkci, kterou máš uloženou v proměnné zavoláš tak, že jí dáš závorky.


def a():
   return "A"

def b():
   return "B"

class Klass:
   def m(self):
      return "C"

inst = Klass()

xs = [a, b, inst.m]

for m in xs:
   print m()
print globals()["a"]()
print globals()["b"]()
print getattr(inst, "a")()

1457

Server / Re:Prioritní dotazy do databáze

« kdy: 02. 05. 2018, 19:47:52 »

Řešili jsme to replikací.

Byla master databáze. Zápis do ní byl prioritní.
Následně byly slave databáze, do kterých se nezapisovalo, ale četlo, s tím, že data mohou mět určité spoždění oproti autoritativnímu masteru.

1458

Vývoj / Re:Formální verifikace podle typu na rozsah

« kdy: 02. 05. 2018, 16:34:43 »

Tak to je fikaný, teď je uvedeno:

Kód: [Vybrat]

if (Str.len s) < 4 then

zatímco původně bylo:

Kód: [Vybrat]

if (Str.len s) < 2 then

Jak to tedy má být?

To je fuk, ne? Otázka zněla, jak má typový systém ověřit správnost. V původním by nahlásil chybu, v tom druhém, že je to v pořádku. Podstatné je, zda je schopen.

1459

Vývoj / Re:Formální verifikace podle typu na rozsah

« kdy: 02. 05. 2018, 10:37:44 »

Napsalo by se to takhle:

Kód: [Vybrat]

fn s : String 0 40 -> String 4 20 =
    case s `hasMinimumLen` 4 of
        Just sn -> Str.sub sn 20 -- sn ma tady typ (String 4 40)
        Nothing -> "default"

Ono dnešní jazyky (Java..) by to uměly odvodit i z té podmínky - třeba "null" to schopné odvodit je, ale takhle je to hezčí a explicitně.

Fikaný!

1460

Vývoj / Re:Formální verifikace podle typu na rozsah

« kdy: 02. 05. 2018, 00:39:00 »

Jo, teď jsem se už definitivně ztratil já Co je myšleno tím "změnit návratový typ"?

:-D

Představme si, že jsem typový systém, a mám ověřit, zda tato funkce je v pořádku:

Kód: [Vybrat]

fn s : String 0 40 -> String 4 20 =
    if (Str.len s) < 4 then
        "default"
    else
        Str.sub s 20

Kouknu, a vidím, že na vstupu může přijít řetězec, minimálně 0, maximálně 40. Na výstupu je minimálně 4, max 20.
Takže 13 znaků cajk. 20 znaků cajk. 30 znaků cajk (hrubou silou oříznu). Ale 2 znaky už jsou problém, na vstupu přijít mohou, a na výstupu nesmí.

Funkce Str.sub s 20 v daném kontextu znamená Str.sub (String 0 40) 20 -> String 0 20 protože podle druhého argumentu si mohu odvodit, že tedy nedostanu delší string jak 20znaků, ale jako první argument stále mohu dostat prázdný string. A tedy nevím, jak bych měl uvažovat (jako ten typový systém).

Tedy samozřejmě si takhle jen hraju. Nikdy jsem typový systém neimplementoval, a tak se zkouším vcítit do jeho uvažování :-) A pravděpodobně někde mám i nějaké ty díry v úvaze.

1461

Vývoj / Re:Formální verifikace podle typu na rozsah

« kdy: 01. 05. 2018, 22:57:33 »

To Str.sub bude mít svůj návratový typ, a pokud ten není podtypem návratového typu té vnější funkce, překladač zařve.

Tak v tom případě to není odpověď na mou otázku :-)

Str.sub vrací String 0 ∞, zatímco fn vrací String 4 20. Takže mi to může vrátit dvouznakový řetězec, a to už je špatně.

A přesto očekávám, že (v případě, když bych tam neměl tu záměrnou chybu) mi to překladač označí za korektní.

No ale přece String 0 ∞ není podtypem String 4 20, tady je ta kontrola ještě přímočará. Možná teda nejspíš nechápu otázku. BTW to Str.sub by mělo mít návratový typ také závislostní podle vstupních parametrů, jinak by byla typová kontrola příliš restriktivní.

Počkej, počkej, mám pocit, že jsme se tu někdo z nás ztratil.

Str.sub má návratový typ String 0 ∞. Takže může vrátit dvouznakový řetězec. Vstupní argumenty jsou 20, což je ok na výstup, takže tento argument změní návratový typ na String 0 20. A dále String, jehož minimální velikost je určena tou kontrolou v if. Což je tedy defakto taky správně, a ta funkce bude pracovat korektně. A já se tedy táži, jak typový systém pozná, že díky podmínce if se z hodnoty String 0 20 stane hodnota typu String 2 20 (respektive String 4 20).

Zdůrazňuji, že já se táži na typový systém, který řeší mou úlohu. Netáži se jak fungují závislostní typy (i když zrovna třeba ony mohou řešit mou úlohu, a pak mě zajímá jak to řeší).

1462

Vývoj / Re:Formální verifikace podle typu na rozsah

« kdy: 01. 05. 2018, 21:05:31 »

To Str.sub bude mít svůj návratový typ, a pokud ten není podtypem návratového typu té vnější funkce, překladač zařve.

Tak v tom případě to není odpověď na mou otázku :-)

Str.sub vrací String 0 ∞, zatímco fn vrací String 4 20. Takže mi to může vrátit dvouznakový řetězec, a to už je špatně.

A přesto očekávám, že (v případě, když bych tam neměl tu záměrnou chybu) mi to překladač označí za korektní.

1463

Vývoj / Re:Curryfikované funkce v Haskellu

« kdy: 01. 05. 2018, 14:39:53 »

Takže ve výsledku funkce s libovolným počtem parametrů, která vrací Monoid, je Monoid.

To se mi nezdá. Funkce s libovolným počtem parametrů bude Monoid jen po ruční curryfikaci. Automaticky ne.

funkce s libovolným počtem argumentů je funkce s jedním argumentem kde výsledek je funkce s libovolným počtem argumentů minus jedna
a0 -> a1 -> ... an -> t
je jako
a0 -> t' kde t' = (a1 -> ... -> an -> t)
nebo taky
a0 -> (a1 -> ... an -> t)

Ha! Rozumím.

1464

Vývoj / Re:Curryfikované funkce v Haskellu

« kdy: 01. 05. 2018, 13:21:25 »

Takže ve výsledku funkce s libovolným počtem parametrů, která vrací Monoid, je Monoid.

To se mi nezdá. Funkce s libovolným počtem parametrů bude Monoid jen po ruční curryfikaci. Automaticky ne.

1465

Vývoj / Re:curryfikované funkce

« kdy: 01. 05. 2018, 12:30:18 »

má součinové, součtové a exponenciální typy

Uff! A jdu si studovat :-)

1466

Vývoj / Re:Formální verifikace podle typu na rozsah

« kdy: 01. 05. 2018, 12:29:12 »

A mě by zajímalo, jak má nebohý typový systém odvodit, že ta funkce je špatně?

Např. když si délkově omezený řetězec zadefinuji jako

Kód: [Vybrat]

data BString : Nat -> Nat -> Type where
  MkBString : (a : Nat) -> (b : Nat) -> (s : String) -> (LTE a (length s)) -> (LTE (length s) b) -> BString a b

tak abych do něj zabalil "default", musím psát něco jako

Kód: [Vybrat]

d : BString 4 20
d = MkBString 4 20 "default" (LTESucc (LTESucc (LTESucc (LTESucc LTEZero)))) (LTESucc (LTESucc (LTESucc (LTESucc (LTESucc (LTESucc (LTESucc LTEZero)))))))

kde poslední dva termy typů (LTE 4 7) a (LTE 7 20) jsou důkazy, že 4 <= 7 a 7 <= 20. V tomto případě by stačilo místo nich dát podtržítko a kompilátor je vymyslí sám. Nicméně i ve vaší funkci by bylo třeba dát důkazy, že nerovnosti platí - bez toho by se program nepřeložil.

Trochu jsem se v tom ztratil. Je to odpověď, na to, jak zjistí, že výstup není správně (to není tak zajímavé), nebo to, jak zjistí, že ta větev else, přestože může vrátit výsledek neodpovídající požadovanému výstupu, tak vždy vrátí (vrátila by) správný výsledek, protože proběhne jen v těch případech (to mě zajímá).

Díky.

1467

Vývoj / Re:Formální verifikace podle typu na rozsah

« kdy: 01. 05. 2018, 12:25:14 »

To jsou závislostní typy, verifikace se dělá přes theorem proving (takže překlad programu někdy trvá hodiny). Viz například jazyk Idris.

Mohl by si prosím lidsky popsat princip, jak se ta verifikace dělá?

Jako normální typová analýza, akorát typové operátory (konstruktory) berou i hodnoty krom typů. Třeba append na řetězcích by měl typ "String n m -> String k l -> String (n+k) (m+l)", takže v rámci typové kontroly (tj. během překladu, ne až za běhu) se počítá, v tomto případě s přirozenými čísly. Musí se dávat pozor na subsumpci a varianci, třeba String n m je podtypem String k l, pokud n>=k & m<=l.

Díky.
Uniká mi v tvé odpovědi, jak ten systém pozná, že Str.sub s 20 ve větvi else vrátí vždy korektní minimální čtyři znaky. (Tedy v mém případě pozná, že nevrátí, a tudíž nahlásí chybu.)

1468

Vývoj / Re:Curryfikované funkce v Haskellu

« kdy: 01. 05. 2018, 12:18:16 »

Nebo to má nějaký zajímavý efekt, který mi uniká?

Důležitý rozdíl je třeba ten, že nemusíš předat všechny parametry funkci najednou. Můžeš třeba navázáním jedničky udělat ze součtu inkrement a ten pak jako funkci s jedním parametrem předat dál. Ten inkrement je školometský příklad ale prakticky se to hodí třeba u callbacků. Tam se musí k funkci přibalit nějaká data skoro vždycky.
Sice se to dá ve většině jazyků více i méně rozumně obejít, ale když to podporuje typový systém, tak můžeš podle potřeby  přibalovat data i tam, kde to autora původního kódu ani nenapadlo.

Prosím, psal jsem "Jako já s tím nemám problém. Curryfikování je fajn věc, a umím to použít.".

Takže je tam nějaký zajímavý efekt, který mi uniká?

1469

Vývoj / Re:Formální verifikace podle typu na rozsah

« kdy: 01. 05. 2018, 01:41:41 »

To jsou závislostní typy, verifikace se dělá přes theorem proving (takže překlad programu někdy trvá hodiny). Viz například jazyk Idris.

Mohl by si prosím lidsky popsat princip, jak se ta verifikace dělá?

1470

Vývoj / Formální verifikace podle typu na rozsah

« kdy: 01. 05. 2018, 00:57:43 »

Zdravím.

Mějme takovouto funkci v blíže neurčeném jazyku podobném haskellu:

Kód: [Vybrat]

fn s : String 0 40 -> String 4 20 =
    if (Str.len s) < 2 then
        "default"
    else
        Str.sub s 20

Čtěte to prosím jako "funkce fn má jeden parametr typu String který je minimálně nula znaků dlouhý, a maximálně 40; a vrací String, který je minimálně čtyři znaky dlouhý a maximálně 20.

A mě by zajímalo, jak má nebohý typový systém odvodit, že ta funkce je špatně?

(Tak jasně, můžu na to pustit testy, ale já bych rád zůstal jen u typů a formální verifikace.)

Díky.