Levity polymorphic Backpack.
ClosedPublic

Authored by ezyang on Aug 5 2017, 11:38 PM.

Details

Summary

This patch makes it possible to specify non * kinds of
abstract data types in signatures, so you can have
levity polymorphism through Backpack, without the runtime
representation constraint!

Signed-off-by: Edward Z. Yang <ezyang@cs.stanford.edu>

Test Plan

validate

Diff Detail

Repository
rGHC Glasgow Haskell Compiler
Lint
Automatic diff as part of commit; lint not applicable.
Unit
Automatic diff as part of commit; unit tests not applicable.
ezyang created this revision.Aug 5 2017, 11:38 PM

Disclaimer: My brain's version of GHC does not yet have a working implementation of Backpack. Feel free to educate me when I say something stupid.

This looks scary to me. I haven't looked at the code at all, just the example (test case). It's possible for a downstream module to import just a signature with no implementation, right? Can such a module be compiled? Without knowing the representation (implementation) of a levity-polymorphic module signature, this seems impossible. Or do such modules not really get compiled?

Also, do the levity-polymorphism checks work correctly here? For example, I wouldn't be able to compile f x if x :: TYPE Rep (for the Rep) defined in the test case, unless we have an implementing module. Is such a call discovered? (A more specific way to say this: if only a signature with no implementation is in scope, what kind of TyCon is Rep? Only a FamilyTyCon will cause the levity-polymorphism check to trigger.)

ezyang added a comment.Aug 6 2017, 8:52 PM

Can such a module be compiled?

Nope. In Backpack, we always must know the implementation of a signature before it can be compiled. (This will continue to be true even when we implement recursive linking.)

if only a signature with no implementation is in scope, what kind of TyCon is Rep? Only a FamilyTyCon will cause the levity-polymorphism check to trigger.

This I am a bit fuzzy about; all I did was make the Rep abstract, and see if the typechecker complained: it did not. To be honest, I am not sure this feature actually needs the levity polymorphism machinery at all...

all I did was make the Rep abstract,

What does this mean? When you say data Rep in a signature, that presumably produces something of type TyCon in GHC. Which variant of TyCon?

But maybe this doesn't matter, if we *always* have an implementation of a signature. (I guess only signatures can import other signatures without implementations? But I seem to recall the possibility of parameterizing a whole package on signatures' implementations. Do these not get compiled until instantiated with implementations? What processing happens to these parameterized modules before the package is shipped? I'm quite confused about your statement that there is always an implementation. Feel free to point me to the manual for more info if you don't feel like re-explaining!)

ezyang added a comment.Aug 7 2017, 8:58 AM

Oh! Rep is going to be a AlgTyCon, with an AbstractTyCon RHS.

I guess only signatures can import other signatures without implementations?

No, modules can too, but they won't get compiled until you have implementations for signatures.

What processing happens to these parameterized modules before the package is shipped?

I am not sure what you mean by "shipped", but if this means "before implementations for all signatures are available", we *only* typecheck the modules in question, we don't attempt to compile them or do anything else. Everything gets retypechecked again when the actual implementation is available.

Oh! Rep is going to be a AlgTyCon, with an AbstractTyCon RHS.

Ah. So that won't be caught as levity polymorphic. But I'm thinking all will be OK.

What processing happens to these parameterized modules before the package is shipped?

I am not sure what you mean by "shipped", but if this means "before implementations for all signatures are available", we *only* typecheck the modules in question, we don't attempt to compile them or do anything else. Everything gets retypechecked again when the actual implementation is available.

OK. So a hole-y module (module without implementations for all imported signatures) gets typechecked -- but that's it. And then, later, when the implementation is available, it gets typechecked again? That should be OK. The second typecheck will catch any bad levity polymorphism. I'm not sure about the quality of error messages / blame, but I don't think we'll panic.

bgamari added a comment.EditedAug 21 2017, 4:37 PM

What is the status of this? Are you satisfied that this is safe, @goldfire?

compiler/typecheck/TcHsType.hs
1904–1915

What does this type represent? A docstring would be appreciated.

It... seems like I have managed to convince Richard that this patch won't blow things up... so I guess we can merge it :)

If it does blow anything up, I'll find out soon.

I just noticed that there is quite a bit of red in CI. Could you investigate, @ezyang?

bgamari requested changes to this revision.Aug 25 2017, 9:02 AM
This revision now requires changes to proceed.Aug 25 2017, 9:02 AM

I don't think this patch will launch any rockets, yes. I am worried that the person who gets an error message will be unable to resolve the error, but that's a problem for other idioms, too, I imagine.

ezyang updated this revision to Diff 14227.Oct 1 2017, 10:52 PM

try again ci

bgamari requested changes to this revision.Oct 3 2017, 12:28 PM

@ezyang, it looks like you may need to rebase this to eliminate the build issues.

This revision now requires changes to proceed.Oct 3 2017, 12:28 PM
ezyang updated this revision to Diff 14242.Oct 3 2017, 3:31 PM

rebase for ci

ezyang updated this revision to Diff 14298.Oct 7 2017, 12:12 PM

don't print kinds when they are boring

bgamari accepted this revision.Oct 9 2017, 2:22 PM

This looks good but I'm holding off on merging any more patches until Harbormaster has caught up and the tree is green.

This revision is now accepted and ready to land.Oct 9 2017, 2:22 PM
This revision was automatically updated to reflect the committed changes.