"total" vs. "partial"

[Jason Dagit]

I like that Idris allows us to require definitions to be total by using the "total" keyword. But, I'm thinking that perhaps we have the default the wrong way around. It seems that "partial" might be a better keyword.

Here is my thinking on this:

  * As libraries are developed in Idris and I use them there will probably be many places where I wish I could be sure that everything I'm calling is total. Seeing "partial" at the definition site would tip me off better than the absence of "total".

  * If total is the default, I believe more people will prefer it and subtle bugs where totality was intended but accidentally left out will be caught. If I recall correctly, this sort of bug has already happened once in the Idris standard library.

  * I think most of us will want to make total definitions, and having it has the default means we get the machine checking with fewer keywords in our source.

Basically, I think making totality an "opt out" instead of an "opt in" option will encourage people to write total definitions while still allowing for partial definitions.

Thoughts?

Jason

[Arthur Peters]

I agree. I wrote some "proofs" that were not proofs at all because I forgot totality checking. I'm new to this stuff, so it's an easy mistake to make. So it does seem like something that would avoid newbie mistakes if it were default. Especially since a keyword is not needed in Agda or Coq.

Just my 2 cents.
-Arthur

[Erik de Castro Lopo]

+1

Erik
--
----------------------------------------------------------------------
Erik de Castro Lopo
http://www.mega-nerd.com/

[Edwin Brady]

In principle, I think this is a good idea. As well as helping you know your functions actually work, totality helps make them fast (some optimisations depend on it). However there are a couple of reasons I've gone the other way for the moment:

* The totality checker isn't very good (it was just an afternoon hack, but it's quite high on the list of things to fix)
* It would be nice to have a good story about coinduction first. Or any story.

Perhaps the thing to do is make this configurable, then at some future time the default can be easily switched.

Edwin.

[Jason Dagit]

On Sun, Oct 21, 2012 at 3:40 PM, Edwin Brady <edwin...@gmail.com> wrote:

In principle, I think this is a good idea. As well as helping you know your functions actually work, totality helps make them fast (some optimisations depend on it). However there are a couple of reasons I've gone the other way for the moment:

* The totality checker isn't very good (it was just an afternoon hack, but it's quite high on the list of things to fix)
* It would be nice to have a good story about coinduction first. Or any story.

Perhaps the thing to do is make this configurable, then at some future time the default can be easily switched.

It sounds like most people would like the default switched so what if we look at the problem you mentioned in a different way. Does switching the default make it harder for you to work on these things?

What I'm getting at: If users are having trouble with the totality checker they could, for now, specify things to be partial more frequently than they would if the totality checker worked as you wished (and we had a coinduction story). But only if that wouldn't interfere with improving the checker.

Perhaps changing the default would give you additional motivation to work on the things you mentioned? Once the totality checker is better, the spurious partials could be removed?

Just some thoughts. No pressure. I wish I could help more, but I feel like I'm still struggling to learn the basics of type theory.

[Edwin Brady]

On 22 Oct 2012, at 00:18, Jason Dagit <dag...@gmail.com> wrote:

> It sounds like most people would like the default switched so what if we look at the problem you mentioned in a different way. Does switching the default make it harder for you to work on these things?

Well, most from a sample size of 3 :). But still…

I have added a "partial" keyword and a "%default" directive. So you can now say "%default total" and mark functions as "partial" to get the behaviour you want.

I have also added command line flags "--total" for total-by-default, and "--partial"
for partial-by-default (which is the current behaviour).

I'll keep it partial by default until the totality checker is better.

> What I'm getting at: If users are having trouble with the totality checker they could, for now, specify things to be partial more frequently than they would if the totality checker worked as you wished (and we had a coinduction story). But only if that wouldn't interfere with improving the checker.
>
> Perhaps changing the default would give you additional motivation to work on the things you mentioned? Once the totality checker is better, the spurious partials could be removed?

I don't need additional motivation to make things better. Just additional time and/or resources! (As if this is not the same for everyone… ;))

Edwin.

[Jason Dagit]

On Mon, Oct 22, 2012 at 7:21 AM, Edwin Brady <edwin...@gmail.com> wrote:

On 22 Oct 2012, at 00:18, Jason Dagit <dag...@gmail.com> wrote:

> It sounds like most people would like the default switched so what if we look at the problem you mentioned in a different way. Does switching the default make it harder for you to work on these things?

Well, most from a sample size of 3 :). But still…

Isn't that how it works? 1 or 2 and you just have some data points, but 3 means you should generalize :)

I have added a "partial" keyword and a "%default" directive. So you can now say "%default total" and mark functions as "partial" to get the behaviour you want.

I have also added command line flags "--total" for total-by-default, and "--partial"
for partial-by-default (which is the current behaviour).

Thanks!

 

I'll keep it partial by default until the totality checker is better.

Okay.

I don't need additional motivation to make things better. Just additional time and/or resources! (As if this is not the same for everyone… ;))

That's fair. Thanks for add this new feature.

Jason

[Carter Schonwald]

I hope to find time to dig into the totality checker piece.... depends on how a bunch of dust settles on some work matters in the next week or two, i'll be hassling y'all with questions about that 

[Edwin Brady]

Hi Carter,
That'd be great! I'm playing around with size-change termination at the minute - it computes some simple size change graphs just by looking at structure, but doesn't do anything clever. So that should improve things soon. If you're interested in improving it, hopefully that would be a good starting point for you.

Edwin (who is not in any way an expert on this corner of language implementation :)).