CC @simonpj @rrnewton @fryguybob @niteria

Do the constructors need to be magic like that? I rather have a magic way to construct a Ref# so all exposed variants are non-magical.

Perhaps we constrain the RuntimeReps in -> so whatever magic constructs Ref# is always inlinable / not exists on its own post compilation?

Edward K has a package , Structs, that effectively allows unboxed
references in a potentially recursive setting. It's worth looking at as a
point of comparison perhaps

On Tuesday, September 20, 2016, ramonkeypr notifications@github.com wrote:

@ramonkeypr commented on this pull request.

In proposals/0000-mutable-fields.rst
#8 (review)
:

+generate code for other constructors, taking care to add the Void
+argument for the State#, and generating an info table with the
+correct information about the mutable fields.
+
+Unpacking constructors with mutable fields
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+UNPACK must be a no-op on constructors with mutable fields. There's
+no sensible way to make UNPACK work with mutable fields.
+
+Drawbacks
+---------
+
+The GC write barrier for a mutable constructor may be a little less
+efficient than the write barrier for a MutVar#, but this is more
+than compensated for by losing a layer of indirection.

Has the effect of "losing a layer of indirection" been measured and
benchmarked? Instinctively, this seems correct to me, that removing a layer
of indirection is more beneficial than the performance hit of the GC write
barrier for a mutable constructor.

—
You are receiving this because you are subscribed to this thread.
Reply to this email directly, view it on GitHub
#8 (review),
or mute the thread
https://github.com/notifications/unsubscribe-auth/AAAQwoIf5HDBgszUTJGoFyziBLBKqnq_ks5qr3nggaJpZM4KBKtX
.

Cc @ekmett , this seems very related to your structs package / codes.

From a surface syntax standpoint, I don't like the magical use of IOField. What if we introduce a new keyword mutable and require the GADT syntax at the bottom of the proposal?

data MutPair :: Type -> Type -> Type where
  MutPair :: mutable a -> mutable b -> IO (MutPair a b)

Differentiating between an IOField and a STField could be done by looking at the monad mentioned in the return type.

Can I declare a mutable field with record syntax? If so, what are the typing rules for record selection and update?

Would it be feasible to support mutable unboxed fields? It would be nice to have an "IORef Int#". Presumably Ref would need to gain an argument to describe the representation of the referent.

I very much like the fact that this involves the compiler properly knowing about the mutable fields and generating info tables, since this means profiling should work, whereas with @ekmett's cunning hack all your mutable types are the same as far as the profiler can tell.

Will there also be a Ref type, as well as Ref#? It'd be nice if error messages can mention Ref rather than scary # types :-)

Something I've been working on in my own (unpublished, broken, incomplete & in eternal development hell) unboxed-records-with-first-class-labels-library is the freezing & thawing of records, analogous to the way it works for e.g. (im)mutable vectors. That way my main simulation core can run blazingly fast in ST while calculating statistics after a round can be done in a nicely pure interface.

Do you see (the value of) any way of extending the current proposal later to support something similar?

Will it be possible to compare such constructors for reference equality? How would that look?

I have a bunch of additional features that I want and don't need to be fully worked out yet, but might influence decisions about syntax now. One consideration would be including memory model information. In the GADT form this could be something like AtomicRef#. Another extension is arrays with ArrayRef#. I want this feature in the context of STM too which would likely add some metadata to the representation. This might be just using STM instead of IO in the GADT syntax. I also want sum types. All together I would like to be able to write this for a Hashed Array Mapped Trie:

data Node k v where
    Level :: Word -> ArrayRef# (Node k v) -> STM (Node k v)
    Leaf :: Hash -> ArrayRef# (k,v) -> STM (Node k v)

or

data Node k v where
    Level :: Word -> ArrayRef# (Node k v) -> STM (Node k v)
    Leaf :: Hash -> k -> v -> STM (Node k v)
    Leaves :: Hash -> ArrayRef# (k,v) -> STM (Node k v)
    Nil :: STM (Node k v)

or even better:

data Node k v where
    Level :: Word -> ArrayRef# (Node k v) -> STM (Node k v)
    Leaf :: Hash -> k -> v -> Node k v
    Leaves :: Hash -> ArrayRef# (k,v) -> STM (Node k v)
    Nil :: Node k v

What are the rules for what monad goes on the RHS of a constructor signature? It seems like there is a spectrum here between (1) only supporting raw State# types, and (2) giving special treatment to IO/ST/STM.

@adamgundry Record selection works smoothly I think - the record selector returns a Ref# s a, and the typing is exactly as if you'd written the record selector by hand. Record construction should also work nicely, although of course the record constructor has an IO or ST type. Record update should probably be disallowed for a record with mutable fields. I'll add some notes about this to the proposal.

@rwbarton It would be nice to allow mutable unboxed fields. In fact, there's no reason why Ref# shouldn't be able to take a representation-polymorphic type argument, since that doesn't affect the representation of the Ref# itself. However, we would need a family of primitives for reads and writes at the different unboxed types. I'll add a section about this to the proposal.

@goldfire yes GADT syntax gives us a great way to specify whether you want IO or ST (or later STM), so I agree this is the way to go. There is still magic though: mutable a turns into a for the constructor, but IOField a when pattern matching. I'm not crazy about adding a new keyword, but I don't have a better suggestion so I think we could go with this. Anyone else have thoughts before I update the proposal?

I would hope that it's not hard coded to just ST and IO, at the very least I've my own third sibling ,
STE https://hackage.haskell.org/package/monad-ste that is valid in any use site of MonadPrim or or PrimBaseMonad along with ST and IO

Would this boil down to "is the monad thing a new type around the raw internal rep that we use for IO Or ST"?

Granted there's then several parallel yaks around fields that form valid mvars or stm variables I guess ?

@fryguybob why do you say we would need a different AtomicRef#? I imagined we would just have atomic primops that operate on the ordinary Ref#, in the same way that we have atomic primops for MutVar#.

@simonmar right, this choice would go along with having a memory model. C++11/14/17 whatever distinguishes atomic locations and concurrent accesses (with at least one a write) outside of those locations are undefined behavior. Other approaches may work but at a minimum we should be ensuring that enough information gets down to say the LLVM level, if it is doing the code generation. For instance we may know that an atomic release store on TSO is a normal store, but we don't want LLVM to reorder that store in a basic block. I imagine we are doing the right thing now for this particular case, but it may be very convenient to distinguish explicitly synchronization locations when it does come to having a memory model. In addition, I think volatile is considered orthogonality in LLVM preventing things like accumulating in a register from a value that may be accessed in the same thread from a signal handler.

Just leaving my reddit comment here for consideration...

Yes, I'd also prefer some syntactic clue, that something different is going on.

data MutPair a b in IO = MutPair (IOField a) (IOField b)

sounds like a possibility.

@fryguybob I was writing a message earlier to thank you for such detailed answer but it seems I've never sent it, so thank you!

Btw, did anything change regarding this topic? I know it's not the highest priority but I'm waiting for it like crazy now! :)

@wdanilo I don't have any major updates at this point. I will probably have discussions with people about working toward an implementation that can be merged in at some point at Haskell Symposium.

If the linear types proposal is accepted, we could perhaps someday purely do this at the library level. I'd be interested to see that design fleshed out.

I think it's worthwhile to describe the difference between a primitive mutable field and a lifted one in full detail because a closure with only primitive mutable fields do not need write barrier, while lifted fields require them. I even prefer the extension can be split into two variations: MutableFields and PrimMutableFields for different performance consideration.

@winterland1989 I would expect the compiler to just do "the right thing" when emitting code (e.g., if it does not need a write barrier it should not emit one). What would be the benefit of having two separate extensions?

@yav The benefit of a separate PrimMutableFields is twofold:

1. Currently, we don't have primitive references. Users simulate it with MutableByteArray#, but it carries an extra word (length which is always 1). PrimMutableFields can provide a good replacement.

2. I believe PrimMutableFields have a different impact on implementation and performance, and some operations should be limited to primitive fields, such as fetch-and-add.

Of course, if we can state all these differences clearly and the compiler is smart enough to always do the right thing, a unified extension is OK.

@winterland1989 I think we should be fine with just one extension. In my implementation you can specify an unlifted type directly and it does what you would expect. Matching on an unlifted field gives a RefU# type which supports only unlifted types. Writing to a non-pointer field does not incur the GC write barrier. If you have a constructor with only non-pointer fields I do still generate two info tables. All the information is available at the right place for me to improve that, however.

I think some sort of levity polymorphism would be needed to handle what is normally done with strictness and unpacking. If you had something like:

data M a where
    MkM :: {-# UNPACK #_} mutable !a -> IO (M a)

When you match on an M Int do you get a Ref# or a RefU#? I haven't gone down that rabbit hole yet.

@fryguybob The unpacking example probably shouldn't work since we don't allow unpack polymorphic field anyway. But we probably shouldn't allow unpacking arbitrary concrete type either.

Do you think it helps if we introduce another mutable# keyword? We can limit the types which mutable# accept (and unpack), matching on a mutable# field will always result in a RefU#, which may support exotic atomic operations.

Is someone still working on this?

@treeowl I've wondered the same thing, I think this would open up lots of interesting Haskell performance which didn't rely on strange aspects of ArrayArray# and the like.

I have worked on it some in the last year when I had a little time.

https://github.com/fryguybob/ghc/tree/wip/ryates/mutable-fields-9

It is sort of in a state of minimal working example for only IO based mutable constructor fields.

Now that we have -XLinearTypes, I think there's room in this proposal for a third Data.Mutable API as well. Maybe something like:

module Data.Mutable.Linear where
  type Mutable a = ??? -- Unsure what this should be
  readRef :: Mutable a %1-> (Ur a, Mutable a)
  writeRef :: a -> Mutable a %1-> Mutable a

I'd imagine if we wanted to leverage LTs for this proposal, more changes would also be needed.

I would be very happy to see progress here! Thanks for your efforts, @fryguybob.

I'm not convinced considering linear types adds any value to this proposal. Sure, the API will be unsafe, but then you can always expose a safe, linearly-typed layer over it, as is the case for mutable arrays, for example. The primitives are ST/IO-based (e.g. state-token passing based), and it works well enough. Unless I see a use case that really needs specific treatment for linear types, I don't see why we should complicate the proposal even more.

@sgraf812 If I understand this proposal correctly, that route would not work very well. Correct me if I'm wrong:

The proposed extension generates Mutable fields in IO or ST, and when you pattern match on the record, you're now forced to use either of those. So the benefit of adding LTs as a third option would be to avoid having the end-user (i.e. the person who defined their records) perform unsafe operations. It's not really worth it if you have to write the unsafe IO to LT wrapper for each of your records. This is unlike mutable arrays, which are a single type and therefore can hide the IO completely internally in a single module. Mutable record fields otoh give you that IO/ST everywhere you define them.

More concretely:

I don't think you can safely write this shim:

module Data.Mutable.Linear where
  type Mutable a = Data.Mutable.IO.Mutable a
  readRef :: Mutable a %1-> (Ur a, Mutable a)
  writeRef :: a -> Mutable a %1-> Mutable a

because that would allow you to break referential transparency. There's no guarantee that that IO.Mutable a is used linearly throughout the program. With the linear mutable arrays you mention, you can use the module system to get this guarantee.

So I think that would be the value of including a LT option to this extension. We would need a different Mutable type for LTs that is distinct, and we would then know that all Linear.Mutable values are used linearly, which in turn allows for this safe, linear, pure API. And frees the end-programmer from unsafe boilerplate.

Whether or not that should go in this extension or a future incremental one 🤷‍♂️ This proposal has plenty of value as-is and great work already towards implementation thanks to @fryguybob So a future incremental one may make more sense, especially since -XLinearTypes is so new and we are still learning our way around it as a programming community.

Correct me if I'm wrong: The proposed extension generates Mutable fields in IO or ST, and when you pattern match on the record, you're now forced to use either of those.

Basically, yes. I'm not familiar with the implementation, but I'm pretty sure that internally we won't have "implementations in IO or ST", but just one that uses state-token passing, e.g. State# s -> (# State# s, t #), which is representationally equal to ST s t and to IO t if s is specialised to RealWorld#. Note that the arrow there is basically a linear arrow for all intends and purposes (it seems that linear-base even redefines it as such), but it is not really checked by GHC (which has led to bugs in the past) and it doesn't matter for surface language semantics, because it's an implementation detail of the compiler. (Whether the compiler should make more use of linear types in its PrimOps is an entirely unrelated discussion.)

"Make it compatible with Linear Types" isn't a demand that makes sense; You can always use an unsafe non-linear arrow and coerce it into a linear one, offering a safe API over that. You restrict the programs the user can write, thereby making an API that previously allowed unsafe operations into one that only allows safe programs by construction.

With that in mind...

So the benefit of adding LTs as a third option would be to avoid having the end-user (i.e. the person who defined their records) perform unsafe operations. It's not really worth it if you have to write the unsafe IO to LT wrapper for each of your records.

I think you want new syntactic sugar for linear types and mutable record fields. E.g. if you have

data MutPair a b where
  MutPair :: { mutFst :: mutable a
             , mutSnd :: mutable b
             } -> IO (MutPair a b}

You want the corresponding safe, linear API to be "autogenerated" (to the extent that I understand -XLinearTypes):

newtype LMutPair a b = LMutPair' (MutPair a b) -- constructor is internal!
pattern LMutPair :: a -> b -> LMutPair a b
get_mutFst :: LMutPair a b %1-> (a, LMutPair a b) 
get_mutSnd :: LMutPair a b %1-> (b, LMutPair a b)
set_mutFst :: LMutPair a b %1 -> a %1-> LMutPair a b 
set_mutSnd :: LMutPair a b %1 -> b %1-> LMutPair a b

set_mutFst (LMutPair' p) a = unsafePerformIO (writeRef (mutFst p) a) `pseq` LMutPair' p

The other functions are defined similarly to set_mutFst, using an abundance of unsafePerformIO. I already see a bunch of new concerns:

• Should the functions operate in a Linear state monad directly?
• Is get_mutFst :: LMutPair a b -> a OK?
• get_ and set_ is ugly, I want record accessors and update syntax! Can't we integrate it with one of the record field proposals?

Etc. Finally, I don't see why you couldn't just use TH to derive this API from the MutPair data type. Heck, even some Generic-based implementation should do it if we can have generic-lens and you prefer that.

This is unlike mutable arrays, which are a single type and therefore can hide the IO completely internally in a single module. Mutable record fields otoh give you that IO/ST everywhere you define them.

I don't think it's different at all. A data type mit mutable fields that is meant to be used linearly should define a corresponding linear API. linear-base defines its own shim over mutable arrays, for example. If you want to retro-fit a linear API on a mutable data constructor, use the corresponding TH function. Another point for this derivation business not to end up in a language extension.

Frankly, I wish this and the linear types extension were co-designed in the past, rather than trying to retrofit one onto the other after the fact. Being able to tie together the type system changes to low level FFI stuff like this would have been wonderful.

@sgraf812 my concern about PrimMonad specifically is that it is tied into GHC's internal representations of IO and ST. Exposing that in a language feature seems quite wrong. I wouldn't be opposed to using some internal version that doesn't expose that. I am curious whether some linearity-based approach could unify these in a more principled way, but I don't know nearly enough to guess.

I don't think we need to expose the methods of PrimMonad (although we could in a GHC-specific module), it suffices to specify the instances. We do the same for Coercible.

Also note that the proposal already exposes the internal State# s -> (# State# s, t #) type by offering it as one of 3 alternative return types in the constructor signature. If anything, hiding all 3 types behind the rather abstract PrimMonad constraint makes the proposal less implementation specific.

As I said above, I don't see how linear types help. They are just in the type system and have no operational nature. You'd need unsafe primops and hide them behind a linear API (unless you want to extend Core with new LT-specific primitive operations...), which I did in the comment above, using primops this proposal provides.

Is someone still working on this?

I still think this proposal is important, but my bandwidth to work on it is very limited so I'd be more than happy if someone else wanted to pick it up and drive it.

From the perspective of GHC, it would be so good to have some form of this proposal implemented. I believe that we could have significant savings in allocations in GHC by using a transient (e.g. locally mutable and selectively frozen) IntMap data structure backing UniqFM/VarEnv/InScopeSet/whatnot. Each update/insertion into these structures cost us a full re-allocation of the spine. Very costly if they are huge! I think we are suffering death by a thousand papercuts.

Unfortunately, a good source level representation of opt-in mutability eludes me.

Fwiw: we would use this at work if it were implemented! We need it because we have a system in which we have many small components which are being mutated at high rates. There is an overhead to StateT that is becoming too large for us, and IORef is also not great.

It's unclear to me whether Simon's original proposal or a linear-types-focused version would have better usability for our use case. The nice thing for us about a linear-types version is that it would the mutation would be able to live outside of IO.