TypeRep does indeed resemble * as a type. I'm working on a system for reification of types, building on my open-witness package (which is essentially a cleaner, more Haskell-ish alternative to TypeRep). Firstly, there's a witness type to equality of types: data EqualType :: k -> k -> * where MkEqualType :: EqualType a a Then there's a class for matching witnesses to types: class SimpleWitness (w :: k -> *) where matchWitness :: w a -> w b -> Maybe (EqualType a b) Then I have a type IOWitness that witnesses to types. Through a little Template Haskell magic, one can declare unique values of IOWitness at top level, or just create them in the IO monad. Internally, it's just a wrapper around Integer, but if the integers match, then it must have come from the same creation, which means the types are the same. data IOWitness (a :: k) = ... instance SimpleWitness IOWitness where ... OK. So what I want to do is create a type that's an instance of SimpleWitness that represents types constructed from other types. For instance, "[Integer]" is constructed from "[]" and "Integer". data T :: k -> * where DeclaredT :: forall ka (a :: ka). IOWitness a -> T a ConstructedT :: forall kfa ka (f :: ka -> kfa) (a :: ka). T f -> T a -> T (f a) instance SimpleWitness T where matchWitness (DeclaredT io1) (DeclaredT io2) = matchWitness io1 io2 matchWitness (ConstructedT f1 a1) (ConstructedT f2 a2) = do MkEqualType <- matchWitness f1 f2 MkEqualType <- matchWitness a1 a2 return MkEqualType matchWitness _ _ = Nothing But this doesn't work. This is because when trying to determine whether "f1 a1 ~ f2 a1", even though "f1 a1" has the same kind as "f2 a2", that doesn't mean that "a1" and "a2" have the same kind. To solve this, I need to include in "ConstructedT" a witness to "ka", the kind of "a": ConstructedT :: forall kfa ka (f :: ka -> kfa) (a :: ka). IOWitness ka -> T f -> T a -> T (f a) matchWitness (ConstructedT k1 f1 a1) (ConstructedT k2 f2 a2) = do MkEqualType <- matchWitness k1 k2 MkEqualType <- matchWitness f1 f2 MkEqualType <- matchWitness a1 a2 return MkEqualType Sadly, this doesn't work, for two reasons. Firstly, there isn't a type for *, etc. Secondly, GHC isn't smart enough to unify two kinds even though you've given it an explicit witness to their equality. -- Ashley Yakeley On 16/09/12 20:12, Richard Eisenberg wrote:
If you squint at it the right way, TypeRep looks like such a type *. I believe José Pedro Magalhães is working on a revision to the definition of TypeRep incorporating kind polymorphism, etc., but the current TypeRep might work for you.
Your idea intersects various others I've been thinking about/working on. What's the context/application?
Thanks, Richard
On Sep 16, 2012, at 7:09 PM, Ashley Yakeley wrote:
Now that we have type promotion, where certain types can become kinds, I find myself wanting kind demotion, where kinds are also types. So for instance there would be a '*' type, and all types of kind * would be demoted to values of it. Is that feasible?
-- Ashley Yakeley
_______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users