J Garrett Morris asked me | I also rather like the TDNR proposal, as it's rather similar to the | approach we're taking in Habit (our pet language at Portland State). | However, I'm curious as to why you don't want to quantify over name | resolution constraints. For example, why shouldn't: | | x f = f.x | | be a reasonable function? Yes, it would, and of course any impl of TDNR would need an internal constraint similar to your Select. In my original proposal I was hiding that, but it has to be there in the implementation. But you are right that making it explicit might be a good thing. Esp with Julien's new kind stuff (coming soon) we should be able to say 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 where the "@" stuff is type application, because get's type is ambiguous: get :: forall rec fld. Select rec fld => rec -> ResTy rec fld Just like what Hobbit does really. 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 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: f v = f { x = v } Restricting to record fields only would, I suppose, allow polymorphic update, by adding a 'set' method to Select. Simon
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."
participants (2)
-
J. Garrett Morris -
Simon Peyton-Jones