Zobrazit příspěvky

Tato sekce Vám umožňuje zobrazit všechny příspěvky tohoto uživatele. Prosím uvědomte si, že můžete vidět příspěvky pouze z oblastí Vám přístupných.


Příspěvky - BoneFlute

Stran: 1 ... 47 48 [49] 50 51 ... 133
721
Vývoj / Re:Naivní závislostní typ (úvaha)
« kdy: 15. 11. 2019, 17:45:39 »
ta funkce pak má typ Nat->y:Nat->Not (y=0)->Nat.

Můžeš mi prosím, v nějakém srozumitelnějším pseudo jazyku s hodně komentáři popsat, cože to vlastní říká? Jsem na to Nat už narazil mnohokrát. Vždycky tím začíná každá učebnice Idris a Agdy, a já to prostě neumím přečíst. (Předpokládám, že Nat je jako Natural - přirozené číslo?)
Jo, Nat jsou přirozená čísla. Když T je typ, tak Not T se definuje jako T->Void (kde Void je typ bez hodnot, odpovídající false v intuicionistické logice), typ třetího parametru je tedy (y=0)->Void. Možná si spíš představ něco jako typ NonZero n:Nat, kde bude konstruktor NonZero (Succ n). Popravdě tento příklad není úplně nejjednodušší, protože obsahuje rovnostní typ a negaci.

Taky jsem to bohužel nedal, promiň :-(

Když by si uvedl nějaký příklad s něčím tedy jednodužším?

722
Vývoj / Re:Naivní závislostní typ (úvaha)
« kdy: 15. 11. 2019, 17:15:03 »
ta funkce pak má typ Nat->y:Nat->Not (y=0)->Nat.

Můžeš mi prosím, v nějakém srozumitelnějším pseudo jazyku s hodně komentáři popsat, cože to vlastní říká? Jsem na to Nat už narazil mnohokrát. Vždycky tím začíná každá učebnice Idris a Agdy, a já to prostě neumím přečíst. (Předpokládám, že Nat je jako Natural - přirozené číslo?)

723
Vývoj / Re:Naivní závislostní typ (úvaha)
« kdy: 15. 11. 2019, 17:10:45 »
V mé úvaze jsem dospěl k tomu, že potřebuju:

Zavést tu kaskádu typů. Mám Numeric a z něj "dědí" PositiveUnzeroNumeric
Mít "nonzero" typ není asi úplně ideální, to je virální až to bolí. Nechci nikomu kazit iluze, ale tohle je zrovna učebnicový příklad ...

Tak není to virální až dolů, bych řekl.

A zase musíš na mě pomalu. Už vím jak se cejtil kamoš, když jsem mu vysvětloval Promise :-)

Každopádně díky.

724
/dev/null / Re:Těžké OOP problémy
« kdy: 15. 11. 2019, 17:04:27 »
Ta smrt byla adekvátní. Adam s Evou přesně a jasně věděli do čeho jdou. Oni nebyli děti. Nelze na ně pohlížet jako na nezkušené, naivní, nebo psychicky nedostatečné. Na to, co se po nich chtělo byly vybavení více než dostatečně. A trest, který dostali je z dnešní pohledu naprosto ale naprosto nedostačující.
Nemohu souhlasit. Z dnešního pohledu českých zákonů i z dnešního pohledu věřících je trest smrti nepřiměřený

Z dnešního pohledu toho, k čemu to jeho/jejich rozhodnutí vedlo. Čistě univerzalisticky. Pro mě dnešní právo není vrcholem spravedlonosti. Je to jen smutnej kompromis.

Uniká ti detail, že trest smrti je odmítaný ne proto, že by byl nepřiměřený. Ale proto, že je nevratný v případě, že by došlo k omylu. Pokud si myslíš něco jiného, tak si to mysli, je mi to celkem jedno.

Každopádně by mě třeba zajímalo kolik let vězení by jsi třeba zrovna ty dal někomu, kdo vědomě a čistě pro svůj pocit způsobil smrt čtrnácti miliardám lidí.

Abychom to rozlouskli, člověk má nárok na život? Ty mě přivedeš nějakýho člověka ke mě do baráku, a já jsem povinnen ho živit, šatit, dát mu napít, a on bude jen čumět na bednu a šikanovat moje děti?

Budu mluvit za sebe. To, že jsou "stará" náboženství založena na diktatuře je jedna z hlavních překážek, proč se nemohu stát věřícím.
Tohle je celkem přesné. A je to asi většinový důvod, proč lidé nejsou věřící. Ostatně to není nic nového. Přesně tento důvod byl už na počátku. Přesně ze stejného důvodu Adam s Evou dopadli jak dopadli.

Už ti to řekl Mirek Prýmek a řeknu ti to i já. Na tvůj názor, jestli je Bůh diktátor není nikdo zvědavej. Nikoho to nezajímá, smiř se s tím. To, zda věříš, nebo nevěříš v Boha opravdu ale opravdu není podstatné. A už vůbec to neovlivní, zda Bůh existuje. To je prostě jen taková naivita lidí, kteří si myslí, že když v Boha nebudou věřit, tak on jakože zmizí, nebo co.

Klidně je možné, že Bůh, jak jej popisuje Bible není. Klidně je možné, že není vůbec. Taky je možné, že tím jediným a skutečný Bohem je Alláh (allah yakhlusuna). A taky je možné, že skutečnými bohy jsou ti bohové Olympští. A když bychom měli fakt velkou smůlu, tak Prastaří.

Já teda doufám, že tak velkou smůlu nemám, a existuje Bůh s vlastnostmi, které jsou popsané v Bibli, a udělá co slíbil udělat.

725
Vývoj / Re:Naivní závislostní typ (úvaha)
« kdy: 15. 11. 2019, 16:42:49 »
Šlo by tímto způsobem na úrovni typového systému zabránit dělení nulou?
Ano, šlo. Je nebetyčná blbost, že by to fungovalo jen s konstantními výrazy, kdo to tvrdí, netuší nic o symbolických výrazech. Ovšem ve složitějším kódu by si to vyžádalo součtové závislostní typy, které jsou “virální” podobně jako zvedání typů pomocí funktorů. Čili technicky to jde a posílí to typovou kontrolu, ale za cenu menší intuitivnosti.
Mohl by si to rozvést?

V mé úvaze jsem dospěl k tomu, že potřebuju:

Zavést tu kaskádu typů. Mám Numeric a z něj "dědí" PositiveUnzeroNumeric který je jeho podmnožinou (subtyp?). A nějaký instrumenty na to, jak to zapsat.

Pak mi všechno začne "magicky" fungovat, a nic dalšího bych neměl potřebovat. Protože typový systém, tak jak by byl, tak jak ho známe, by my automaticky vyhodil místa, kde ty typy nebudou sedět. Konkrétně třeba:
Kód: [Vybrat]
calculate :: Numeric -> Numeric -> Numeric
calculate a b = a `div` (b - 3)

Stejně tak funkce inc a, nebo for cyklus (ve skutečnosti to bude funkce map), to všechno se automaticky vyhodí, protože ty typy nebudou sedět. Což mi přijde intuitivní dost. Ale třeba mi ještě něco nedochází.

Jaké součtové typy by to vyžadovalo v jakém případě? To je asi to co mě zajímá. Protože takhle mi přijde, že víc toho nepoutřebuju.

problém (ko|kontra)variance - můžeš do l: List Int vložit x : Age? Když ho potom z listu vybíráš, vrátí se ti Int nebo Age?
Tak naivně předpokládám, že ano, může ho tam vložit, protože Age je Int (zatímco Int není Age). A když ho vyberu tak...
No, to by chtělo příklad. Protože tak co, může to vráti Age. A funkce, která vyžaduje pole Intů a dostane pole Ageů, tak s tím Age bude pracovat jako s Intem, tak by furt mělo všechno fungovat... Co mi uniká?

...no a druhá možnost je, že to nebudou podtypy. Pak to ale bude strašná otrava používat.
A co to pak bude? A jak by to teda vypadalo?

726
/dev/null / Re:Těžké OOP problémy
« kdy: 14. 11. 2019, 23:38:37 »
Není z toho jasné, že jsem měl na mysli naše lidské/české zákony? V těch je definice vraždy. Nebo snad nesouhlasíš, že by potopa, nebo Sodoma-Gomora nesplňovala definici vraždy podle současných českých zákonů?
Přijde ti velice vzácná obchodní návštěva, k tobě domů. Tři dívky. Pozveš si je k sobě domů a pohostíš. A když tu náhle se ti do bytu vláme banda chuligánů, kteří ty tři dívky opakovaně znásilní tak, že na to zemřou.
Toliko příměr (nepřesný, zavádějící, a vůbec).
Ale mě by zajímalo, uznáváš, že podle českých zákonů tito chuligáni by mohli být alespoň na pár let zavření do vězení? Že jo? Nebo ne? Nebo ti přijde, že potrestání všech deseti chuligánů je příliš, a že by měl být potrestán jen jeden, protože potrestat všechny by bylo genocidní?

Já ti toto píšu ne jako odpověď na tvou otázku, ale jako ukázku toho, jak absurdně se ptáš.
Já bych pro ně chtěl trest smrti, protože by to pro mě bylo velice osobní, cítil bych nenávist a toužil po pomstě, ale můj rozum mi říká, že o tom musí rozhodnout někdo nezávislý a nezaujatý a musí posoudit všechny okolnosti jednotlivě. Co když mezi těmi chuligány byl ňáký borec co ho chytli náhodou venku a pohrozili mu, že když nepůjde s nimi, tak mu vyvraždí rodinu?

Není to tak správnější, posuzovat lidi jednotlivě a uložit různé tresty podle výše provinění?

Nechápu jak mi má tvůj příklad ukázat, že se ptám absurdně. Absurdní samozřejmě je každá hádanka s Bohem, ale jak jsem psal Mirkovi o "kapání" ze zkumavky, tak nevidím nic absurdního na tom použít Boha jako symboliku vlastností a pracovat s ním v určité teorii, ať už logické nebo právní, to je fuk.

Pokračování zítra. :-)

Protože těch chuligánů bylo plné město. Protože všichni to dělali bez donucení. Protože to bylo posouzeno spravedlivě, jednotlivě, zohledněny všechny polehčující okolnosti, a žádné se nenašli.

A tak přišel kat.

Pak po čtyřech tisíci letech přijde někdo, kdo se s případem ani neseznámí, komu se to baj oko zdá moc, a začne to komentovat.

727
/dev/null / Re:Těžké OOP problémy
« kdy: 14. 11. 2019, 23:18:13 »
... k nám do demokracie a zeptáš se toho nejzarytějšího demokrata, který věří v Boha, tak najednou Bůh přestane být diktátorem, ale přitom nic ze svých diktátorských vlastností neztratil.
Bůh je totalitní autokrat, vo tom přece nic. Ano, určuje jak máme myslet (totalitní), a ano, je svrchovaný vládce a nikomu než sobě se nezpovídá (autokrat). To bylo to co chceš vědět?

728
Vývoj / Re:Naivní závislostní typ (úvaha)
« kdy: 14. 11. 2019, 23:02:23 »
Tak jak jsi ten problém popsal, je snad jasné, že

Kód: [Vybrat]
calculate a b

kde a b jsou čísla z venku, žádnou compile time chybu generovat nemůže.

Pokud myslíš něco jako:
Kód: [Vybrat]
main :: IO ()
main = do
    a <- getLine
    b <- getLine
    putStrLn $ format $ calculate (parseNumeric a) (parseNumeric b)
Tak mi je jasné, že fungovat bude. Respektive se to nepřeloží. V tomto by být problém neměl.

729
Vývoj / Re:Naivní závislostní typ (úvaha)
« kdy: 14. 11. 2019, 22:46:22 »
Citace
Jaké to může mít úskalí?

funguje to jen s konstantními výrazy.

Můžeš to prosím rozvést? Co myslíš konstantními výrazy a co myslíš tím nefunguje.

730
/dev/null / Re:Těžké OOP problémy
« kdy: 14. 11. 2019, 22:36:46 »
Není z toho jasné, že jsem měl na mysli naše lidské/české zákony? V těch je definice vraždy. Nebo snad nesouhlasíš, že by potopa, nebo Sodoma-Gomora nesplňovala definici vraždy podle současných českých zákonů?

Budu vycházet z předpokladu, že jsi nevěřící, že jsi Bibli viděl ve vitríně, že o Sodomě Gomoře jsi viděl maximálně film (nic z toho nepovažuji za problém, jen si připravuji půdu).

Přijde ti velice vzácná obchodní návštěva, k tobě domů. Tři dívky. Pozveš si je k sobě domů a pohostíš. A když tu náhle se ti do bytu vláme banda chuligánů, kteří ty tři dívky opakovaně znásilní tak, že na to zemřou.

Toliko příměr (nepřesný, zavádějící, a vůbec).

Ale mě by zajímalo, uznáváš, že podle českých zákonů tito chuligáni by mohli být alespoň na pár let zavření do vězení? Že jo? Nebo ne? Nebo ti přijde, že potrestání všech deseti chuligánů je příliš, a že by měl být potrestán jen jeden, protože potrestat všechny by bylo genocidní?

Já ti toto píšu ne jako odpověď na tvou otázku, ale jako ukázku toho, jak absurdně se ptáš.



Jako příklad dívek jsem uvedl protože jsem nechtěl zabrušovat do homosexuálního světa. Nehledej v tom žádné prasečinky.


S tou smrtí:
Já to chápu tak, že Adam hrubě porušil domovní řád a vydupal si, že nechce Boží autoritu. Tak mu vyhověl.
Opravdu to takto Bible popisuje? Jako vydupání si odchodu a aktivní snahu vypadnout z ráje? A když už byl Adam s kufrem přededveřma tak křičel "já už se těším na smrt"?
Já tam tehdá nebyl, tak nemůžu říct. Ale podle popisu toho, tak ano, tak nějak to bylo. Je tam spoustu detailů, které jsou obávám se mimo tvou rozlišovací schopnost, a tak to nebudu rozebírat a můžeš nebo nemusíš mi věřit.

Děti si často chtějí vydupat nějakou hračku, ale nemůžeš jim za to udělit jeden z nejtvrdších trestů (né-li nejtvrší) který exituje - smrt.
Ta smrt byla adekvátní. Adam s Evou přesně a jasně věděli do čeho jdou. Oni nebyli děti. Nelze na ně pohlížet jako na nezkušené, naivní, nebo psychicky nedostatečné. Na to, co se po nich chtělo byly vybavení více než dostatečně. A trest, který dostali je z dnešní pohledu naprosto ale naprosto nedostačující.

Děti (copak děti, dělaj to i dospělí) si často chtějí vydupat nějakou hračku. A pak když ji dostanou, tak jsou hrozně tvrdě potrestaní, protože je to další věc kterou si musí uklízet. Ano, je to strašně nespravedlivé, od rodičů kruté, a ti rodiče by měli být potrestání tím, že jim bude odňato právo na existenci.


731
Vývoj / Naivní závislostní typ (úvaha)
« kdy: 14. 11. 2019, 22:09:42 »
Mějme hypotetický jazyk s hypotetickým typovým systémem.

Mějme typ Numeric reprezentující všechna reální čísla, a pak následující kaskádu typů:

Numeric > Int > Age > Young
Numeric > PositiveUnzeroNumeric
Kde Age je rozsah 0 - 255, Young 0 - 19, PositiveUnzeroNumeric rozsah 1 - MAX_INT

Máme funkci pro dělení:
Kód: [Vybrat]
div a b = a / b

A dáme jí takovouto typovou signaturu:
Kód: [Vybrat]
div :: Numeric -> PositiveUnzeroNumeric -> Numeric

Šlo by to? Šlo by tímto způsobem na úrovni typového systému zabránit dělení nulou? Možná ne, ale zajímalo, jestli by se k tomu někdo zkušenější mohl vyjádřit. Protože třeba:

Kód: [Vybrat]
calculate :: Numeric -> Numeric -> Numeric
calculate a b = a `div` (b - 3)
calculate 9 6 -- 3
calculate 9 3 -- divide zero
se IMHO nepřeloží.

Jaké to může mít úskalí?

732
/dev/null / Re:Těžké OOP problémy
« kdy: 14. 11. 2019, 19:47:13 »
Ty si vazne nevybiras ty lehci cesty co?
Pro mě je to důležité téma, protože to nemám jako koníčka. Takže se snažím, abych se za své rozhodnutí nemusel stydět.

Na ktery ruce si strihas nehty jako prvni?
Na levé. Protože jsem pravák a na pravé levou to neumím, takže mi to stříhá moje Paní. Co jsi z toho vyvodil? :-)

No zajimalo me jestli to tak mas se vsim. Zdalo se mi, ze pozoruju i v jinych tematech, ze se snazis jit tou "dokonalou" cestou i kdyz je to tezky a existuje zkratka na skoro stejne a dostatecne dobre misto. (viz TS versus UT, ale nechci to znova otevirat :-))
Tak nemůžeš soudit podle fóra.

Řekl bych, že v práci víc používám good-enought.

Co se Boha týče, tak mě přijde poněkud naprd, hrát si na náboženství, když z toho nic není. A pokud věřím, že Bůh existuje, a já ho budu poslouchat jen na půl, tak ho akorád naštvu, to mi taky nepřijde jako rozumné.

733
/dev/null / Re:Těžké OOP problémy
« kdy: 14. 11. 2019, 18:36:39 »
S tím nemohu souhlasit. Pokud by nebyl zákon i nad Bohem, tak by nešlo prohlásit, že Bůh je spravedlivý.
Myslíš "spravedlivý" jako to české slovo, nebo to hebrejské slovo, které takhle překládáme (https://www.blueletterbible.org/lang/lexicon/lexicon.cfm?t=kjv&strongs=h6663)? To jsou totiž dvě dost rozdílné věci. Viz např. ocenění "spravedlivý mezi národy", to fakt není cena pro soudce :)

No a pokud by nějaký zákon nad Bohem byl, jaký? Kde je zapsaný? Jak víme, co v něm je?

A to bral takovej Abraham jako jasnou věc.
No mě by zajímalo třeba, když dostal příkaz zabít svého jediného syna, který vůbec nic neudělal, jestli si v tu chvíli říkal "Jo! To je spravedlivé!" :)
Pravděpodobně si říkal "to je divné, ale tak On asi ví co dělá, a kdyžtak ho vzkřísí, nebo tak něco, protože to by nebylo spravedlivé". Soudě podle toho, jak je tato událost v Bibli popisována.

Tím zákonem nad Bohem samozřejmě myslím zákon, který stanovil On sám. A pak jde o to, že ho sám dodržuje.

Abraham to formuloval tak, že "je nepředstavitelné, že bys usmrtil se špatnými i spravedlivé, neučiní soudce celé země co je správné? Je nepředstavitelné, že by si to udělal."

Můžeme se bavit o tom, kde a jak a zda je ten zákon napsaný, ale Abraham ho evidentně "vnímal". A to dokonce v době, kdy žádné desatero nebylo. (V tomto detailu máš pravdu, desatero se týkalo jen Izraelského národa. Ale je na něm vidět "cit pro spravedlnost" který Bůh má.)

Raději bych za Abraháma moc nemluvil, víme prd, co si myslel a co bral jako "jasnou věc"...
Tak on (Abraham) to řekl, jde si o tom přečíst, tak nevím proč bych to nemohl použít. Je spousta věcí které nevím, tak nevím proč bych měl nevědět věci které vědět jde :-)


Něco jiného je samozřejmě detail, že Bůh ten zákon nikdy nepřekročil i když to někteří lidé chtějí vidět.
Tak pokud bysme věděli, jaký zákon to je a jaké je jeho znění, mohli bysme se bavit o tom, jestli ho Bůh někdy překročil nebo ne. Já to ale nevím, nikde jsem nikde nic takového nečetl. Ty jo?
Nikde jsem nečetl co, že by Bůh někdy překročil svá vlastní pravidla? Ano, to jsem nikdy nečetl. A ano, je mi jasné, že to, že jsem to nečetl neznamená, že se to nestalo. Ale nemám problém uplatni pravidlo presumpce neviny i na takovou bytost, jako je Bůh.

Přičemž jsem četl případy, kdy lidé, i andělé mohli prohlásit pokud by bylo na co. (Samozřejmě tiše předpokládáme, že Bůh třeba nezneužil svou moc aby nezamaskoval své přešlapy a tak, ale to je jednak poněkud nelogické - opět, proč by to dělal, není snazší aby ty přešlapy prostě nedělal, a druhak i kdyby, tak je to informace k ničemu.)

Ale třeba jsem četl případy kdy bůh nepřekročil svá vlastní pravidla a docela ho to dost "bolelo". V mnoha různých podobách, ať už co se týče hrdosti, osobních citů, etc.

734
/dev/null / Re:Těžké OOP problémy
« kdy: 14. 11. 2019, 18:13:06 »
Ty si vazne nevybiras ty lehci cesty co?
Pro mě je to důležité téma, protože to nemám jako koníčka. Takže se snažím, abych se za své rozhodnutí nemusel stydět.

Na ktery ruce si strihas nehty jako prvni?
Na levé. Protože jsem pravák a na pravé levou to neumím, takže mi to stříhá moje Paní. Co jsi z toho vyvodil? :-)

735
/dev/null / Re:Těžké OOP problémy
« kdy: 14. 11. 2019, 14:42:43 »
S tou smrtí:

Já to chápu tak, že Adam hrubě porušil domovní řád a vydupal si, že nechce Boží autoritu. Tak mu vyhověl.

Adam se odstěhoval, a ztratil nárok na kyslík, vodu, prostor, společnost.

Když domácímu zničím kvartýr, a pak si seženu skupinu lidí, kteří mne podpoří v mém požadavku že domácí je povinnen mi zajistit abych nebydlel na ulici.

Samozřejmě vím že jsou lidé kterým to dokonce ani nepřijde absurdní.

Stran: 1 ... 47 48 [49] 50 51 ... 133