Changes between Initial Version and Version 12 of Ticket #1999


Ignore:
Timestamp:
May 9, 2011 10:33:08 AM (4 years ago)
Author:
simonpj
Comment:

In our POPL paper Generative type abstraction and type-level computation we proposed to remove the ability to decomopose type applications. So Ganesh's example above would not work any more:

data EqTypes a b where
  EqConstr :: EqTypes a b -> EqTypes (s a) (s b)

eqUnConstr :: EqTypes (s a) (s b) -> EqTypes a b
eqUnConstr (EqConstr eq) = eq

Neither would Jim Apple's example.

This is an un-forced change, and it does reduce expressiveness slightly, with no workaround. On the other hand, it does undoubtedly make things a bit simpler and, as Section 6.2 of the paper says, it allows FC to have un-saturated type functions. BUT for type inference we still need saturated type functions, so allowing un-saturated type functions in the intermediate language only a theoretical improvement -- programmers don't see the benefit.

Dimitrios and I think that it'd be possible to re-add left and right coercions, without too much hassle (and re-add the saturated-type-function reqt to FC). Stephanie, Brent: do you agree?

Meanwhile, Gasnesh, Jim, how much do you care?

All this relates to the ghc-new-co branch, which will shortly become the master, so it's of more than theoretical interest.

Simon

Legend:

Unmodified
Added
Removed
Modified
  • Ticket #1999

    • Property Cc ganesh@… sweirich@… jbapple@… byorgey@… added
    • Property Test Case changed from to T1999, T1999a
    • Property Type of failure changed from to None/Unknown
    • Property Milestone changed from to 6.10 branch
  • Ticket #1999 – Description

    initial v12  
    55 
    66    class C a where 
    7  
    87        f :: G a -> () 
    98 
    109    instance (C ()) => C (b c) where 
    11  
    1210        f (G x) = f x where 
    1311 
    1412    data G a where 
    15  
    1613        G  :: G () -> G (b c) 
    1714}}}