Co si myslíte o OOP?

[v]

pro srovnání idris:

Kód: [Vybrat]

inc : (n : Nat) -> (m : Nat ** m = n + 1)
inc n = (n + 1 ** Refl)
přírůstek můžete přepsat podle potřeby, pokud se liší v typu a těle, neprojde typecheckerem

Pripomnel jsi mi, ze jsem se chtel - az budu mit nekdy trochu vic casu na ptakoviny* - na nejaky jazyk s dependent types podivat. Idris je horky kandidat. Pouzival jsi ho nekdy trochu vic? Doporucil bys ho na hrani nebo radsi neco jinyho?

* takze nejspis nejdriv tak v duchodu

znám jenom letmo idris a agdu jsem viděl z vlaku... ale doporučil, příbuznost s haskellem je IMHO velká výhoda, jinak ten-jehož-jméno-je-nestálé o tom asi ví víc
pro zajímavost, blodwen/idris 2 https://www.youtube.com/watch?v=mOtKD7ml0NU

[Reklama]

[BaldSlattery]

Aha, takže úplně stejně to udělám, když budu chtít napsat funkci inc4096, která zvýší hodnotu o 4096?

V podstate jo, akorat pouzijes silnejsi typovy system, kde se to "funkce zvysuje o 4096" zapise v typech rovnou s konstantou 4096.

Neni to pak (co do psani) odlisne od toho, mit test, ktery overi, jestli je vystup skutecne o 4096 vyssi nez vstup.

nebo se přidá pár type families a napíše se třeba

Kód: [Vybrat]

Nat' n -> Nat' (Plus (Exp (S (S Z)) (S (S (S (S (S (S (S (S (S (S (S (S Z))))))))))))) n)hnus, ale taky úplně umělý příklad

A co třeba kdybych chtěl funkci inc1234567, která bude přidávat 1234567? To budu zase vymýšlet podobnou bejkárnu?

jestli potřebujete funkci inc1234567 tak dobře vám tak

Tohle uz ma jiny principialni problem. Ten typ je radove slozitejsi nez sama funkce, takze je tu otazka, kdo bude kontrolovat spravnost zapisu typu :-).

pro srovnání idris:

Kód: [Vybrat]

inc : (n : Nat) -> (m : Nat ** m = n + 1)
inc n = (n + 1 ** Refl)


Hic svnt dracones 

[BaldSlattery]

pro srovnání idris:

Kód: [Vybrat]

inc : (n : Nat) -> (m : Nat ** m = n + 1)
inc n = (n + 1 ** Refl)
přírůstek můžete přepsat podle potřeby, pokud se liší v typu a těle, neprojde typecheckerem

Pripomnel jsi mi, ze jsem se chtel - az budu mit nekdy trochu vic casu na ptakoviny* - na nejaky jazyk s dependent types podivat. Idris je horky kandidat. Pouzival jsi ho nekdy trochu vic? Doporucil bys ho na hrani nebo radsi neco jinyho?

* takze nejspis nejdriv tak v duchodu

Jako první bych ho nedoporučil, má implicitní argumenty, při učení člověk jen zírá, kde se ztrácí proměnné.

[Mirek Prýmek]

Jako první bych ho nedoporučil, má implicitní argumenty, při učení člověk jen zírá, kde se ztrácí proměnné.

Takze radsi Agdu? Nebo jeste neco jinyho?

[Tom@as]

Aha, takže úplně stejně to udělám, když budu chtít napsat funkci inc4096, která zvýší hodnotu o 4096?

V podstate jo, akorat pouzijes silnejsi typovy system, kde se to "funkce zvysuje o 4096" zapise v typech rovnou s konstantou 4096.

Neni to pak (co do psani) odlisne od toho, mit test, ktery overi, jestli je vystup skutecne o 4096 vyssi nez vstup.

nebo se přidá pár type families a napíše se třeba

Kód: [Vybrat]

Nat' n -> Nat' (Plus (Exp (S (S Z)) (S (S (S (S (S (S (S (S (S (S (S (S Z))))))))))))) n)hnus, ale taky úplně umělý příklad

A co třeba kdybych chtěl funkci inc1234567, která bude přidávat 1234567? To budu zase vymýšlet podobnou bejkárnu?

jestli potřebujete funkci inc1234567 tak dobře vám tak

Tohle uz ma jiny principialni problem. Ten typ je radove slozitejsi nez sama funkce, takze je tu otazka, kdo bude kontrolovat spravnost zapisu typu :-).

pro srovnání idris:

Kód: [Vybrat]

inc : (n : Nat) -> (m : Nat ** m = n + 1)
inc n = (n + 1 ** Refl)


Hic svnt dracones 

Tak to už je šílené tolik vnořených komentářů

[Reklama]

[BaldSlattery]

Aha, takže úplně stejně to udělám, když budu chtít napsat funkci inc4096, která zvýší hodnotu o 4096?

V podstate jo, akorat pouzijes silnejsi typovy system, kde se to "funkce zvysuje o 4096" zapise v typech rovnou s konstantou 4096.

Neni to pak (co do psani) odlisne od toho, mit test, ktery overi, jestli je vystup skutecne o 4096 vyssi nez vstup.

nebo se přidá pár type families a napíše se třeba

Kód: [Vybrat]

Nat' n -> Nat' (Plus (Exp (S (S Z)) (S (S (S (S (S (S (S (S (S (S (S (S Z))))))))))))) n)hnus, ale taky úplně umělý příklad

A co třeba kdybych chtěl funkci inc1234567, která bude přidávat 1234567? To budu zase vymýšlet podobnou bejkárnu?

jestli potřebujete funkci inc1234567 tak dobře vám tak

Tohle uz ma jiny principialni problem. Ten typ je radove slozitejsi nez sama funkce, takze je tu otazka, kdo bude kontrolovat spravnost zapisu typu :-).

pro srovnání idris:

Kód: [Vybrat]

inc : (n : Nat) -> (m : Nat ** m = n + 1)
inc n = (n + 1 ** Refl)


Hic svnt dracones 

Tak to už je šílené tolik vnořených komentářů

Tak to už nezhoršujte 

[Mirek Prýmek]

Aha, takže úplně stejně to udělám, když budu chtít napsat funkci inc4096, která zvýší hodnotu o 4096?

V podstate jo, akorat pouzijes silnejsi typovy system, kde se to "funkce zvysuje o 4096" zapise v typech rovnou s konstantou 4096.

Neni to pak (co do psani) odlisne od toho, mit test, ktery overi, jestli je vystup skutecne o 4096 vyssi nez vstup.

nebo se přidá pár type families a napíše se třeba

Kód: [Vybrat]

Nat' n -> Nat' (Plus (Exp (S (S Z)) (S (S (S (S (S (S (S (S (S (S (S (S Z))))))))))))) n)hnus, ale taky úplně umělý příklad

A co třeba kdybych chtěl funkci inc1234567, která bude přidávat 1234567? To budu zase vymýšlet podobnou bejkárnu?

jestli potřebujete funkci inc1234567 tak dobře vám tak

Tohle uz ma jiny principialni problem. Ten typ je radove slozitejsi nez sama funkce, takze je tu otazka, kdo bude kontrolovat spravnost zapisu typu :-).

pro srovnání idris:

Kód: [Vybrat]

inc : (n : Nat) -> (m : Nat ** m = n + 1)
inc n = (n + 1 ** Refl)


Hic svnt dracones 

Tak to už je šílené tolik vnořených komentářů

Tak to už nezhoršujte 

Coze?

[BaldSlattery]

Jako první bych ho nedoporučil, má implicitní argumenty, při učení člověk jen zírá, kde se ztrácí proměnné.

Takze radsi Agdu? Nebo jeste neco jinyho?

Na naučení asi (nebo spíše rozhodně) ne. Na první lekce Pie (z knihy The little typer), nemá implicitní parametry, takže jsou všechna odvození (důkazy) názorně vidět.

[BaldSlattery]

Aha, takže úplně stejně to udělám, když budu chtít napsat funkci inc4096, která zvýší hodnotu o 4096?

V podstate jo, akorat pouzijes silnejsi typovy system, kde se to "funkce zvysuje o 4096" zapise v typech rovnou s konstantou 4096.

Neni to pak (co do psani) odlisne od toho, mit test, ktery overi, jestli je vystup skutecne o 4096 vyssi nez vstup.

nebo se přidá pár type families a napíše se třeba

Kód: [Vybrat]

Nat' n -> Nat' (Plus (Exp (S (S Z)) (S (S (S (S (S (S (S (S (S (S (S (S Z))))))))))))) n)hnus, ale taky úplně umělý příklad

A co třeba kdybych chtěl funkci inc1234567, která bude přidávat 1234567? To budu zase vymýšlet podobnou bejkárnu?

jestli potřebujete funkci inc1234567 tak dobře vám tak

Tohle uz ma jiny principialni problem. Ten typ je radove slozitejsi nez sama funkce, takze je tu otazka, kdo bude kontrolovat spravnost zapisu typu :-).

pro srovnání idris:

Kód: [Vybrat]

inc : (n : Nat) -> (m : Nat ** m = n + 1)
inc n = (n + 1 ** Refl)


Hic svnt dracones 

Tak to už je šílené tolik vnořených komentářů

Tak to už nezhoršujte 

Coze?

[Mirek Prýmek]

Na naučení asi (nebo spíše rozhodně) ne. Na první lekce Pie (z knihy The little typer), nemá implicitní parametry, takže jsou všechna odvození (důkazy) názorně vidět.

Dik!

[BaldSlattery]

Na naučení asi (nebo spíše rozhodně) ne. Na první lekce Pie (z knihy The little typer), nemá implicitní parametry, takže jsou všechna odvození (důkazy) názorně vidět.

Dik!

Je to na githubu.

[Mirek Prýmek]

Je to na githubu.

Jo, videl jsem.

[Ondra Satai Nekola]

Tak jsem chtel overit tu haskell ukazku a zjistil, ze haskell je tak okrajovy jazyk, ze neni k dispozici v termuxu. Hledal jsem balicek s nazvem haskell nebo ghc. Seznam balicku: https://pastebin.com/kdfgUFRt To jen upevnuje me presvedceni, ze nema smysl ztracet cas okrajovymi nepodporovanymi jazyky.  Je schopen to nekdo predvest v jinem jazyku ktery je mezi balicky? (je tam kde co, rust, vala, erlang, java, ocaml, golang, clang, racket, ...)  Nebo se jedna ciste o schopnost haskellu, ktera je tu mylne prisuzovana jazykum se statickymi typy?

To je tak pitomá metrika (přítomnost v termuxu) a tak pitomý argument (když je to v Haskellu a opírá se to o statické typy, tak to nutně je demonstrace výhod statických typů)...

Neni to demonstrace vyhod statickych typu, pokud je haskell jediny jazyk, ktery to umi. V takovem pripade je to demonstrace vyhoda haskellu. Na tom zalozene tvrzeni o statickych typech je argumentacni klam, predcasna generalizace.

Ale houby, umi to s drobnymi rozdily kopec jazyku (o Scale a F# tu uz rec sla), ten Haskell se proste bere jako "zlaty standard", co ho navic pomalu kazdy zna.

Zatim to spis vypada na vlastnost funkcionalnich jazyku, porad cekam na nejaky normalni. :-)

Normální? Oba jsou to multiparadigmatické jazyky.

Normalni, to jest ty, ktere se bezne pouzivaji v komercni praxi.

Tak to jsou normální.

:-)) Ohledne moznosti zneuznaneho a neuspesneho haskellu mi muzes veset buliky na nos, ohledne bezne pouzivanych jazyku v komercni sfere nikoliv.

To je takovy problem se podivat do inzeratu? Scala neni zdaleka takova masovka jako trebas Java, ale misto se najde bez problemu. Pokud zuzis sve pozadavky na "zajimava prace", tak se ten pomer navic dost zlepsi...

[operator]

Tak jsem chtel overit tu haskell ukazku a zjistil, ze haskell je tak okrajovy jazyk, ze neni k dispozici v termuxu. Hledal jsem balicek s nazvem haskell nebo ghc. Seznam balicku: https://pastebin.com/kdfgUFRt To jen upevnuje me presvedceni, ze nema smysl ztracet cas okrajovymi nepodporovanymi jazyky.  Je schopen to nekdo predvest v jinem jazyku ktery je mezi balicky? (je tam kde co, rust, vala, erlang, java, ocaml, golang, clang, racket, ...)  Nebo se jedna ciste o schopnost haskellu, ktera je tu mylne prisuzovana jazykum se statickymi typy?

To je tak pitomá metrika (přítomnost v termuxu) a tak pitomý argument (když je to v Haskellu a opírá se to o statické typy, tak to nutně je demonstrace výhod statických typů)...

Neni to demonstrace vyhod statickych typu, pokud je haskell jediny jazyk, ktery to umi. V takovem pripade je to demonstrace vyhoda haskellu. Na tom zalozene tvrzeni o statickych typech je argumentacni klam, predcasna generalizace.

Ale houby, umi to s drobnymi rozdily kopec jazyku (o Scale a F# tu uz rec sla), ten Haskell se proste bere jako "zlaty standard", co ho navic pomalu kazdy zna.

Zatim to spis vypada na vlastnost funkcionalnich jazyku, porad cekam na nejaky normalni. :-)

Normální? Oba jsou to multiparadigmatické jazyky.

Normalni, to jest ty, ktere se bezne pouzivaji v komercni praxi.

Tak to jsou normální.

:-)) Ohledne moznosti zneuznaneho a neuspesneho haskellu mi muzes veset buliky na nos, ohledne bezne pouzivanych jazyku v komercni sfere nikoliv.

To je takovy problem se podivat do inzeratu? Scala neni zdaleka takova masovka jako trebas Java, ale misto se najde bez problemu. Pokud zuzis sve pozadavky na "zajimava prace", tak se ten pomer navic dost zlepsi...

Pro mě jsou zajímavé zakázky. Nikdo z našich klientů (podniková sféra) takové obskurnosti nepoptává.

[Ondra Satai Nekola]

Tak jsem chtel overit tu haskell ukazku a zjistil, ze haskell je tak okrajovy jazyk, ze neni k dispozici v termuxu. Hledal jsem balicek s nazvem haskell nebo ghc. Seznam balicku: https://pastebin.com/kdfgUFRt To jen upevnuje me presvedceni, ze nema smysl ztracet cas okrajovymi nepodporovanymi jazyky.  Je schopen to nekdo predvest v jinem jazyku ktery je mezi balicky? (je tam kde co, rust, vala, erlang, java, ocaml, golang, clang, racket, ...)  Nebo se jedna ciste o schopnost haskellu, ktera je tu mylne prisuzovana jazykum se statickymi typy?

To je tak pitomá metrika (přítomnost v termuxu) a tak pitomý argument (když je to v Haskellu a opírá se to o statické typy, tak to nutně je demonstrace výhod statických typů)...

Neni to demonstrace vyhod statickych typu, pokud je haskell jediny jazyk, ktery to umi. V takovem pripade je to demonstrace vyhoda haskellu. Na tom zalozene tvrzeni o statickych typech je argumentacni klam, predcasna generalizace.

Ale houby, umi to s drobnymi rozdily kopec jazyku (o Scale a F# tu uz rec sla), ten Haskell se proste bere jako "zlaty standard", co ho navic pomalu kazdy zna.

Zatim to spis vypada na vlastnost funkcionalnich jazyku, porad cekam na nejaky normalni. :-)

Normální? Oba jsou to multiparadigmatické jazyky.

Normalni, to jest ty, ktere se bezne pouzivaji v komercni praxi.

Tak to jsou normální.

:-)) Ohledne moznosti zneuznaneho a neuspesneho haskellu mi muzes veset buliky na nos, ohledne bezne pouzivanych jazyku v komercni sfere nikoliv.

To je takovy problem se podivat do inzeratu? Scala neni zdaleka takova masovka jako trebas Java, ale misto se najde bez problemu. Pokud zuzis sve pozadavky na "zajimava prace", tak se ten pomer navic dost zlepsi...

Pro mě jsou zajímavé zakázky. Nikdo z našich klientů (podniková sféra) takové obskurnosti nepoptává.

Jinymi slovy - generalizujes sve zkusenosti s patlanim v jedne oblasti na cely obor.