TypeSet.subsetFun'

0 views
Skip to first unread message

Dylan Alex Simon

unread,
Aug 29, 2009, 2:49:30 AM8/29/09
to duck...@googlegroups.com
I'm trying to understand subsetFun'('). Why do we only ever look at the first
of the right side arrow types (al') if the List.elem fails? Shouldn't we try
them all? Is this what the note about rollback and intersect is about? If I
understand, what you need is for the monad to be MonadPlus, not MonadMaybe
(!), so the changes I'm making should make this easier.

On a sort of unrelated note, Infer.cache has a note about only rolling back
some of the state changes. This means finalizing things exactly when they
converge on a fixpoint, right?

:-Dylan

Geoffrey Irving

unread,
Aug 29, 2009, 6:11:00 PM8/29/09
to duck...@googlegroups.com
On Sat, Aug 29, 2009 at 2:49 AM, Dylan Alex Simon<dylan-...@dylex.net> wrote:
>
> I'm trying to understand subsetFun'(').  Why do we only ever look at the first
> of the right side arrow types (al') if the List.elem fails?  Shouldn't we try
> them all?  Is this what the note about rollback and intersect is about?  If I
> understand, what you need is for the monad to be MonadPlus, not MonadMaybe
> (!), so the changes I'm making should make this easier.

Yes, that's what the rollback comment is about. The MonadPlus thing
is amusing. However, if you want to attach real error messages, it
still isn't exactly right; you want mplus but not mzero. :)

I think I'll postpone the tuple stuff until after your changes, since
your changes might also be useful for handling quotients (or maybe
not). I'll get rid of TValue in the mean time, and try to remove some
of the duplicated time inference logic from Interp.

By the way, I think I concluded that the function type related code
would look nicer if TypeFun was a single list of an Either-like type
rather than partitioned into two lists.

> On a sort of unrelated note, Infer.cache has a note about only rolling back
> some of the state changes.  This means finalizing things exactly when they
> converge on a fixpoint, right?

Right.

Geoffrey

Dylan Alex Simon

unread,
Aug 29, 2009, 6:19:42 PM8/29/09
to Geoffrey Irving, duck...@googlegroups.com
> I think I'll postpone the tuple stuff until after your changes, since
> your changes might also be useful for handling quotients (or maybe
> not). I'll get rid of TValue in the mean time, and try to remove some
> of the duplicated time inference logic from Interp.

I consolidated the spec and cons stuff into Infer already, just to get rid of
all direct calls from Interp to TypeSet, but feel free to do whatever since
I've gotten a bit carried away with these changes and probably won't commit
for a couple more hours. I'm too distractable.

:-Dylan

Geoffrey Irving

unread,
Aug 29, 2009, 6:41:56 PM8/29/09
to Dylan Alex Simon, Geoffrey Irving, duck...@googlegroups.com
On Aug 29, 2009, at 6:19 PM, Dylan Alex Simon <dylan-...@dylex.net>
wrote:

>

A few hours (or a day) isn't a problem, so I'm happy to wait.

Geoffrey
>

Dylan Alex Simon

unread,
Aug 30, 2009, 3:15:58 AM8/30/09
to duck...@googlegroups.com
I looked at layout again, and it's actually quite simple to make things work
the way I'd like for let (and nested cases). I've checked it in to my layout
branch. All it does is allows deeper contexts to be less indented (violating
Note 1 of the haskell rules). So, for example, this program is legal:

f = case x of
y -> case z of
w -> ...

Or, with lets:

f x = let y = case x of
z -> let
w = z in w

Effectively this does two things:

1. Disallow empty implicit contexts. Otherwise, these would often be parsed
as {}, which is (on very rare occasions) a sensible thing to want, but it
seems reasonable to say you need to explicitly write "{}" if you do.

2. Makes programs that were previously incomplete (e.g., a "case ... of"
somewhere deeply nested for which the cases had not yet been filled in)
possibly valid, and possibly in unintentional ways. It also lets you, for
example, make it impossible to get back to a certain context (even the top
level) if a nested level has taken it over.

My feeling is that 1 is completely fine, and 2 might make debugging some
things slightly more tricky, but I doubt in any important ways. If we really
don't think this is safe, I have a less powerful and more messy backup
proposal that would make both of the earlier programs valid but not this one:

f = let
x = 1
y = case x of
z -> z in y


We still aren't implementing Note 5 of the haskell rules, it seems, so this
doesn't work with the in:

f x = let y = case x of z -> z in y

But that's an orthogonal issue that will be more important for lets
themselves.

:-Dylan

Geoffrey Irving

unread,
Aug 30, 2009, 9:33:09 AM8/30/09
to duck...@googlegroups.com
On Sun, Aug 30, 2009 at 3:15 AM, Dylan Alex Simon<dylan-...@dylex.net> wrote:
>
> I looked at layout again, and it's actually quite simple to make things work
> the way I'd like for let (and nested cases).  I've checked it in to my layout
> branch.  All it does is allows deeper contexts to be less indented (violating
> Note 1 of the haskell rules).  So, for example, this program is legal:
>
>  f =   case x of
>      y -> case z of
>    w -> ...
>
> Or, with lets:
>
>  f x = let y = case x of
>    z -> let
>    w = z in w
>
> Effectively this does two things:
>
> 1. Disallow empty implicit contexts.  Otherwise, these would often be parsed
>   as {}, which is (on very rare occasions) a sensible thing to want, but it
>   seems reasonable to say you need to explicitly write "{}" if you do.

Yep, I agree that {} is fine.

> 2. Makes programs that were previously incomplete (e.g., a "case ... of"
>   somewhere deeply nested for which the cases had not yet been filled in)
>   possibly valid, and possibly in unintentional ways.  It also lets you, for
>   example, make it impossible to get back to a certain context (even the top
>   level) if a nested level has taken it over.

I think this does make it too easy to take over the toplevel context,
which would result in weird error messages. It essentially makes
layout strongly nonlocal.

> My feeling is that 1 is completely fine, and 2 might make debugging some
> things slightly more tricky, but I doubt in any important ways.  If we really
> don't think this is safe, I have a less powerful and more messy backup
> proposal that would make both of the earlier programs valid but not this one:
>
>  f = let
>    x = 1
>    y = case x of
>    z -> z in y

Can you describe the messy one? The first option that comes to mind
is "nested contexts must be more indented than their parents unless
the parent started on the previous line."

> We still aren't implementing Note 5 of the haskell rules, it seems, so this
> doesn't work with the in:
>
>  f x = let y = case x of z -> z in y
>
> But that's an orthogonal issue that will be more important for lets
> themselves.

Yeah, that's why I didn't implement it; I realized it was important
only for lets. It's trivial to add to the parser (just allow "error"
in place of '}'), but I'm not sure if it requires a change the layout
pass itself.

Geoffrey

Dylan Alex Simon

unread,
Aug 30, 2009, 10:37:00 AM8/30/09
to Geoffrey Irving, duck...@googlegroups.com
> > 2. Makes programs that were previously incomplete (e.g., a "case ... of"
> > ? somewhere deeply nested for which the cases had not yet been filled in)
> > ? possibly valid, and possibly in unintentional ways. ?It also lets you, for
> > ? example, make it impossible to get back to a certain context (even the top
> > ? level) if a nested level has taken it over.

>
> I think this does make it too easy to take over the toplevel context,
> which would result in weird error messages. It essentially makes
> layout strongly nonlocal.

We could explicitly disallow replacing a column-1 context. Though, I think:

main = do
...

seems potentially useful, even.

> Can you describe the messy one? The first option that comes to mind
> is "nested contexts must be more indented than their parents unless
> the parent started on the previous line."

Yeah, that's basically it. It comes down to this: Implicit is amended and the
"top" function is changed so that, if the top Implicit context has never been
used to insert a ';', then it is skipped and recurses to the next down context
to determine the "top" column. So, if the outermost context is implicit,
you'd never be able to take it over (except in the first line).

> > We still aren't implementing Note 5 of the haskell rules, it seems, so this
> > doesn't work with the in:
> >

> > ?f x = let y = case x of z -> z in y


> >
> > But that's an orthogonal issue that will be more important for lets
> > themselves.
>
> Yeah, that's why I didn't implement it; I realized it was important
> only for lets. It's trivial to add to the parser (just allow "error"
> in place of '}'), but I'm not sure if it requires a change the layout
> pass itself.

I don't completely get this. Every rule including '{' '}' needs to be
changed? It is still useful with what we have now, in my code above for
example.


By the way, my most recent commit adds more functions in base.duck and tests
in base-test.duck. Some of the lines are commented out, as they seem to
expose as many as four separate bugs (at least one of which is mine), but I
probably won't have time to look at them until later today:

test_list3 = assert \ [3,1] < [3,2]

reverse :: List a -> List a
reverse l = fold (flip (:)) [] l

succ x = x + 1

range x y = if x > y then [] else x : range (succ x) y

test_list5 = assert \ range 1 3 == reverse [3,2,1]

:-Dylan

Geoffrey Irving

unread,
Aug 30, 2009, 10:45:01 AM8/30/09
to Geoffrey Irving, duck...@googlegroups.com
On Sun, Aug 30, 2009 at 10:37 AM, Dylan Alex
Simon<dylan-...@dylex.net> wrote:
>
>> > 2. Makes programs that were previously incomplete (e.g., a "case ... of"
>> > ? somewhere deeply nested for which the cases had not yet been filled in)
>> > ? possibly valid, and possibly in unintentional ways. ?It also lets you, for
>> > ? example, make it impossible to get back to a certain context (even the top
>> > ? level) if a nested level has taken it over.
>>
>> I think this does make it too easy to take over the toplevel context,
>> which would result in weird error messages.  It essentially makes
>> layout strongly nonlocal.
>
> We could explicitly disallow replacing a column-1 context.  Though, I think:
>
>  main = do
>  ...
>
> seems potentially useful, even.

I think treating column 1 specially is bad. If we think that main
thing is useful, an alternative would be to allow implicit ';' within
explicit '{ }'.

>> Can you describe the messy one?  The first option that comes to mind
>> is "nested contexts must be more indented than their parents unless
>> the parent started on the previous line."
>
> Yeah, that's basically it.  It comes down to this: Implicit is amended and the
> "top" function is changed so that, if the top Implicit context has never been
> used to insert a ';', then it is skipped and recurses to the next down context
> to determine the "top" column.  So, if the outermost context is implicit,
> you'd never be able to take it over (except in the first line).

That sounds good.

>> > We still aren't implementing Note 5 of the haskell rules, it seems, so this
>> > doesn't work with the in:
>> >
>> > ?f x = let y = case x of z -> z in y
>> >
>> > But that's an orthogonal issue that will be more important for lets
>> > themselves.
>>
>> Yeah, that's why I didn't implement it; I realized it was important
>> only for lets.  It's trivial to add to the parser (just allow "error"
>> in place of '}'), but I'm not sure if it requires a change the layout
>> pass itself.
>
> I don't completely get this.  Every rule including '{' '}' needs to be
> changed?  It is still useful with what we have now, in my code above for
> example.

Yes, every occurrence of '}' has to be changed, but that isn't difficult:

http://www.haskell.org/happy/doc/html/sec-error.html

> By the way, my most recent commit adds more functions in base.duck and tests
> in base-test.duck.  Some of the lines are commented out, as they seem to
> expose as many as four separate bugs (at least one of which is mine), but I
> probably won't have time to look at them until later today:
>
>  test_list3 = assert \ [3,1] < [3,2]
>
>  reverse :: List a -> List a
>  reverse l = fold (flip (:)) [] l
>
>  succ x = x + 1
>
>  range x y = if x > y then [] else x : range (succ x) y
>
>  test_list5 = assert \ range 1 3 == reverse [3,2,1]

I'm looking at them now. The first thing I have to do is fix
typeMismatch to be more specific, since one of them says

type mismatch: 'Int' vs 'Void'

I think I'll go with

type mismatch: 'a' != 'b'
type mismatch: 'a' union 'b'
type mismatch: 'a' intersect 'b'

until we find something better.

Geoffrey

Reply all
Reply to author
Forward
0 new messages