Má Haskell budoucnost?

Wichser

Re:Má Haskell budoucnost?
« Odpověď #510 kdy: 19. 09. 2018, 12:32:18 »
Šel by příklad? Neumím si to představit. (fakt)
Nejjednodušší, co mě napadá:
Kód: [Vybrat]
FApp : (Type -> Type) -> Type -> Type
FApp f a = f a
Pak můžu volat např. FApp List Int.
No... a jaký je teda rozdíl od:
Kód: [Vybrat]
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}

newtype FApp :: (* -> *) -> * -> * where
  FApp :: f l -> FApp f l
Resp. to, co tady celou dobu ukazuju:
Kód: [Vybrat]
newtype Fix :: (* -> *) -> * where
  Fix :: f (Fix f) -> Fix f
Což je jenom rozepsaná ta původní definice?

Teda kromě toho, že haskell nemá dependent types, tak se to holt píše takhle...?
Hele, tys tvrdil, že parametrem funkce nemůže být funktor. Dal jsem ti příklad, cos chtěl. Proč pořád uhýbáš?


andy

Re:Má Haskell budoucnost?
« Odpověď #511 kdy: 19. 09. 2018, 13:42:34 »
Šel by příklad? Neumím si to představit. (fakt)
Nejjednodušší, co mě napadá:
Kód: [Vybrat]
FApp : (Type -> Type) -> Type -> Type
FApp f a = f a
Pak můžu volat např. FApp List Int.
No... a jaký je teda rozdíl od:
Kód: [Vybrat]
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}

newtype FApp :: (* -> *) -> * -> * where
  FApp :: f l -> FApp f l
Resp. to, co tady celou dobu ukazuju:
Kód: [Vybrat]
newtype Fix :: (* -> *) -> * where
  Fix :: f (Fix f) -> Fix f
Což je jenom rozepsaná ta původní definice?

Teda kromě toho, že haskell nemá dependent types, tak se to holt píše takhle...?
Tys tvrdil, že parametrem funkce nemůže být funktor. Dal jsem ti příklad, cos chtěl. Proč pořád uhýbáš?
V čem uhýbám? Funkce v Haskellu nemůže dostat Type jako parametr, v Agdě jsou typy first class. OK, díky za informaci, někdy se na to podívám víc.

Nicméně v Haskellu můžeš psát funkce, které akceptují typy jako parametr, akorát se to nenazývá funkce. No a tady jsem ti dal ukázku toho, že to

1) jde taky
2) Fix je příkladem takové funkce

No a ty jsi tvrdil, že cata (s Fix) není příkladem praktického užití HKT (mimo typeclassy). A mně připadá, že podle toho, co píšeš, je. Takže bys mi mohl vysvětlit, proč FApp v tvém příkladu by byl ukázkou HKT, zatímco FApp v haskellu nikoliv, případně proč je Fix něco úplně jiného. Protože mně to přijde jako dost stejné.

Wichser

Re:Má Haskell budoucnost?
« Odpověď #512 kdy: 19. 09. 2018, 13:48:15 »
Funkce v Haskellu nemůže dostat Type jako parametr, v Agdě jsou typy first class
...
Nicméně v Haskellu můžeš psát funkce, které akceptují typy jako parametr
Koukám, že tu terminologii motáš i po explicitním vysvětlení. BTW v Haskellu jde napsat funkce typu Type->Type například.

andy

Re:Má Haskell budoucnost?
« Odpověď #513 kdy: 19. 09. 2018, 13:53:54 »
Funkce v Haskellu nemůže dostat Type jako parametr, v Agdě jsou typy first class
...
Nicméně v Haskellu můžeš psát funkce, které akceptují typy jako parametr
Koukám, že tu terminologii motáš i po explicitním vysvětlení. BTW v Haskellu jde napsat funkce typu Type->Type například.
No třeba takhle:
Kód: [Vybrat]
newtype Id f = Id fAle dobře - dáš mi tvůj příklad?

Wichser

Re:Má Haskell budoucnost?
« Odpověď #514 kdy: 19. 09. 2018, 14:06:22 »
Ale dobře - dáš mi tvůj příklad?
Na úrovni typů: 
Kód: [Vybrat]
Add 'Zero n = n
Add ('Succ n) m = Add n ('Succ m)


andy

Re:Má Haskell budoucnost?
« Odpověď #515 kdy: 19. 09. 2018, 14:56:00 »
Ale dobře - dáš mi tvůj příklad?
Na úrovni typů: 
Kód: [Vybrat]
Add 'Zero n = n
Add ('Succ n) m = Add n ('Succ m)
Closed type family? Nebo obecně type families. Jasně. A použití by bylo například:

Kód: [Vybrat]
f :: Neco x -> Neco (Add x 1)
A jak se to liší od:
Kód: [Vybrat]
cata :: Functor f => (f a -> a) -> Fix f -> aProtože já bych řekl, že "Fix" je v tomhle prostě zavolání typové funkce (akorát to přes type families nejde udělat). Nebo se mýlím?

Tvrdil jsi, že použití Fix v cata není příkladem použití HKT. A to, co teď dáváš jako příklady, je tomu ekvivalentní - definice FApp přes newtype a ta Agdová dělají v podstatě to samé. Tak v čem se to teda liší? Připadá mi, že nějak...uhýbáš...?

jouda

Re:Má Haskell budoucnost?
« Odpověď #516 kdy: 23. 09. 2018, 22:23:46 »
BTW když to tak sleduju, vrtá mi hlavou jedna otázka na Haskelisty (a nemímím to nijak zle, žádný flame, fakt jen zvědavost)

Že je Haskell založený k obrazu CT je notoricky známý fakt. Ale vrtá mi v hlavě otázka, jestli CT pro něj funguje primárně jako design vzor, nebo jestli i nějakým netriviálním způsobem využívá "něco" (teorém, ... ) co by se bez CT odvozovalo jinak mnohem složitěji.
ufff snad je to aspoň trochu srozumitelné :)

Bacsa

Re:Má Haskell budoucnost?
« Odpověď #517 kdy: 23. 09. 2018, 22:49:25 »
BTW když to tak sleduju, vrtá mi hlavou jedna otázka na Haskelisty (a nemímím to nijak zle, žádný flame, fakt jen zvědavost)

Že je Haskell založený k obrazu CT je notoricky známý fakt. Ale vrtá mi v hlavě otázka, jestli CT pro něj funguje primárně jako design vzor, nebo jestli i nějakým netriviálním způsobem využívá "něco" (teorém, ... ) co by se bez CT odvozovalo jinak mnohem složitěji.
ufff snad je to aspoň trochu srozumitelné :)
Využívá terminologii, formální výsledky moc využívat nemůže, protože “kategorie typů” ani není kategorie podle definice v KT.

JS

Re:Má Haskell budoucnost?
« Odpověď #518 kdy: 24. 09. 2018, 13:10:15 »
jestli CT pro něj funguje primárně jako design vzor, nebo jestli i nějakým netriviálním způsobem využívá "něco" (teorém, ... ) co by se bez CT odvozovalo jinak mnohem složitěji.

K vyse uvedene odpovedi bych dodal..

Haskell je spis postaveny na teorii typoveho lambda kalkulu (konkretne https://en.wikipedia.org/wiki/System_F) nez na CT.

Nicmene, z toho malo co o CT vim, tak je obecne jen malo vysledku v CT ktere by se mimo CT dokazovaly obtizne. Hlavni smysl CT vidim v tom, ze je to jakysi "makro system" pro matematiku - muzeme stejny dukaz nechat provest pro mnoho ruznych objektu, a tim si usetrime praci. Ale samo o sobe ty dukazy nejsou magicky elegantnejsi nez by byly v kazde te jednotlive teorii.

Dusledek je, ze hodne konceptu CT se pak v Haskellu objevi jako typove tridy. Zase, jejich smyslem neni primarne poskytnout lepsi algoritmus, ale zbytecne se neopakovat.

Wichser

Re:Má Haskell budoucnost?
« Odpověď #519 kdy: 24. 09. 2018, 16:14:41 »
objevi jako typove tridy. Zase, jejich smyslem neni primarne poskytnout lepsi algoritmus, ale zbytecne se neopakovat.
Pak je otázka, proč jsou v mainstreamu jen v C++, Swiftu a Ocamlu, neopakování se by mělo ležet na srdci hlavně lepičům v boilerplate jazycích jako Java.

JS

Re:Má Haskell budoucnost?
« Odpověď #520 kdy: 24. 09. 2018, 16:47:51 »
objevi jako typove tridy. Zase, jejich smyslem neni primarne poskytnout lepsi algoritmus, ale zbytecne se neopakovat.
Pak je otázka, proč jsou v mainstreamu jen v C++, Swiftu a Ocamlu, neopakování se by mělo ležet na srdci hlavně lepičům v boilerplate jazycích jako Java.

Protoze skoro nikdo aplikace CT v programovani nezna a tak to nikomu moc nechybi. Haskell ma nektere koncepty z CT ve standardni knihovne, a i tam to nebylo uplne spravne (Monad dlouho nebyla podtridou Applicative).

Swift a OCaml zase takovy mainstream nejsou, a v C++ taky nejsou ve standardni knihovne. Takze..

Jinak Java odjakziva resila boilerplate pomoci generovani kodu prostrednictvim IDE, coz je asi ze vsech moznych ta nejhorsi metoda.

Wichser

Re:Má Haskell budoucnost?
« Odpověď #521 kdy: 24. 09. 2018, 17:25:30 »
objevi jako typove tridy. Zase, jejich smyslem neni primarne poskytnout lepsi algoritmus, ale zbytecne se neopakovat.
Pak je otázka, proč jsou v mainstreamu jen v C++, Swiftu a Ocamlu, neopakování se by mělo ležet na srdci hlavně lepičům v boilerplate jazycích jako Java.

Protoze skoro nikdo aplikace CT v programovani nezna a tak to nikomu moc nechybi. Haskell ma nektere koncepty z CT ve standardni knihovne, a i tam to nebylo uplne spravne (Monad dlouho nebyla podtridou Applicative).

Swift a OCaml zase takovy mainstream nejsou, a v C++ taky nejsou ve standardni knihovne. Takze..

Jinak Java odjakziva resila boilerplate pomoci generovani kodu prostrednictvim IDE, coz je asi ze vsech moznych ta nejhorsi metoda.
Stačily by jen ty typové třídy, CT vzal čert, ta s nimi nesouvisí.