
On Thu, Sep 15, 2011 at 7:51 AM, Simon Peyton-Jones
class Select (rec :: *) (fld :: String) where type ResTy rec fld:: * get :: rec -> ResTy rec fld
data T = MkT { x,y :: Int } instance Select T "x" where get (MkT {x = v}) = v
And now we desugar f.x as get @T @"x" f
That's close to our approach, yes. To avoid the ambiguity in the type of 'get' (which we call 'select'), we introduce a type constructor < Lab :: lab -> * to build singleton types out of type-level lables. Then the Select class is defined by: < class Select (t :: *) (f :: lab) = (r :: *) < where select :: t -> Lab f -> r and 'f.x' is desugared to 'select f #x' (again, using '#x' as syntax for the label thingy). The potential advantage to this approach is that it allows select to behave normally, without the need to insert type applications (before type inference); on the other hand, it requires syntax for the singleton label types. Take your pick, I suppose. :)
You probably don't use the idea of extending to arbitrary other functions do you? (Which Ian does not like anyway.) Something like
getIndex :: T -> Int getIndex (MkT x y) = x+y
Then I'd like to be able to say
t.getIndex
So there's an implicit instance instance Select T "getIndex" where type ResTy T "getIndex" = Int get = getIndex
We don't support that for arbitrary functions, no. On the other hand, our Select class is exposed, so the user can potentially add new instances; for a silly example in Habit: < newtype Temperature = Temp Signed < < instance Temperature.celsius = Signed where < (Temp c).celsius = c < < instance Temperature.fahrenheit = Signed where < (Temp c).fahrenheit = 32 + (c*9)/5
It's a little unclear what operations should be in class Select. 'get' certainly, but I propose *not* set, because it doesn't make sense for getIndex and friends. So that would mean you could write a polymorphic update:
We treat update as a separate class, < class Update (t :: *) (f :: lab) < where update :: t -> Lab f -> t.f -> t and desugar update syntax, something like: < e { x = e' } to calls to the update function < update e #x e' As with Select, this should allow polymorphic update functions: < updX :: Update f #x => f -> f.x -> f < updX f e = f { x = e } /g -- "I’m surprised you haven’t got a little purple space dog, just to ram home what an intergalactic wag you are."