Kind Demotion

[Ashley Yakeley]

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 at haskell.org
>> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users