#11471: Kind polymorphism and unboxed types: bad things are happening -------------------------------------+------------------------------------- Reporter: bgamari | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.10.3 checker) | Keywords: TypeInType, Resolution: | LevityPolymorphism Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by rwbarton): So under comment:7 as I understand it `*` is a synonym for `TYPE L`. We can make a table {{{ 1 :: Int and Int :: * = TYPE L 2# :: Int# and Int# :: TYPE UW64 3.0# :: Double# and Double# :: TYPE UF64 Int :: * and * :: * = TYPE L }}} The last line is given to us by TypeInType. But to me the thing `Int` seems at least as different from the thing `1` as the things `1`, `2#` and `3.0#` are from each other. So, the suggestion is to add another constructor `T` to `RuntimeRep` and replace the last line with {{{ Int :: * and * :: TYPE T }}} We could define a synonym `type Kind = TYPE T` and then `* :: Kind`. The motivation is basically: By merging the type and kind levels, TypeInType means that we no longer ''need'' to distinguish types and kinds. That is great for implementing, say, kind coercions because we don't need to duplicate the language of coercions to the kind level any more. (Feel free to substitute your own, better examples.) However, now that this RuntimeRep story has emerged, it seems we could get the best of both worlds, by defining `* = TYPE L`, and `Kind = TYPE T`. Now we can abstract over the difference between types and kinds when we want to, by working with `TYPE t`. Or we can distinguish between types and kinds when that makes sense, by using `*` and `Kind`. I don't have any great examples for the latter. Maybe if you define a type family whose result is intended to be a kind (since you use it to classify a type elsewhere) you would want to be able to enforce that on clients who may define their own instances. Or maybe the typing rule for a coercion should be that the type `s ~ t` of coercions is well-formed only if `s :: TYPE r` and `t :: TYPE r` for the same `r`, and you don't want to allow coercing between values and types. (But see the end of this comment.) ---- Note that one could perhaps retain even more of the type/kind/sort/etc. hierarchy by adding a parameter to `T`. The parameter `r` would contain information about the representation of the "values" (types) classified by types of kind `TYPE (T r)`. Or in symbols, {{{ if C :: K = TYPE r, (i.e., the type C has representation r) then K :: TYPE (T r), }}} or in short `TYPE r :: TYPE (T r)`. I'm not sure how this would interact with type constructors though (with kinds built from `(->)`). This probably has something to do with the indexed TypeRep story also, which I haven't been paying any attention to. ---- These suggestions apply to an unspecified extension of Haskell that might want to treat the type level in an arbitrary way. If there's a specific plan for "GHC Haskell" to identify types with their TypeReps as mentioned in comment:10 (I guess this means there is some way to refer to a type at the value level, so now it really makes sense to write functions of type `* -> *`, etc.) then there is probably not much reason to take this route, indeed. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11471#comment:13 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler