Opened 5 years ago

Closed 5 years ago

Last modified 5 years ago

#9568 closed feature request (wontfix)

Type classes that fully cover closed kinds

Reported by: dmcclean Owned by:
Priority: lowest Milestone:
Component: Compiler (Type checker) Version: 7.8.3
Keywords: Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

When we have a closed kind (I think data kinds may be the only ones that are closed?), and a type class that takes only that kind as a parameter, and we have instances of the typeclass for every type in the kind, it would be nice if we didn't have to list it in the context of every function that uses it.

Example:

in GHC.TypeLits, this relationship exists between Nat and KnownNat, Symbol and KnownSymbol.

It also arises in many of my uses of data kinds, because I often end up with a KnownX class that provides term-level things related to whatever the type is.

The constraints tend to end up everywhere, which is noisy. As far as I can tell they don't really carry any information: a KnownNat n constraint where n :: Nat should be able to be discharged in the same way that something like Show Bool is, because regardless of which n we pick we know there will be an instance.

(This is trickier for closed kinds like Nat and Symbol than for user-defined ones through the data kinds feature, because the former are inhabited by infinitely many types.)

Perhaps we could have a pragma to inform the compiler that this situation exists for a certain typeclass, which the compiler could check in finite cases (like the ones arising for user-defined data kinds) by enumerating all the cases.

Change History (6)

comment:1 Changed 5 years ago by rwbarton

This is a natural thing to want but, alas, it's not so simple. It's not enough for the compiler to know that some instance exists. It has to know which instance to use, because the choice of instance affects the runtime semantics of the program.

From a theory point of view, polymorphism over closed kinds has the same parametricity properties as polymorphism over open kinds like *. If I have a function f :: forall (b :: Bool). Proxy b -> String then f's behavior cannot depend on the choice of b, so f (Proxy :: Proxy False) must be equal to f (Proxy :: Proxy True), just like a function g :: Maybe a -> String must satisfy g (Nothing :: Maybe Int) = g (Nothing :: Maybe Bool).

From an implementation point of view there is no difference at all at runtime between Proxy :: Proxy False and Proxy :: Proxy True, so simply for that reason it's impossible for any function to distinguish them.

But with a class constraint C b, even when C has instances for both False and True, f's behavior can depend on b, as I'm sure you know. This is possible because the C b constraint gets translated to an extra value-level argument to the function. So, f :: forall (b :: Bool). C b => Proxy b -> String is really different from f :: forall (b :: Bool). Proxy b -> String even when C b is satisfied for each individual type b :: Bool.

In light of all this, I'm not sure what change along the lines of your suggestion would be possible. IIRC Richard Eisenberg's "dependent Haskell" project includes a non-parametric universal quantifier; perhaps that is related.

comment:2 Changed 5 years ago by goldfire

I agree fully with Reid (rwbarton). Those "class constraints" are really, under the hood, implicit parameters (dictionaries) passed around at runtime. Given that they have runtime significance, I don't think it's a good idea to hide them from the programmer.

On the relationship to Pi-types: As described in this video and this wiki page, I'm working on a version of GHC that allows a type parameter to be made available at runtime. This feature could be used to simulate dictionary passing (I believe), by examining the type parameter at runtime and making decisions based on it. So, I guess this might improve the syntax a bit -- hard to say for sure at this point.

comment:3 Changed 5 years ago by dmcclean

Great point. Not sure what I was thinking, sorry.

Regarding "If I have a function f :: forall (b :: Bool). Proxy b -> String then f's behavior cannot depend on the choice of b", I think I got off track by thinking that the binding happens in two stages, and that when type type-level lambda was applied it could "pick" which term-level function it wanted to return after inspecting the type argument, and that all of that always happened at compile time. But it doesn't.

comment:4 Changed 5 years ago by Herbert Valerio Riedel <hvr@…>

removed commit with wrong ticket reference

Last edited 5 years ago by hvr (previous) (diff)

comment:5 Changed 5 years ago by Herbert Valerio Riedel <hvr@…>

removed commit with wrong ticket reference

Last edited 5 years ago by hvr (previous) (diff)

comment:6 Changed 5 years ago by goldfire

Resolution: wontfix
Status: newclosed

I'm assuming that those two recent commits reference this ticket in error.

And, it seems that the original poster agrees that the requested feature is invalid, so I'm closing this ticket.

Note: See TracTickets for help on using tickets.