tweag / linear-base

Standard library for linear types in Haskell.
MIT License
336 stars 37 forks source link

Dupable wars, episode IV: a new plan #343

Closed aspiwack closed 2 years ago

aspiwack commented 3 years ago

Background

I've been insisting, in the past few years, that the Dupable type class ought to:

To this effect, we've been using dupV :: a %1 -> V n a as our main type class method.

We realised long ago that the Data.Applicative instance for dupV is not super efficient, as it allocates intermediate arrays for each use of (<*>). Which I have proposed in the past should be solved by using pull arrays instead (#208) and deducing dupV from the pull-array based duplication function.

Another proposal which has been floated is to specialised to V 2, which would be sufficient (https://github.com/tweag/linear-base/issues/151#issuecomment-690130887). I find my explanation, in this comment, that V 2 is insufficient to be lacking: I can defined dupV in term of dup2 (equivalently dupV2). I didn't explain why it is not a great idea.

Movable -> Dupable

A typical instance of Dupable will deep-copy the data type. When I defined dupV @n in terms of dup2, I need to do n-1 of these copies. This is often ok, but if I have a Movable instance, I can do a single copy:

dupV x = case move x of
  Ur x' -> pure x')

It would be quite a pity to forbid ourselves from using this when we can.

A streaming hot approach

I was thinking about the choice between non-mutable and mutable array for the implementation of V (#312, #341). And was starting to be a bit dismayed by the seemingly untamable zoology of twisted little data structures all alike. How can we keep the complexity low? Do we need a special, scoped, dup function for the mutable case (https://github.com/tweag/linear-base/pull/341#issuecomment-905344920).

Then I realised that I had made a pretty incorrect assumption there: that the only applicable multi-ary Data.Applicative was V. This is very not true: there are also (pull-polarity) streams. This would look something like this:

data Stream a where
  Stream { state :: x, next :: x %1 -> (a, x), final :: x %1 -> a}

instance Data.Applicative Stream where
  pure a = Stream
    { state = Ur a
    , next = (\(Ur x) -> (x, Ur x))
    , final = unur }
  (fs <*> xs) = Stream
    { state = (state fs, state xs)
    , next = (\(sf, sx) -> case (next sf, next sx) of 
                           ((f, sf'), (x, sx')) -> (f x, (sf', sx')))
    , final = (\(sf, sx) -> final sf (final sx))}

(Stream is a variant of AffineStream (Of a) Identity a from the streaming sublibrary with a single occurrence of a (to be able to define instances), Of is linear in a, and which (crucially) cannot decide to end on its own)

We could define dupS :: a %1 -> Stream a as our main method for the Dupable type class. Note how pure gives us the move-based implementation.

We could then derive functions like dupV (or the mutable equivalent) as a derived concept. More generally, we can define

elim :: KnownNat n => Fun n a b -> Stream a %1 -> b

(though the question of doing this efficiently is probably as tricky as in the case of V.elim, but it does give us elimination into V, and into tuples for instance).

This gives us a much more comprehensible Dupable type class too! And it becomes the responsibility of the various data types that we provide to provide a good interface to Dupable. Much more manageable.

A moving touch

There is still something unfortunate though (which also holds the current dupV-based abstraction): if I use <*> on pure streams, then I lose the only-one-deep-copy property. Let's look at the instance for lists:

instance Dupable a => Dupable [a] where
  dupS [] = pure []
  dupS (a:as) = (:) <&> dupS a <*> dupS as

If a is movable, then [a] is movable too. However, if each of the a-s is indeed deep-copied only once, the spine of the list is copied n times 🙁 .

I think that the right solution is to do some dynamic dispatch:

data BetterStream a where
  Moved :: a -> BetterStream a
  Sequential :: Stream a %1 -> BetterStream a

instance Applicative BetterStream a where
  pure = Moved

  (Moved f) <*> (Moved x) = Moved (f x)
  fs <*> xs = (toStream fs) <*> (toStream xs)

toStream :: BetterStream a %1 -> Stream a
toStream (Moved x) = pure x
toStream (Sequential xs) = xs

We can similary defined elim for this type.

Conclusion (kind of)

I don't feel super great to introduce two extra stream types on top of the existing two. I suppose Stream may want to stay internal while BetterStream is exposed (with a less silly name). A type of stream defined solely to be the output of dupS still does feel a tad unsatisfactory. Still, it's probably the best thing to do. I do wonder though if we don't want BetterStream to expose its constructors, so that V (and its mutable variant) can take advantage of it for a slightly faster build in the Moved case. Or maybe we have a clever elim' function with a type like

elim' :: (a -> b) -> (Fun n a b) -> BetterStream a %1 -> b

This would avoid displaying one additional stream types. I don't quite know yet.

Anyway, this does look like the right way forward, doesn't it?

aspiwack commented 3 years ago

I forgot a probably important point: you can define dupS in terms of dup2:

dup2 :: a %1 -> (a, a)

dupS :: a %1 -> BetterStream a
dupS a = Sequential $ BetterStream
  { state = a
  , next = dup2
  , final = id }
Divesh-Otwani commented 3 years ago

I'm just going to comment that I love this title. I'll give my thoughts on the content a bit later.

treeowl commented 3 years ago

I know nothing about linear types, but the deep copying/traversal required all over the place seems rather sad. One option would look something like this:

class Dupable a where
  ....
  glump :: Maybe (Dict (Moveable a))

class Consumable a where
   ...
   glamp :: Maybe (Dict (Moveable a))

Now we could use something like

instance (Dupable a, Dupable b) => Dupable (a, b) where
  dup = case glump @(a, b) of
    Nothing -> ....
    Just Dict -> \ab -> case move ab of Ur ab' -> (ab', ab')
  glump = do
    Dict <- glump @a
    Dict <- glump @b 
    Just Dict

I dunno how this all relates to the Applicative stuff you're talking about here.

treeowl commented 3 years ago

Another flavor:

type family IsMoveable a :: Bool
class GoodBool (a :: Bool)
instance GoodBool 'True
instance GoodBool 'False
class GoodBool (IsMoveable a) => Consumable a where ...
class GoodBool (IsMoveable a) => Dupable a where ...
class (IsMoveable a ~ 'True) => Moveable a where ...

This shifts more to the type level, but lots of auxiliary classes show up.

aspiwack commented 3 years ago

Thanks for the suggestions.

I'd say that you generally want to avoid deep copies. So when you are using one of these classes you have to be cognisant of their cost on the particular type you are, e.g., dup-ing (much like .clone() in Rust).

That being said they are natural classes and we do want to get them right. I'm not quite sure what problem your suggestions are intended to address, though, could you elaborate?

treeowl commented 3 years ago

I don't think my approach above is quite sufficient. I think what I'm really trying to do is work more efficiently with the case where move is basically a no-op because the values are pure. In that situation, we really don't want to copy anything. Does Ur have to be a datatype or can it be a newtype? If the latter, I suspect there may be some options with safe coercions.

treeowl commented 3 years ago

OK, now that I've learned what linear types are and read your proposal in detail, I'm pretty much on board. One thing I really don't like: your <*> is not at all associative or commutative when performance is taken into account. We can fix that, at the price of a bit more complexity. The key is to let each stream have both a state (that changes) and an unrestricted "spring" that does not. Then liftA2 can merge the states and the springs separately.

data Stream a where
  AllMovable :: a -> Stream a
  Stream ::
      { _spring :: !(Ur w)              -- movable part
      , _state :: x                     -- state
      , _next :: w -> x %1-> (x, a)   -- next
      , _final :: w -> x %1-> a              -- final
      } %1-> Stream a
instance Data.Functor Stream where
  fmap f (AllMovable a) = AllMovable (f a)
  fmap f (Stream
    { _spring = m
    , _state = st
    , _next = nxt
    , _final = fn}) =
    Stream
      { _spring = m
      , _state = st
      , _next = \w x -> nxt w x & \case
          (x', a) -> (x', f a)
      , _final = \w x -> f (fn w x) }

instance Data.Applicative Stream where
  pure a = AllMovable a
  liftA2 f (AllMovable x) (AllMovable y) = AllMovable (f x y)
  liftA2 f (AllMovable ws) (Stream
    { _spring = Ur wt
    , _state = t
    , _next = nt
    , _final = fnt })
    = Stream
        { _spring = Ur (ws, wt)
        , _state = t
        , _next = \(wsx, wtx) tx -> nt wtx tx & \case
                      (tx', b) -> (tx', f wsx b)
        , _final = \(wsx, wtx) tx -> f wsx (fnt wtx tx)}
  liftA2 f (Stream
    { _spring = Ur ws
    , _state = s
    , _next = ns
    , _final = fns }) (AllMovable wt) = Stream
        { _spring = Ur (ws, wt)
        , _state = s
        , _next = \(wsx, wtx) sx -> ns wsx sx & \case
                      (sx', a) -> (sx', f a wtx)
        , _final = \(wsx, wtx) sx -> f (fns wsx sx) wtx}

  liftA2 f (Stream (Ur ws) s ns fns) (Stream (Ur wt) t nt fnt)
    = Stream
    { _spring = Ur (ws, wt)
    , _state = (s, t)
    , _next =
        \(wsx, wtx) (sx, tx) -> ns wsx sx &
            \case { (s', a) -> nt wtx tx &
              \case (t', b) -> ((s', t'), f a b) }
    , _final = \(wsx, wtx) (sx, tx) -> f (fns wsx sx) (fnt wtx tx) }

We can again define dupS and dup2 in terms of each other:

  dupS :: a %1-> Stream a
  dupS a = Stream
    { _spring = Ur ()
    , _state = a
    , _next = \ ~() s -> dup2 s
    , _final = \ ~() s -> s }

  dup2 :: Dupable a => a %1-> (a, a)
  dup2 a = dupS a & \case
    AllMovable b -> (b, b)
    Stream
      { _spring = Ur w
      , _state = s
      , _next = nxt
      , _final = fn } -> nxt w s & \case
         (s', b) -> (b, fn w s')
treeowl commented 3 years ago

One modification of the above: if we decide that we want users to be able to find out, dynamically, whether the type is movable, then I think we should consider defining

  AllMovable :: Movable a => a -> Stream a

That way, matching on the AllMovable constructor would allow a to be used with any function that has a Movable constraint. That will require defining Dupable and Movable in the same module, but to be honest I think that's almost certainly a good idea anyway. The other potential operational downside is that the AllMovable constructor will grow by a word. I'm ... not that worried. A bigger question is whether you think that sort of dynamic dispatch should be supported or not; I still don't know enough to have a definite opinion. It's almost certainly useful, but I don't know if it can damage any properties you want to preserve.

treeowl commented 3 years ago

By the way: if you're wondering why I didn't pull the "spring" out and use a worker stream type, it's because GHC still doesn't know how to unbox existential types. That'd be a potentially significant performance hit.

treeowl commented 3 years ago

Now I'm starting to doubt myself. Does my version actually do anything better? I'd better go to bed.

aspiwack commented 3 years ago

I think that the problem with your version is that you still get to decompose the non-movable state to match the structure of the applicative expression. So I think that you have essentially the same computational behaviour as my version (possibly worse as you decompose some things twice): you decompose the structure until you hit a Movable substructure, then you use the spring bit.

You may be saved by laziness in some cases (if we use \~(x,y) -> … everywhere), but I don't know how to check this.

treeowl commented 3 years ago

I just realized that there are actually two separate ideas that may (possibly) be worth separating here: movable types and movable values . That suggests something like

data Motion a where
  MovableType :: Movable a => Motion a
  -- For your version, SomeStream b ~ BetterStream
  UnmovableType :: Movable b => a -> SomeStream b a

instance Apply Motion where
  MovableType <.> MovableType = MovableType
  ... -- depends on stream type

class Consumable a => Dupable a where
   motion :: Motion a
treeowl commented 3 years ago

Sorry, it's not an Apply. Needs a custom combiner.

treeowl commented 3 years ago

I am becoming convinced that your BetterStream is sufficient, at least for the "movable values" situation. I was letting my imagination run a bit wild.

treeowl commented 3 years ago

I've been doing a bit of a deep dive into this as part of the generics work (in the name of shaking out the orphan instance mess without introducing fragility in module dependencies). There are ... quite a few knobs to tweak. So ... here we go! I'm going to rename BetterStream to Duplicator for the sake of clarity; that definitely doesn't have to be its final name. Here's one flavor:

data Duplicator a where
  MovingDup :: a -> Duplicator a
  StreamDup :: {-# UNPACK #-} !(Stream_ s a) %1-> Duplicator a
data Stream_ s a where
  Stream_ ::
      s %1-> -- ^ state
      (s %1-> (s, a)) -> -- ^ next; this must be unrestricted
      (s %1-> a) %1-> -- ^ finish
      Stream_ s a
data Stream a = forall s. Stream {-# UNPACK #-} !(Stream_ s a)

We get Applicative Duplicator and Applicative Stream. Additionally:

stepDuplicator :: Duplicator a %1-> (Duplicator a, a)
stepStream :: Stream a %1-> (Stream a, a)
stepStream_ :: Stream_ s a %1-> (Stream_ s a, a)

finishDuplicator :: Duplicator a %1-> a
finishStream :: Stream a %1-> a
finishStream_ :: Stream_ s a %1-> a

Note that Stream_, unlike Stream, can be unpacked and can participate in the worker/wrapper transformation. GHC can't do that sort of thing with existential types. This version allows consumers to choose to use totally different approaches depending on whether they're dealing with MovingDup or StreamDup. If they're consuming a stream all at once, access to the Stream_ may make that perform better (though of course that could also be accomplished using some sort of eliminator).


Alternatively, we could include a Stream in the Duplicator. This would not be unpacked into it, and could introduce performance issues with stepDuplicator in some contexts.


There's another general option for what the stream might look like:

data Duplicator' a where
  MovingDup' :: a -> Duplicator a
  StreamDup' :: a %1-> {-# UNPACK #-} !(Stream'_ s a) %1-> Duplicator a
data Stream'_ s a where
  Stream'_ ::
      s %1-> -- ^ state
      (s %1-> (s, a)) -> -- ^ next; this must be unrestricted
      (s %1-> ()) %1-> -- ^ finish
      Stream'_ s a
data Stream' a = forall s. Stream' a {-# UNPACK #-} !(Stream'_ s a)

This lets users end the stream precisely when they're done with it, rather than when they have one more element to go, which seems much friendlier. The potential downside I see is that the first duplication must occur when the duplicator is built, which I imagine could shift work earlier than desired in some situations. As a result, it might be better to offer the Duplicator' version separately, with functions to convert from Duplicator, Stream, and Stream_ to Duplicator', Stream', and Stream'_, respectively.

aspiwack commented 3 years ago

I'm not convinced that the unpacking buys us much, but I'm open to the idea. At least, we'd have to check the Core to ensure that the reboxings are eliminated.

In principle I prefer the former version, because it is likely that the finish function will do some work. So there is a hidden extra duplication hidden.


I think that Replicator would be a better name than Duplicator, if we are to go for this sort of name.

treeowl commented 3 years ago

One challenge: these streams aren't (efficiently) Dupable. To duplicate a stream, you have to step it to get a value, then dupS that value to get a new stream. Awkward. First guess: StreamDup (or StreamRep, as I guess you'd call it) should wrap a Dupable s constraint. Concern: in the common case that s ~ a, the dictionary construction function will be recursive. Is that okay, or will it clog the optimizer?

An additional issue: for some reason, Dupable has a Consumable superclass constraint. If, in the real world, everything that can be duplicated can be consumed, then that's fine. However, in that case, it's a bit awkward that the Replicator doesn't give you a way to consume the value, so (absent dupV) there's no way to write a default consume using Dupable methods. Maybe it should offer one.

Divesh-Otwani commented 3 years ago

I think the original stream approach by @aspiwack (with BetterStream) does work and is a fine solution to (1) n-generation, (2) applicative support and (3) minimizing not-needed deep copies. It's not perfectly elegant but is a good improvement on V n a.

I would suggest compacting the definition but maybe there are reasons why this doesn't work:


data Stream a where
  Repeat :: a -> Stream a
  Affine :: x %1-> (x %1 -> (x, a)) -> (x %1-> ()) -> Stream a

class Dupable a where
  dupS :: a %1-> Stream a

instance Applicative (Stream a) where
  pure = Repeat
  Repeat f <*> Repeat x = Repeat f x
  Repeat f <*> xs = fmap f xs
  fs <*> Repeat x = fmap ($ x) fs
  -- other case as before
treeowl commented 3 years ago

@Divesh-Otwani, I agree it works, but there are a few issues. Some things I think we want to be able to do:

  1. Avoid producing a seed that we're not going to use. @aspiwack's version accomplishes this, except in the degenerate case where we consume the stream. Your version does not do so, because you need to dispose of the final seed using the x %1-> () function.
  2. Produce really clean Core when transforming streams and when consuming streams all at once. Based on experience and very limited experimentation, I suspect this is best done by having an underlying Stream_ type without sums or existentials. But much more experimentation will be required to make sure I'm getting this right.
  3. Write an efficient, or at least reasonably efficient, Dupable instance for streams themselves. This comes down to streams offering an efficient way to duplicate their seeds. @aspiwack's streams, if they're written with unrestricted access to next and finish, support duplication like this:

    instance Dupable a => Dupable (BetterStream a) where
      dupS (Moved a) = Moved (Moved a)
      dupS (Sequential s) = Sequential <$> dupS s
    instance Dupable a => Dupable (Stream a) where
      dupS (Stream (s0 :: s) nxt fin) = Sequential $ Stream s0 nxt' fin'
        where
          nxt' :: s %1-> (s, Stream a)
          nxt' s = nxt s & \case
            (s', a) -> (s', toStream (dupS a))
          fin' :: s %1-> Stream a
          fin' s = Stream s nxt fin

    One potential problem here is that instead of directly splitting the seed, we have to step it to produce an a and then convert that back to an s. Another potential problem: there's no special facility for the case where the seed is Movable. One option, which I have some concerns about, is to stash a Dupable s dictionary in the Stream. Then

    instance Dupable (Stream a) where
      dupS (Stream s0 nxt fin) = dupS s0 & \case
        Moved s -> Moved (Stream s nxt fin)
        Sequential (Stream x nxt' fin') = Sequential (Stream x (nxt' >>> \case (x', s) -> (x', Stream s nxt fin)) (\x' -> Stream (fin' x) nxt fin)

But like I said, I wonder if the recursion there will cause optimization trouble. Big question: are there important cases where the seed will be movable even though the original value is not?

Divesh-Otwani commented 3 years ago

I think I'm missing something with (3) -- could you help clarify? If Dupable just duplicates the original item in a better stream, how is the instance you provided for Stream a correct? It should be a better stream, each of whose elements is the original stream.

I don't understand why you are stepping the state instead of doing this:

instance Dupable a => Dupable (Stream a) where
  dupS :: Stream a %1-> BetterStream (Stream a)
  dupS (Stream (s0 :: s) nxt fin) = Sequential $ Stream s0 nxt' fin'
    where
      nxt' :: s %1-> (s, Stream a)
      nxt' s = (s, Stream s nxt fin)

      fin' :: s %1-> Stream a
      fin' s = Stream s nxt fin
treeowl commented 3 years ago

@Divesh-Otwani, your nxt' isn't linear; that won't type check.

Divesh-Otwani commented 3 years ago

@treeowl Hmm, yes I see. I'm thinking about how to implement it. But the question still remains -- shouldn't it be copies of the original stream?

treeowl commented 3 years ago

I don't understand your question.

Divesh-Otwani commented 3 years ago

In lists, dupS [1,2,3,...] should be [[1,2,3,...], [1,2,3,...], ...] and what you wrote produces [[1,1,1,...], [2,2,2,...], ...].

Divesh-Otwani commented 3 years ago

That's what this does: (but as @aspiwack mentioned it does too many deep-copies if the original list is deep copied only once)

instance Dupable a => Dupable [a] where
  dupS [] = pure []
  dupS (a:as) = (:) <&> dupS a <*> dupS as
treeowl commented 3 years ago

@Divesh-Otwani, well, I was working on the assumption that the streams are only used for duplication. If they're not, that's another story.

treeowl commented 3 years ago

@Divesh-Otwani, I think if you want to be able to duplicate a general stream (i.e., one that doesn't only contain duplicates) then you need to include in the stream a way to duplicate the seed.

aspiwack commented 3 years ago

Ok, hear me out (sorry I couldn't get back to this earlier), I've got a bit of a crazy thought.

Where we are at

To sumarise the state of the conversation: the two deficiencies that we've identified is that

An observation

Before I move on, let me make an observation.

If Dupable a, then I have a function a %1 -> t a for any (Applicative t, Traversable t). It goes like this

dupT :: (Applicative t, Traversable t, Dupable a) => a %1 -> t a
dupT = traverse (\() a -> a) (pure ())

instance Dupable a => Control.Monad (FUN 'One a) where
  …

A solution?

Based on this, we can change the inner stream type, without loss of generality, to duplicate the seed in arbitrary traversable applicatives.

data Streamish a where
  Streamish :: (s %1 -> a) -> (forall t. (Data.Applicative t, Data.Traversable t) => s %1 -> t s) -> s %1 -> Streamish a

class Data.Applicative a where
  pure a = Streamish (unur a) (\(Ur a') -> pure a') (Ur a)
  (Streamish givef multf sf) <*> (Streamish givea multa sa) =
    Streamish
      (\(sf', sa') -> givef sf' (givea sa'))
      (\(sf' ,sa') -> (,) Data.<$> multf Data.<*> multa)
      (sf, sa)

Notice how pure @t is used in the implementation of pure and (<*>) @t in the implementation of (<*>) (whereas we only needed pure in dupT above).

Now, we can get the next element by calling the mult map at V2 and the give map on the first copy. We can also consume the stream by calling mult at V0. It's also easy to duplicate the stream. Note however, that Streamish is not Traversable which means that we can't instantiate mult at Streamish a.

We actually haven't used the Traversable instance yet, though. But we need it to create a Streamish from functions a %1 -> (a, a) and a %-> () using (a variant of) dupT (maybe we could identify a weaker class that also includes Streamish, but I don't know what it would be, nor whether it's desirable).

Is it a good idea? I don't really know. It may be a little too cute. In this version, making a Streamish a out of an a %1 -> (a, a) and an a %-> () may be slow than the previous version (as the reader monad uses consume at every return and each consume is a waste). It's also very polymorphic, which probably means less well-optimised code. Since we basically use only V2 and V0, we may also just define

data Streamish a where
  Streamish :: (s %1 -> a) -> (s %1 -> (s, s)) -> (s %1 -> ()) %-> s %1 -> Streamish a

and get the same effect. Maybe this is the right definition. Though I must admit that very polymorphic definitions have quite a lot of appeal.

treeowl commented 3 years ago

If we give up on making the fundamental stream type Applicative, we gain the option of revealing the seed.

class (Consumable a, s ~ Seed a) => Dupable s a where
  type Seed a
  dupS :: Replicator s a -- for some implementation of Replicator

(It's definitely possible to do this with a single-parameter Dupable class, but I'm not a fan of the way constraints tend to look in that style.)

Then we can impose the constraints on the seed from outside, which is probably more efficient operationally as well as more flexible:

instance Consumable s => Consumable (Replicator s a)
instance Dupable s => Dupable (Replicator s a)
instance Movable s => Movable (Replicator s a)

Rather than an Applicative instance, we'd get custom functions

bleep :: a -> Replicator a a
bloop :: (a %1-> b %1-> c) -> Replicator s a %1-> Replicator t b %1-> Replicator (s, t) c
treeowl commented 3 years ago

We may actually want

class (Consumable a, Dupable (Seed s) s, s ~ Seed a) => Dupable s a where
  type Seed a
  dupS :: Replicator s a

because it seems unlikely in practice that the seed type can't be duplicated and consumed generally. In most cases, Seed s ~ s, but I don't think we'd gain much by requiring that.

Divesh-Otwani commented 3 years ago

The last definition seems elegant to me:

data Streamish a where
  Streamish :: (s %1 -> a) -> (s %1 -> (s, s)) -> (s %1 -> ()) %-> s %1 -> Streamish a

I generally don't like super polymorphic definitions unless we see a strong need. I think it addresses (1) n-generation, (2) an applicative instance, (3) seed-friendly replication if the way you duplicate a moveable value is by making s some Ur a.

treeowl commented 3 years ago

@Divesh-Otwani, I don't see how that gives you friendly stream duplication when s is Movable. My version is really not "super polymorphic"; I find it more "Haskelly" actually.

aspiwack commented 3 years ago

If we give up on making the fundamental stream type Applicative, we gain the option of revealing the seed.

That the streams (well the replicators) be applicative is the point. I'd much rather not have an extra parameter to Dupable either.

@Divesh-Otwani, I don't see how that gives you friendly stream duplication when s is Movable. My version is really not "super polymorphic"; I find it more "Haskelly" actually.

I think “super polymorphic” was referring to my forall t. (Applicative t, Traversable t) => … proposal. This is all with an understanding that a replicator is either a Streamish a or an unrestricted a, to handled the movable case.

aspiwack commented 3 years ago

Oh dear! As I'm posting this, I see that the previous comment was “24 days ago”. Sorry for being so unresponsive.

treeowl commented 3 years ago

Okay, I'm convinced to drop the type family thing. How about this:

data Duplicator a where
  Duplicator :: Dupable s => s %1-> (s %1-> (a, s)) -> (s  %1-> a) -> Duplicator a

That lets us duplicate streams efficiently, terminate early (with consume), and otherwise do all the stuff.

My only concern: when s ~ a, will having a cyclical reference between the Dupable dictionary and its Duplicator get in the way of compiler optimizations?

aspiwack commented 3 years ago

My only concern: when s ~ a, will having a cyclical reference between the Dupable dictionary and its Duplicator get in the way of compiler optimizations?

I think that it's probably fair to just store the s %1-> () and s -> (s, s) methods.

Or we may want to store an s %1 -> Duplicator s method directly.

But trying to make everything mutually recursive with the Dupable type seems a bit overkill to me.

Note that when we are using this type, s is not known to be movable. So we don't need to be able to optimise for this case.