Opened 6 years ago

Last modified 6 months ago

#2595 new feature request

Implement record update for existential and GADT data types

Reported by: simonpj Owned by:
Priority: normal Milestone: 6.12 branch
Component: Compiler Version: 6.8.3
Keywords: Cc: noah.easterly@…, adam.gundry@…, byorgey@…
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Difficulty: Unknown
Test Case: tc244 Blocked By:
Blocking: Related Tickets:

Description

Ganesh writes: The most important thing for me is supporting record update for
existentially quantified data records, as in the error below.

In general I also find working with code that involves existential
type variables quite hard work - for example I can't use foo as a
record selector either, even if I immediately do something that seals
the existential type back up again.

I don't understand this stuff well enough to be sure whether it's an
impredicativity issue or not, though.

Foo.hs:11:8:
    Record update for the non-Haskell-98 data type `Foo' is not (yet)
supported
    Use pattern-matching instead
    In the expression: rec {foo = id}
    In the definition of `f': f rec = rec {foo = id}

Program is:

{-# LANGUAGE Rank2Types #-}
module Foo where

data Foo = forall a . Foo { foo :: a -> a, bar :: Int }

x :: Foo
x = Foo { foo = id, bar = 3 }

f :: Foo -> Foo
f rec = rec { foo = id }

g :: Foo -> Foo
g rec = rec { bar = 3 }

Simon says: Ah now I see. The relevant comment, TcExpr line 465, says

-- Doing record updates on
-- GADTs and/or existentials is more than my tiny 
-- brain can cope with today

Should be fixable, even with a tiny brain.

Change History (8)

comment:1 Changed 6 years ago by simonmar

  • Architecture changed from Unknown to Unknown/Multiple

comment:2 Changed 6 years ago by simonmar

  • Operating System changed from Unknown to Unknown/Multiple

comment:3 Changed 5 years ago by simonpj

  • Resolution set to fixed
  • Status changed from new to closed
  • Test Case set to tc244

OK I have mostly-implemented this feature request

Tue Oct 28 11:54:27 GMT Standard Time 2008  simonpj@microsoft.com
  * Mostly-fix Trac #2595: updates for existentials
  
  Ganesh wanted to update records that involve existentials.  That 
  seems reasonable to me, and this patch covers existentials, GADTs,
  and data type families.
  
  The restriction is that 
    The types of the updated fields may mention only the
    universally-quantified type variables of the data constructor
  
  This doesn't allow everything in #2595 (it allows 'g' but not 'f' in
  the ticket), but it gets a lot closer.

No need to merge.

Simon

comment:4 Changed 3 years ago by rampion

  • Cc noah.easterly@… added
  • Resolution fixed deleted
  • Status changed from closed to new
  • Type of failure set to None/Unknown

Could this be extended to allow updating the non-universally-quantified type variables of the data constructor? The example code still gives the error:

    Record update for insufficiently polymorphic field: foo :: a -> a
    In the expression: rec {foo = id}
    In the definition of `f': f rec = rec {foo = id}

And it'd be nice to be able to update the existentials.

comment:5 Changed 3 years ago by simonpj

The difficulty is this. A simple, consistent position is this. Consider

data T where
  T1 :: { x1 :: <type1>, x2 :: <type2> } -> T
  T2 :: { x1 :: <type1> } -> T
  T3 :: { x3 :: <type2> } -> t

Then we'd like e { x1=e1 } to be accepted if and only if the desugared version would be accepted:

  case e of 
    T1 { x2 = x2' } -> T1 { x1=e1, x2=x2' }
    T2 {} -> T2 { x1 = e1 }
    T3 {} -> error "Bad update"

The difficulty is that GHC's typechecker typechecks source code not desugared code. This is good because it leads to meaningful error messages. But pattern matching (as in the above case) is the hardest bit of the typechecker, so figuring out whether the desugared version would typecheck is tricky. If the data type T has existentials, or type constraints, or is a GADT, it becomes even more fun.

Last time I looked at this I decided it was too hard to go the whole hog. But I thin the above is the only really consistent position. Quite when I (or anyone else) will get round to doing this I'm not sure!

Simon

comment:6 Changed 3 years ago by simonmar

This has a similar flavour to typechecking pattern bindings, where we decided we wanted the static semantics to be defined by the desugaring (http://hackage.haskell.org/trac/haskell-prime/wiki/SpecifyPatternBindingSemantics). I know nothing about the typechecker, but perhaps this is a two birds/one stone situation?

comment:7 Changed 8 months ago by adamgundry

  • Cc adam.gundry@… added

comment:8 Changed 6 months ago by byorgey

  • Cc byorgey@… added
Note: See TracTickets for help on using tickets.