cyclic duck values
Geoffrey Irving
cyclic. It's a very clean sort of cyclic, since it will all get
wrapped up and finalized in the first stage of Ir -> Lir conversion,
but I'm not sure the best way to express it.
First, in order to avoid trying to convert cyclic data structures back
and forth between Haskell, I think the type Datatype will always refer
to a duck value; the Haskell version will exist only temporarily when
someone wants to ask something about the datatype. All Datatypes
(except for a couple primitives) will then be created at Ir -> Lir
conversion time, which is the only stage that has to know about the
cycles.
In Haskell this is all naturally expressible with laziness, of course.
However, since laziness is not a primitive notion in Duck we probably
want to express it through mutable fields. Mutable fields are cleanly
compatible if we switch to effect typing later. For now, I can teach
ToHaskell that Ref t (maybe Mut t or Mutable t?) means a mutable boxed
value, and have ToLir do the appropriate surgery to create the cyclic
values.
In the future, if we decide that we want to teach the duck runtime
that Datatypes are immutable after the initial creation stage, we can
make a mutable DatatypePre type which is unsafely cast to the
immutable Datatype type. This is the kind of thing that general
effect typing makes safe, so if we get that all the better. In fact,
I'll probably do this right away, since it keeps the datatype
interrogation functions outside of the IO monad.
Thoughts?
Geoffrey
Dylan Simon
> Once the first argument to TyCons is a Datatype, Types will become
> cyclic. It's a very clean sort of cyclic, since it will all get
> wrapped up and finalized in the first stage of Ir -> Lir conversion,
> but I'm not sure the best way to express it.
>
> First, in order to avoid trying to convert cyclic data structures back
> and forth between Haskell, I think the type Datatype will always refer
> to a duck value; the Haskell version will exist only temporarily when
> someone wants to ask something about the datatype. All Datatypes
> (except for a couple primitives) will then be created at Ir -> Lir
> conversion time, which is the only stage that has to know about the
> cycles.
>
> In Haskell this is all naturally expressible with laziness, of course.
> However, since laziness is not a primitive notion in Duck we probably
> want to express it through mutable fields. Mutable fields are cleanly
> compatible if we switch to effect typing later. For now, I can teach
> ToHaskell that Ref t (maybe Mut t or Mutable t?) means a mutable boxed
> value, and have ToLir do the appropriate surgery to create the cyclic
> values.
This all seems reasonable. Ref t sounds fine.
> In the future, if we decide that we want to teach the duck runtime
> that Datatypes are immutable after the initial creation stage, we can
> make a mutable DatatypePre type which is unsafely cast to the
> immutable Datatype type. This is the kind of thing that general
> effect typing makes safe, so if we get that all the better. In fact,
> I'll probably do this right away, since it keeps the datatype
> interrogation functions outside of the IO monad.
I don't quite get how this works. You mean you can make a function that does
something like "everywhere freeze" to convert an entire data structure of Ref
a to a, in place?
Geoffrey Irving
For now the Haskell code uses an unsafe castPtr operation, but in duck
we should be able to do it safely by asserting that the two types are
isomorphic and that the source is at least as mutable as the target.
Geoffrey
Dylan Simon
> >> that Datatypes are immutable after the initial creation stage, we can
> >> make a mutable DatatypePre type which is unsafely cast to the
> >> effect typing makes safe, so if we get that all the better. ?In fact,
> >> I'll probably do this right away, since it keeps the datatype
> >> interrogation functions outside of the IO monad.
> >
> > something like "everywhere freeze" to convert an entire data structure of Ref
> > a to a, in place?
>
> For now the Haskell code uses an unsafe castPtr operation, but in duck
> we should be able to do it safely by asserting that the two types are
> isomorphic and that the source is at least as mutable as the target.
>
> Geoffrey
So, they have the same representation. I guess that makes sense. But if I
do (making up syntax and functions):
let x :: Ref Int = newRef 1
let y :: Int = freeze x
writeRef x 2
print y
What do I get? If they alias, then it seems like this violates purity, no?
Geoffrey Irving
Yes. That's why freeze is actually called unsafeFreeze. It's in the
IO monad, and calling it is a promise that you won't ever modify the
value again.
Geoffrey
Dylan Simon
> On Mon, May 2, 2011 at 9:39 AM, Dylan Simon <dylan-...@dylex.net> wrote:
> >> >> In the future, if we decide that we want to teach the duck runtime
> >> >> that Datatypes are immutable after the initial creation stage, we can
> >> >> make a mutable DatatypePre type which is unsafely cast to the
> >> >> immutable Datatype type. ?This is the kind of thing that general
> >> >> effect typing makes safe, so if we get that all the better. ?In fact,
> >> >> I'll probably do this right away, since it keeps the datatype
> >> >> interrogation functions outside of the IO monad.
> >> >
> >> > I don't quite get how this works. ?You mean you can make a function that does
> >> > something like "everywhere freeze" to convert an entire data structure of Ref
> >> > a to a, in place?
> >>
> >> For now the Haskell code uses an unsafe castPtr operation, but in duck
> >> we should be able to do it safely by asserting that the two types are
> >> isomorphic and that the source is at least as mutable as the target.
> >
> > do (making up syntax and functions):
> >
> > ? ? ? ?let y :: Int = freeze x
> > ? ? ? ?writeRef x 2
> > ? ? ? ?print y
> >
> > What do I get? ?If they alias, then it seems like this violates purity, no?
>
> Yes. That's why freeze is actually called unsafeFreeze. It's in the
> IO monad, and calling it is a promise that you won't ever modify the
> value again.
Okay. So presumably there is a safeFreeze that does a full copy, too. What
is the type of these functions, though? Ref a -> a is simple enough, but if
you want to remove refs everywhere -- does the programmer guarantee that the
representations are the same (unsafeCast) or can duck validate that (safeCast)
and/or generate the function with the appropriate type (in the SYB sort of
sense)?
Geoffrey Irving
In addition to Ref t, there are Box t and Vol t for immutable and
volatile (not writable but possibly mutable) boxes, which are
guaranteed to have the same representation as Ref t. Vol t may be a
poor name choice. Checking type isomorphism is fairly easy, so duck
should be able to validate that everything is safe (except for the
freezing itself).
Geoffrey