Šel by příklad? Neumím si to představit. (fakt)
Nejjednodušší, co mě napadá:
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:
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
newtype FApp :: (* -> *) -> * -> * where
FApp :: f l -> FApp f l
Resp. to, co tady celou dobu ukazuju:
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é.
521 Odpovědí
99208 Zhlédnutí