Ashley Yakeley | 17 Sep 01:09 2012

Kind Demotion

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
Richard Eisenberg | 17 Sep 05:12 2012

Re: Kind Demotion

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
Ashley Yakeley | 17 Sep 06:41 2012

Re: Kind Demotion

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
(Continue reading)

Richard Eisenberg | 17 Sep 15:05 2012

Re: Kind Demotion

I see what you're getting at, but the problem is more fundamental than just the lack of a type *. GHC has no
notion of equality between kinds other than syntactic identity. If two kinds are other than
syntactically identical, they are considered distinct. This fact basically renders your approach
doomed to failure. Furthermore, a promoted datatype and the unpromoted datatype are distinct entities
with the same names, so you can't just use a variable both at the kind level and the type level (variable ka in
your final ConstructedT example). It is not hard to write a Demote type family that computes an unpromoted
datatype from its promoted kind, but that type family will interfere with type inference.

That's all the bad news. The good news is that some of us are working out how to extend GHC's rich notion of type
equality to the kind level, which would also allow intermingling of type- and kind-variables. We're
still a little ways out from starting to think about implementing these ideas, but there's a good chance
that what you want will be possible in the (not-so-terribly-long-term) future.

Richard

On Sep 17, 2012, at 12:41 AM, Ashley Yakeley wrote:

> 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
(Continue reading)

Ashley Yakeley | 18 Sep 06:17 2012

Re: Kind Demotion

My workaround is to wrap types of all kinds as kind *:

   data WrapType (a :: k)

...or better yet, as its own kind:

   data WrappedType = forall a. WrapType a

Now I can make an apples-to-apples comparison of types of different 
kinds, e.g. "WrapType []" and "WrapType Bool". All I need now is a way 
of applying wrapped types:

   type family WrapApply
     (f :: WrappedType) (x :: WrappedType) :: WrappedType
   type instance WrapApply
     (WrapType (f :: ka -> kfa)) (WrapType (a :: ka)) = WrapType (f a)

-- Ashley Yakeley

On 17/09/12 06:05, Richard Eisenberg wrote:
> I see what you're getting at, but the problem is more fundamental than just the lack of a type *. GHC has no
notion of equality between kinds other than syntactic identity. If two kinds are other than
syntactically identical, they are considered distinct. This fact basically renders your approach
doomed to failure. Furthermore, a promoted datatype and the unpromoted datatype are distinct entities
with the same names, so you can't just use a variable both at the kind level and the type level (variable ka in
your final ConstructedT example). It is not hard to write a Demote type family that computes an unpromoted
datatype from its promoted kind, but that type family will interfere with type inference.
>
> That's all the bad news. The good news is that some of us are working out how to extend GHC's rich notion of
type equality to the kind level, which would also allow intermingling of type- and kind-variables. We're
(Continue reading)


Gmane