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
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
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
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 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
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 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 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
participants (2)
-
Ashley Yakeley -
Richard Eisenberg