On Tue, Sep 9, 2008 at 3:49 PM, Jason Dagit <[EMAIL PROTECTED]> wrote:
> On Tue, Sep 9, 2008 at 9:06 AM, David Roundy <[EMAIL PROTECTED]> wrote:
>
>>> The problem here is that each replace patch we construct in the
>>> sequence basically comes from a different unrecorded state (since they
>>> are a sequence each new one comes from the final state of the previous
>>> one). With the two seals, we get that the sealed phantom on x won't
>>> unify with the unrecorded state.
>>
>> The problem here is that the type of sequenceRepls is wrong--I hadn't
>> looked carefully at that code previously. You're making it always
>> create patches that start at the unrecorded state, but that's not what
>> it's actually doing (or so we hope). All we need to do is to
>> eliminate the Repository argument from sequenceRepls, and the problem
>> is fixed.
>
> I'm very confused by this. We take the result of sequenceRepls and
> hand it off to add_to_pending and applyToWorking which both take a
> sequence starting from the unrecorded state. The new type of
> sequenceRepls from your patch returns an arbitrary starting type,
> which happens to unify with the unrecorded state. But, we could
> equally make it unify with some other function from
> Repository.Internal that takes, say, a recorded state. This seems
> like a violation of type safety to me.
We don't have type safety here, and pretending that we do won't add it.
> I would agree that the recursive call shouldn't return something from
> the unrecorded state, I tried to say that much in my description.
Right, this made the code buggy. It meant that the state of each
patch you added was always the identity state, which is just wrong,
since replace patches are not in fact identity patches. It worked
because we haven't tightened up the lower-level code
(get_force_replace in this case) to be typesafe, and we also haven't
added type witnesses to slurpies.
> But, your version doesn't return something that is ultimately
> constrained to starting in the unrecorded state so it seems dangerous
> to me. My understanding is that we apply the results to the
> unrecorded state very intentionally. Perhaps the unrecorded state is
> not useful here? And if so, why?
It's not useful because you defined the function recursively. In
local functions like this, I think it's generally best to simply
define the types of functions to be what they actually are, rather
than adding additional constraints.
> How about:
> sequenceRepls :: Repository p C(r u t) -> String -> Slurpy -> Slurpy
> -> [SubPath] -> IO (Sealed (FL Prim C(u)))
> sequenceRepls _ = sequenceRepls_
> where
> sequenceRepls_ :: String -> Slurpy -> Slurpy -> [SubPath] -> IO
> (Sealed (FL Prim C(u)))
> <insert your definition of sequenceRepls>
>
> This version would mean than whoever calls sequenceRepls gets
> something from the unrecorded state while fixing the problem we both
> saw in the recursive call.
We could do this, but it doesn't give us any additional safety. The
type checker already knows that the one time we use sequenceRepls it
is in the 'u' state.
If this were an exported function, we might want to do this to provide
a nicer interface.
>>> The only other trick that comes to mind is that it could be:
>>> _foo :: String -> Maybe (FL a C(x y))
>>> _foo _ = Nothing
>>>
>>> That is, we only return non-empty FLs. I've made this change and it
>>> does compile, so I guess I'll now add this to my bag of FL tricks.
>>
>> This isn't really a good trick, since it just works around a bug
>> elsewhere.
>
> I'm sorry, but comments like this are not helpful to me. What bug are
> you thinking of?
The bug *here* is basically that _foo is a non-type-safe function.
It's exporting values with arbitrary type witnesses, which means that
it is equivalent to unsafeCoerceP.
unsafeCoerceP :: forall a b. a -> b
unsafeCoerceP x = case foo1 =\/= foo2 of
IsEq -> x
_ -> impossible
where foo1 :: Maybe (FL Patch C(() a))
foo1 = _foo "input" -- where I give it any input that
leads to a Just value.
foo2 :: Maybe (FL Patch C(() b))
foo2 = _foo "input" -- where I give it any input that
leads to a Just value.
True, this code won't compile unless we enable type witnesses, but
we'd rather keep type witnesses from subverting the type system.
David
_______________________________________________
darcs-users mailing list
[email protected]
http://lists.osuosl.org/mailman/listinfo/darcs-users
