Some quick responses

1. Splitting
What's the need for splitting anyway?

Just so you can use uniques in a tree-like way, without threading the supply 
around.  No more than that.

This is not needed everywhere.  For example, the Simplifier threads it thus:


newtype SimplM result

  =  SM  { unSM :: SimplTopEnv  -- Envt that does not change much

                -> UniqSupply   -- We thread the unique supply because

                                -- constantly splitting it is rather expensive

                -> SimplCount

                -> IO (result, UniqSupply, SimplCount)}

I suspect that (now that SimplM is in IO anyway) we could use an IORef instead, 
and maybe speed up the compiler.

But perhaps not all uses are so simple to change.

2. The tree

The crucial thing is that there /is/ a data structure – a tree, that is the 
unique supply. So if you have
     f u s = ….(splitUniqueSupply us)…..(splitUniqueSupply us)….
you’ll get the same trees in the two calls.  The supply is just a 
purely-functional tree.

So, for example

  *   The `unsafeInterleaveIO` makes it so that `genSym` is actually forced 
before any of the recursive calls to `mk_split` force their `genSym`, 
regardless of evaluation order
I don’t think this is important, except perhaps to avoid creating a thunk.

  *   This guarentees a certain partial order on produced uniques: Any parent 
`UniqSupply`'s `Unique` is calculated by a call to 
compiler/cbits/genSym.c#genSym() before any `Unique`s of its offsprings are]
  *   The order of `Unique`s on different off-springs of the same `UniqSupply` 
is determined by evaluation order as a result of `unsafeInterleaveIO`, much the 
same as when we create two different `UniqSupply`s by calls to 
`mkSplitUniqSupply`
  *   So, `unfoldr (Just . takeUniqFromSupply) us) !! n` is always 
deterministic and strictly monotone, in the sense that even forcing the 
expression for n=2 before n=1 will have a lower `Unique` for n=1 than for n=2.
I don’t think any of these points are important or relied on.  A different impl 
could behave differently.

  1.  `takeUniqSupply` returns as 'tail' its first off-spring, whereas 
`uniqsFromSupply` always recurses into its second off-spring. By my intuition 
above, this shouldn't really make much of a difference, so what is the 
motivation for that?
I think this is unimportant. I.e. it should be fine to change it.


  1.  Judging from SimplCore, we probably want to `splitUniqSupply` after each 
iteration/transformation, either through a call to `splitUniqSupply` or 
`getUniqueSupplyM`. Is that right?
I don’t understand the question.   If you use the same supply twice, you’ll get 
(precisely) the same uniques.  That may or may not be ok

SImon

From: ghc-devs <ghc-devs-boun...@haskell.org> On Behalf Of Sebastian Graf
Sent: 23 July 2018 12:06
To: ghc-devs <ghc-devs@haskell.org>
Subject: Understanding UniqSupply

Hi all,

I'm trying to understand when it is necessary to `splitUniqSupply`, or even to 
create my own supply with `mkSplitUniqSupply`.

First, my understanding of how `mkSplitUniqSupply` 
(https://hackage.haskell.org/package/ghc-8.4.1/docs/src/UniqSupply.html#mkSplitUniqSupply<https://na01.safelinks.protection.outlook.com/?url=https%3A%2F%2Fhackage.haskell.org%2Fpackage%2Fghc-8.4.1%2Fdocs%2Fsrc%2FUniqSupply.html%23mkSplitUniqSupply&data=02%7C01%7Csimonpj%40microsoft.com%7C58b620e0f148448bbe0608d5f08c485e%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636679407654961407&sdata=cA6N%2FGzMVYKD0fAVkbG%2BC%2F%2FuXuhenR95CwhHQAZrUQ4%3D&reserved=0>)
 works is as follows:

  *   The `unsafeInterleaveIO` makes it so that `genSym` is actually forced 
before any of the recursive calls to `mk_split` force their `genSym`, 
regardless of evaluation order
  *   This guarentees a certain partial order on produced uniques: Any parent 
`UniqSupply`'s `Unique` is calculated by a call to 
compiler/cbits/genSym.c#genSym() before any `Unique`s of its offsprings are
  *   The order of `Unique`s on different off-springs of the same `UniqSupply` 
is determined by evaluation order as a result of `unsafeInterleaveIO`, much the 
same as when we create two different `UniqSupply`s by calls to 
`mkSplitUniqSupply`
  *   So, `unfoldr (Just . takeUniqFromSupply) us) !! n` is always 
deterministic and strictly monotone, in the sense that even forcing the 
expression for n=2 before n=1 will have a lower `Unique` for n=1 than for n=2.
  *   This is of course all an implementation detail
These are the questions that bother me:

  1.  `takeUniqSupply` returns as 'tail' its first off-spring, whereas 
`uniqsFromSupply` always recurses into its second off-spring. By my intuition 
above, this shouldn't really make much of a difference, so what is the 
motivation for that?
  2.  The docs state that the character tag/domain/prefix in the call to 
`mkSplitUniqSupply` should be unique to guarantee actual uniqueness of produced 
`Unique`s. Judging from the implementation of `genSym`, which is unaware of the 
specific domain to draw the next unique from, this is an unnecessarily strong 
condition?! Also there are multiple places in the code base spread over module 
boundaries even (e.g. CorePrep, SimplCore) that call `mkSplitUniqSupply` with 
the same character anyway. Maybe there should at least be some clarifying 
comment on why this isn't a problem?
  3.  Judging from SimplCore, we probably want to `splitUniqSupply` after each 
iteration/transformation, either through a call to `splitUniqSupply` or 
`getUniqueSupplyM`. Is that right?
  4.  What's the need for splitting anyway? I suspect it's a trick to avoid 
state threading that would be necessary if we just had `type UniqSupply = 
[Unique]`. Would that really be a bad thing, considering we mostly work in 
`UniqSM` anyway? Is there anything else to it?
Happy to hear from you!
Cheers
Sebastian
_______________________________________________
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

Reply via email to