Má Haskell budoucnost?

[Wichser]

No a kind Fix je:

Kód: [Vybrat]

Fix :: (* -> *) -> *což je HKT i bez typeclassy....

Jistě, ale když se v signatuře vyskytne Fix f, tak to už HKT není, protože aplikace.

[Reklama]

[andy]

No a kind Fix je:

Kód: [Vybrat]

Fix :: (* -> *) -> *což je HKT i bez typeclassy....

Jistě, ale když se v signatuře vyskytne Fix f, tak to už HKT není, protože aplikace.

Otázka byla na praktické použití. Tohle není praktické použití?

V signatuře to být nemůže, protože funkce v haskellu jaksi očekávají parametr typu Type... takže v rámci haskellu tu otázku nechápu. Možná v jiných jazycích typu Agda je to možné jinak, ale tu jsem se naučit ještě nestihl (fakt to tam jde?)

[Wichser]

V signatuře to být nemůže, protože funkce v haskellu jaksi očekávají parametr typu Type... takže v rámci haskellu tu otázku nechápu. Možná v jiných jazycích typu Agda je to možné jinak, ale tu jsem se naučit ještě nestihl (fakt to tam jde?)

Jistěže to jde. Tam jde věcí... A taky to jde třeba v C++.

[andy]

V signatuře to být nemůže, protože funkce v haskellu jaksi očekávají parametr typu Type... takže v rámci haskellu tu otázku nechápu. Možná v jiných jazycích typu Agda je to možné jinak, ale tu jsem se naučit ještě nestihl (fakt to tam jde?)

Jistěže to jde. Tam jde věcí... A taky to jde třeba v C++.

No trošku to na mě dělá dojem, že si tu někdo honí ego...

Ale otázka byla na praktické použití - chceš říct, že použití "Fix f" není "praktické použití", protože to je plně aplikované..?

[JSH]

Introspekci C++ umí. Akorát se tomu tam říká RTTI.

Co jsem pochopil, tak RTTI akorát umí dotaz "je tohle typu X"? (což zrovna haskell bez typeclassy neumí...) Nebo umí i něco typu "co je v téhle třídě", takže se to dá použít třeba na nějakou automatickou JSON serializaci? (já fakt nevím)

Tohle znám pod pojmem "introspekce". Věci typu "Co je v téhle třídě?" znám pod pojmem "reflexe". Reflexi C++ neumí, ale momentálně se na statické reflexi intenzivně pracuje. Jestli se to stihne do c++20 je ve hvězdách.

[Reklama]

[Wichser]

chceš říct, že použití "Fix f" není "praktické použití", protože to je plně aplikované..?

Může být praktické, jen to není HKT.

[andy]

chceš říct, že použití "Fix f" není "praktické použití", protože to je plně aplikované..?

Může být praktické, jen to není HKT.

Fix není HKT?

[andy]

Kde se v praxi kromě typových tříd používají HKT?

Příklad:

Kód: [Vybrat]

cata :: Functor f => (f a -> a) -> Fix f -> a)Je použit Fix. Fix je HKT. Použití v praxi v katamorfismu. Odpovídá to na otázku?

[andy]

Nebo ještě jednou - jinak. HKT je typ, který bere jako parametr typový konstruktor a něco z toho vyrobí. Takže třeba:

Kód: [Vybrat]

Functor :: (* -> *) -> Constraint
Fix :: (* -> *) -> *
Samozřejmě, že v kódu se to následně aplikuje celé - a konkrétně třeba u toho "Fix f" to "f" aplikované není. Ale to jaksi neznamená, že ten HKT typ "nebyl použit". Jinak IMO ty neaplikované typy nejde použít jako parametry funkcí, a tak nějak bych si dost tipnul, že to nejde v Agdě a není mi moc jasné, jak by to mohlo jít v C++. Ten typ nemá žádnou hodnotu a funkce berou hodnoty. Ale když tak suverénně píšeš, že to jde, tak se rád poučím - dáš příklady?

[Wichser]

Jinak IMO ty neaplikované typy nejde použít jako parametry funkcí, a tak nějak bych si dost tipnul, že to nejde v Agdě a není mi moc jasné, jak by to mohlo jít v C++. Ten typ nemá žádnou hodnotu a funkce berou hodnoty.

Strašně to motáš, než si ujasníš terminologii, nikam se nedostanem. "Neaplikované" typy samozřejmě jdou použít jako parametry funkcí (nově i v Haskellu, když se použije příslušný jazykový přepínač). Ale díky za podnět, teď mám po nějaké době zase důvod hrát si s Haskellem a zkoušet v něm věci, které doposud šly jen v silnějších typových systémech.

[andy]

Jinak IMO ty neaplikované typy nejde použít jako parametry funkcí, a tak nějak bych si dost tipnul, že to nejde v Agdě a není mi moc jasné, jak by to mohlo jít v C++. Ten typ nemá žádnou hodnotu a funkce berou hodnoty.

Strašně to motáš, než si ujasníš terminologii, nikam se nedostanem. "Neaplikované" typy samozřejmě jdou použít jako parametry funkcí (nově i v Haskellu, když se použije příslušný jazykový přepínač). Ale díky za podnět, teď mám po nějaké době zase důvod hrát si s Haskellem a zkoušet v něm věci, které doposud šly jen v silnějších typových systémech.

Ta funkce "cata" jde samozřejmě zavolat s TypeApplications, ale vůbec netuším, co to má společného s HKT. Ale v pohodě - tak mi to ujasni. Rád se poučím.

[Wichser]

tak mi to ujasni. Rád se poučím.

Jde o tvé použití termínu "parametr funkce", to je přece ta "hodnota", kdežto v signatuře je (meta)typ. A parametrem funkce může být klidně třeba ten Fix (nejen v Agdě, i v Haskellu). Ten příslušný přepínač je KindSignatures.

[andy]

tak mi to ujasni. Rád se poučím.

Jde o tvé použití termínu "parametr funkce", to je přece ta "hodnota", kdežto v signatuře je (meta)typ. A parametrem funkce může být klidně třeba ten Fix (nejen v Agdě, i v Haskellu). Ten příslušný přepínač je KindSignatures.

Šel by příklad? Neumím si to představit. (fakt)

[Wichser]

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

[andy]

Š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...?