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
On Sun, Oct 21, 2012 at 5:17 PM, Jason Dagit <dag
...@gmail.com> wrote:
> 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
