| Where is Proxy data type defined? In the section "The new Typeable class" of http://hackage.haskell.org/trac/ghc/wiki/GhcKinds/PolyTypeable | Which instances should it have? Well, Typeable, perhaps! But that is no so relevant here. S

On Fri, Feb 10, 2012 at 2:24 PM, Ian Lynagh wrote:

But it would be better if they could use the new definition. Is PolyKinds sufficiently well-defined and simple that it is feasible for other Haskell implementations to implement it?

From the users perspective, the Proxy will behave the same as ghcs,

There is actually a much simpler extension I have in jhc called 'existential kinds' that can express this. Existential kinds grew from the need to express the kind of the function type constructcor data (->) :: * -> * -> * is fine for haskell 98, but breaks when you have unboxed values, so jhc used the same solution of ghc, making it data (->) :: ?? -> ? -> * where ?? means * or #, and ? means *, #, or (#), I will call these quasi-kinds for the moment. all you need to express the typeable class is an additional quasi-kind 'ANY' that means, well, any kind. then you can declare proxy as data Proxy (a :: ANY) = Proxy and it will act identially to the ghc version. So why existential? because ANY is just short for 'exists k. k' so Proxy ends up with Proxy :: (exists k . k) -> * which is isomorphic to forall k . Proxy :: k -> * ? expands to (exists k . FunRet k => k) and ?? expands to (exists k . FunArg k => k) where FunRet and FunArg are appropriate constraints on the type. so the quasi-kinds are not any sort of magic hackery, just simple synonyms for existential kinds. The implemention is dead simple for any unification based kind checker, normally when you find a constructor application, you unify each of the arguments kinds with the kinds given by the constructor, the only difference is that if the kind of the constructor is 'ANY' you skip unifying it with anything, or create a fresh kind variable with a constraint if you need to support ?,and ?? too and unify it with that. about a 2 line change to your kind inference code. the only difference is that I need the 'ANY' annotation when declaring the type as such kinds are never automatically infered at the moment. I may just support the 'exists k . k' syntax directly in kind annotations actually eventually, I support it for types and it is handy on occasion. John

On 11 February 2012 00:30, John Meacham wrote:

Would it be useful to make 'Proxy' an unboxed type itself? so

Proxy :: forall k . k -> #

This would statically ensure that no one accidentally passes ⊥ as a parameter or will get anything other than the unit 'Proxy' when trying to evaluate it. So the compiler can unconditionally elide the parameter at runtime. Pretty much exactly how State# gets dropped which has almost the same definition.

Or don't use an argument at all: class Typeable t where typeRep :: Tagged t TypeRep newtype Tagged s b = Tagged { unTagged :: b } See: http://hackage.haskell.org/packages/archive/tagged/0.2.3.1/doc/html/Data-Tag... Bas

Hello, I like Bas's variation on the design (except, perhaps, for the name "Tagged" ;) It captures exactly what we are trying to do: the dictionary for Typeable becomes simply the run-time representation of the type. Coincidentally, this is exactly the same as what I am using to link value level numbers/strings to type-level numbers/symbols, on the type-nats branch of GHC. I wonder if it might make sense to unify the two designs? -Iavor PS: I wouldn't worry too much about breaking existing code, as long as derived Typeable instances continue to work---I never provide custom ones and, in fact, I think that GHC should no allow them or, at least, give a stern warning when it sees one. On Fri, Feb 10, 2012 at 4:35 PM, Bas van Dijk wrote:

Or don't use an argument at all:

class Typeable t where  typeRep :: Tagged t TypeRep

newtype Tagged s b = Tagged { unTagged :: b }

On 10/02/2012, at 23:30, John Meacham wrote:

something I have thought about is perhaps a special syntax for Proxy, like {:: Int -> Int } is short for (Proxy :: Proxy (Int -> Int)). not sure whether that is useful enough in practice though, but could be handy if we are throwing around types a lot.

We really need explicit syntax for type application. There are already a lot of cases where we have to work around not having it (e.g., Storable) and with the new extensions, there are going to be more and more of those. Roman

On 12/02/2012, at 01:44, John Meacham wrote:

I am not so sure, adding type applications to the language seems fairly radical and will change many aspects of the language. Something like Proxy that can be expressed in relatively vanilla haskell and some handy desugarings is much more attractive to me.

With type apllications you end up with odd cases you need to figure out, like forall a b. (a,b) and forall b a. (a,b) meaning different things maybe depending on the details of the impementation.... Also, it meshes with a core language based on type applications, like system F or jhc's PTS. However, it seems quite plausible that there are other ways of writing haskell compilers. Not that i am opposed to them, I just think they are way overkill for this situation and any solution based on them will be ghc-bound for a long time probably.

Type application doesn't necessarily have to tied to the forall syntax. You already suggest {:: T} as a shortcut for (Proxy :: Proxy T). Now suppose {T} is a shortcut for the type Proxy T and you could write: class Typeable t where typeRep :: {t} -> TypeRep ... typeRep {::Int} ... But now you don't need Proxy at all, although it's a perfectly valid desugaring. I'm not necessarily suggesting the syntax above, just trying to point out that type application syntax might be bound to a specific type abstraction syntax. Roman

I hate using things like 'new', 'old', 'unsafe' in module names, the words are too overloaded and mean different things in different contexts. you end up with things like 'NewerTypeable'. So why not call it what it is already known by, 'Data.PolyTypeable'. John On Sat, Feb 11, 2012 at 5:05 PM, Roman Leshchinskiy wrote:

On 10/02/2012, at 16:03, Simon Peyton-Jones wrote:

...

Friends

The page describes an improved implementation of the Typeable class, making use of polymorphic kinds. Technically it is straightforward, but it represents a non-backward-compatible change to a widely used library, so we need to make a plan for the transition.

      http://hackage.haskell.org/trac/ghc/wiki/GhcKinds/PolyTypeable

Comments?  You can fix typos or add issues directly in the wiki page, or discuss by email

IMO, polymorphic kinds are far too experimental at this stage to be used in such a fundamental library. I also fully agree with Ian's point about other implementations.

Should there perhaps be a NewTypeable module which could then be renamed into Typeable once it is sufficiently well established?

Roman

_______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

| Should there perhaps be a NewTypeable module which could then be renamed | into Typeable once it is sufficiently well established? I started with that idea, but there would be a 2-stage process: * Step 1: (when PolyTypable becomes available) People change to import Data.PolyTypeable * Step 2: (when PolyTypeable becomes Typeable) People change back to Data.Typeable I was hoping to avoid that. Notice that even if we replace Typeable immediately with the new polymorphic one, doing so has very limited impact: for users who just use "deriving Typeable" and "typeOf", that will work fine with the new thing too. But I'm sure that some "seams" would show through. It's a balance. Simon

Sent from my iPhone On Feb 14, 2012, at 3:00 AM, Roman Leshchinskiy wrote:

On 13/02/2012, at 11:10, Simon Peyton-Jones wrote:

...

| Should there perhaps be a NewTypeable module which could then be renamed | into Typeable once it is sufficiently well established?

I started with that idea, but there would be a 2-stage process: * Step 1: (when PolyTypable becomes available) People change to import Data.PolyTypeable * Step 2: (when PolyTypeable becomes Typeable) People change back to Data.Typeable

The problem is that libraries generally have to support multiple versions of GHC and this would become harder. But that isn't too bad, preprocessor magic solves it. It would be easier if we could define Typeable1 etc. as an alias for Typeable (since they now mean the same thing) but we don't have class aliases.

No, but we do have the ability to make type aliases for classes now that we have constraint kinds, and typeOf1, etc. are amenable to the same implementation technique as typeOf.

My main objection is still the fact that a central library will now rely on a highly experimental language feature which isn't even really available in a GHC release yet (my understanding is that support for polykinds in 7.4 is shaky at best). IMO, this should be avoided as a matter of policy. I realise that others are much less conservative than me in this respect, though.

Roman

_______________________________________________ Libraries mailing list Libraries@haskell.org http://www.haskell.org/mailman/listinfo/libraries

You could probably get away with something like data Proxy = Proxy a class Typeable a where typeOfProxy :: Proxy a -> TypeRep typeOf :: forall a. Typeable a => a -> TypeRep typeOf = typeOfProxy (Proxy :: Proxy a) which being outside of the class won't contribute to the inference of 'a's kind. This would let you retain the existing functionality. On Mon, Feb 13, 2012 at 8:33 AM, Simon Marlow wrote:

On 10/02/2012 16:03, Simon Peyton-Jones wrote:

...

Friends

The page describes an improved implementation of the Typeable class, making use of polymorphic kinds. Technically it is straightforward, but it represents a non-backward-compatible change to a widely used library, so we need to make a plan for the transition.

http://hackage.haskell.org/**trac/ghc/wiki/GhcKinds/**PolyTypeablehttp://hackage.haskell.org/trac/ghc/wiki/GhcKinds/PolyTypeable

Comments? You can fix typos or add issues directly in the wiki page, or discuss by email

I've no objections to the plan itself, except that typeOf itself seems useful, so is there any need to deprecate it?

Cheers,

Simon

______________________________**_________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.**org http://www.haskell.org/**mailman/listinfo/glasgow-**haskell-usershttp://www.haskell.org/mailman/listinfo/glasgow-haskell-users

On Mon, Feb 13, 2012 at 3:27 PM, Simon Marlow wrote:

On 13/02/12 18:16, Edward Kmett wrote:

...

You could probably get away with something like

data Proxy = Proxy a

class Typeable a where typeOfProxy :: Proxy a -> TypeRep

typeOf :: forall a. Typeable a => a -> TypeRep typeOf = typeOfProxy (Proxy :: Proxy a)

which being outside of the class won't contribute to the inference of 'a's kind.

This would let you retain the existing functionality.

Simon's version has this:

typeOf :: forall a. Typeable a => a -> TypeRep typeOf x = typeRep (getType x) where getType :: a -> Proxy a getType _ = Proxy

(your version is clearer, though)

I'm assuming there's no significance behind your renaming of 'typeRep' to 'typeOfProxy'?

No significance at all. I probably should have read the page before commenting. ;) -Edward