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
_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
