I'm going to phrase this as a challenge, because I think that's likely to get the best response: I just released a package, th-kindshttp://hackage.haskell.org/package/th-kinds, which attempts to automatically infer the kind of a specified type, type constructor, type family, type class, or pretty much anything else that has a kind. This package was developed in response to a sort-of challenge from Brent Yorgey on #haskell to create this functionality. So, uh, I stayed up last night until 5 am learning unification algorithms and implementing this...heh. It rolls its own kind inference, so I don't know if it's adequately powerful to handle all the wacky types you can construct. Things I have tested it on: - IO and ST - Many primitive types, including unboxed tuples and State# - mtl - newtype Fix f = Fix (f (Fix f)) - data Tree a = Leaf a | Bin (Tree a) (Tree a) - data Foo a b = a (tests proper defaulting behavior) - A type family from my old TrieMap package with kind -- I kid you not -- ((* -> *) -> ((* -> *) -> * -> *) -> (* -> *) -> * -> * -> *) Things that it will not work on, and that I don't think will change: - GADT types that cannot be reified by TH. Essentially, I think this is "the set of GADT data types that actually couldn't be implemented without GADTs." Not sure, though. In any event, at the moment, I don't think there's any hope of handling GADTs in TH at this point, so I don't really object to this problem. Anyway, y'all should attempt to break th-kinds. Tell me if you can construct a type for which my inference checker breaks, but not because you get an error message saying "Can't reify a GADT data constructor..." By the way, I'd like to bump thesehttp://hackage.haskell.org/trac/ghc/ticket/3916 tickets http://hackage.haskell.org/trac/ghc/ticket/3920. They're certainly related, but I'm not sure if they're genuinely equivalent. It's really irritating, though, that kind parsing is so broken in TH, and I think that a TH backend guru should be able to figure out where there's a foldr instead of a foldl... th-kinds includes a workaround to this bug, but if the bug is fixed, it'll break again. Yuck, bugs. Louis Wasserman wasserman.louis@gmail.com http://profiles.google.com/wasserman.louis
On Mon, Mar 15, 2010 at 07:31:12PM -0500, Louis Wasserman wrote:
I'm going to phrase this as a challenge, because I think that's likely to get the best response:
I just released a package, th-kindshttp://hackage.haskell.org/package/th-kinds, which attempts to automatically infer the kind of a specified type, type constructor, type family, type class, or pretty much anything else that has a kind.
This package was developed in response to a sort-of challenge from Brent Yorgey on #haskell to create this functionality. So, uh, I stayed up last night until 5 am learning unification algorithms and implementing this...heh.
Ironically, after issuing this challenge I later realized that I can actually get away without it for now. =) But it's still pretty cool -- and I may actually end up wanting it later if I continue to extend my library -- and I'll try testing it out soon. -Brent
On Mon, Mar 15, 2010 at 5:31 PM, Louis Wasserman
GADT types that cannot be reified by TH. Essentially, I think this is "the set of GADT data types that actually couldn't be implemented without GADTs." Not sure, though. In any event, at the moment, I don't think there's any hope of handling GADTs in TH at this point, so I don't really object to this problem.
Actually, with existential types and type equality constraints, GADTs are redundant. Here's a couple examples: data GEqType a b where GRefl :: EqTypeGADT a a data DEqType a b = (a ~ b) => DRefl data Expr t where Lam :: (Expr a -> Expr b) -> Expr (a -> b) App :: Expr (a->b) -> Expr a -> Expr b Prim :: Show a => a -> Expr a Gt :: Expr Int -> Expr Int -> Expr Bool data DExpr t = forall a b. (t ~ (a -> b)) => DLam (DExpr a -> DExpr b) | forall a. DApp (DExpr (a -> t)) (DExpr a) | Show t => DPrim t | (t ~ Bool) => Gt (DExpr Int) (DExpr Int) The algorithm is pretty simple: - existentially quantify over all type variables mentioned in the GADT constructor - add a type equality constraint to match the result type - (optional) simplify -- ryan
Actually, with existential types and type equality constraints, GADTs are redundant.
The algorithm is pretty simple: - existentially quantify over all type variables mentioned in the GADT constructor - add a type equality constraint to match the result type - (optional) simplify
While true, this nevertheless doesn't let me perform
unify ''MyGADTType
when MyGADTType was defined with GADT syntax in the first place. GADT handling for TH is, for the moment, Somebody Else's Problem, and not something I'm going to be able to deal with without hacking on TH itself. Louis
Louis Wasserman wrote:
I just released a package, th-kinds, which attempts to automatically infer the kind of a specified type, type constructor, type family, type class, or pretty much anything else that has a kind... It rolls its own kind inference...
Interesting. The "right" way to do this would be to use the GHC API. (Actually - can you read kind information from the GHC API? I'm not sure.) That would guarantee that your program and the compiler will agree about kind inference. So I view this package as similar to the "haskell-src-exts" package: a lightweight alternative to the GHC API for a certain task, where you are willing to sacrifice the 100% guarantee of compiler compatibility. Of course, we hope that the package will in fact be completely compatible with the both the compiler and the Report. And like "haskell-src-exts", ongoing testing and debugging of compatibility could have the additional benefit of improving both compiler and the Report. :) Regards, Yitz
participants (4)
-
Brent Yorgey -
Louis Wasserman -
Ryan Ingram -
Yitzchak Gale