Opened 8 years ago

Last modified 21 months ago

#3701 new feature request

allow existential wrapper newtypes

Reported by: duncan Owned by:
Priority: low Milestone:
Component: Compiler (Type checker) Version: 6.10.4
Keywords: Cc: illissius@…, pho@…
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

Consider this OO-style thing, a class Compiler, and a most general instance MkCompiler:

class Compiler c where
  getInstalledPackages :: c -> IO [String]

data GHC = GHC { }
data NHC = NHC { }

ghc :: GHC
ghc = GHC { }

nhc :: NHC
nhc = NHC { }

instance Compiler GHC
instance Compiler NHC

data MkCompiler where
  MkCompiler :: Compiler c => c -> MkCompiler

instance Compiler MkCompiler where
  getInstalledPackages (MkCompiler c) = getInstalledPackages c

compilers :: [MkCompiler]
compilers = [MkCompiler ghc, MkCompiler nhc]

There's two language features we want to make this really nice:

  1. Letting us call the data type Compiler rather than MkCompiler. That would mean separating the class and type namespaces.
  2. Letting us derive the Compiler instance for MkCompiler.

For the latter we would want either:

newtype MkCompiler where
    MkCompiler :: Compiler c => c -> MkCompiler
  deriving Compiler

or

data MkCompiler where
    MkCompiler :: Compiler c => c -> MkCompiler
  deriving Compiler

The advantage of the first is that newtype deriving already exists as a concept so that's nice and consistent. The problem is we do not allow newtypes that use existentials. From an implementation point of view, it's clear that the representations cannot be equal because of the need to store the class dictionary. From a semantic point of view however it's not obvious that existentials with class contexts are illegitimate in newtypes. The underlying implementation would of course have to be an extra layer of boxing, so like data but with the pattern match behaviour newtype.

Change History (15)

comment:1 Changed 8 years ago by simonpj

Yes, something like this would be good. Here's a very relevant paper that Kim Bruce wrote for ECOOP'97: http://www.ifs.uni-linz.ac.at/~ecoop/cd/papers/1241/12410104.pdf. Just as you propose a type and a class with the same name, so does he, but he calls them T and #T.

But it's not that easy to just "derive the instance". In your case:

data MkCompiler where
  MkCompiler :: Compiler c => c -> MkCompiler

instance Compiler MkCompiler where
  getInstalledPackages (MkCompiler c) = getInstalledPackages c

Notice that this instance of getInstalledPackages is necessarily strict. And I think it requires a OO-style type for getInstalledPackages: that is, the first argument has type 'c'. So classes that are amenable are of form

class C a b c where
  op1 :: c -> <blah>
  op2 :: c -> <blah>
  etc

For classes of that form, we could regard (C t1 t2) as a data type, with a single existential constructor, declared (implicitly) thus

data C a b where
  C :: forall a b c. C a b c => c -> C a b

instance C (C a b) where
  op1 (C x) = op1 x
  op2 (C x) = op2 x

It's a little uncomfortable that this stuff only works when the class has the right shaped signature.

Simon

comment:2 Changed 8 years ago by igloo

Milestone: 6.14 branch

comment:3 Changed 7 years ago by igloo

Milestone: 6.14 branch6.14.1

comment:4 Changed 7 years ago by igloo

Milestone: 7.0.17.0.2

comment:5 Changed 7 years ago by igloo

Milestone: 7.0.27.2.1

comment:6 Changed 7 years ago by illissius

Cc: illissius@… added

comment:7 Changed 6 years ago by igloo

Milestone: 7.2.17.4.1

comment:8 Changed 6 years ago by PHO

Cc: pho@… added

comment:9 Changed 6 years ago by igloo

Milestone: 7.4.17.6.1
Priority: normallow

comment:10 Changed 5 years ago by igloo

Milestone: 7.6.17.6.2

comment:11 Changed 3 years ago by thoughtpolice

Milestone: 7.6.27.10.1

Moving to 7.10.1.

comment:12 Changed 3 years ago by thomie

Component: CompilerCompiler (Type checker)
difficulty: Unknown

comment:13 Changed 3 years ago by thoughtpolice

Milestone: 7.10.17.12.1

Moving to 7.12.1 milestone; if you feel this is an error and should be addressed sooner, please move it back to the 7.10.1 milestone.

comment:14 Changed 2 years ago by thoughtpolice

Milestone: 7.12.18.0.1

Milestone renamed

comment:15 Changed 21 months ago by thomie

Milestone: 8.0.1
Note: See TracTickets for help on using tickets.