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.
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.
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.
Jason Dagit 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.
+1
Erik
-- ----------------------------------------------------------------------
Erik de Castro Lopo
http://www.mega-nerd.com/
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.
On 21 Oct 2012, at 23:33, Erik de Castro Lopo <mle...@mega-nerd.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.
> +1
> Erik
> -- > ----------------------------------------------------------------------
> Erik de Castro Lopo
> http://www.mega-nerd.com/
On Sun, Oct 21, 2012 at 3:40 PM, Edwin Brady <edwin.br...@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.
> On 21 Oct 2012, at 23:33, Erik de Castro Lopo <mle...@mega-nerd.com>
> wrote:
> > Jason Dagit 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.
> > +1
> > Erik
> > --
> > ----------------------------------------------------------------------
> > Erik de Castro Lopo
> > http://www.mega-nerd.com/
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… ;))
On Mon, Oct 22, 2012 at 7:21 AM, Edwin Brady <edwin.br...@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… ;))
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
On Mon, Oct 22, 2012 at 6:47 PM, Jason Dagit <dag...@gmail.com> wrote:
> On Mon, Oct 22, 2012 at 7:21 AM, Edwin Brady <edwin.br...@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… ;))
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 :)).
On 25 Oct 2012, at 06:25, Carter Schonwald <carter.schonw...@gmail.com> wrote:
> 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
> On Mon, Oct 22, 2012 at 6:47 PM, Jason Dagit <dag...@gmail.com> wrote:
> On Mon, Oct 22, 2012 at 7:21 AM, Edwin Brady <edwin.br...@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… ;))
