[Agda] Problem with inductively defined type having (simulated) partial constructors

[Tristan Wibberley]

On Thu, 2008-04-17 at 21:49 +0100, Wouter Swierstra wrote:

> There are actually two problems with your definition of or. First of,  
> as you noted, there are unresolved constraints. Basically, the proofs  
> that you left implicit in the data type definition are not  
> automatically passed around. This is pretty easy to fix in some cases.  
> Just write:
> 
> (_orone a {p}) or allzeros  = _orone a {p}
> 
> and pass around the proofs by hand. In other cases, such as:
> 
> (a orone) or (b orone) = (a or b) orone
> 
> you will need to prove that "even a" and "even b" implies "even (a or  
> b)".  The proof shouldn't be too hard, but it is a little bit annoying.

Ah-ha!

Thanks, I think I tried everything that was nearly what you said but not
that :)


> The other problem with your code is that it isn't obviously  
> structurally recursive, and therefore doesn't termination check. This  
> surprised me a bit. It seems ok, but maybe I'm missing something here.
> 
> By the way, what are you trying to define. I couldn't quite figure out  
> what the inhabitants of Octet should be just from your code. Perhaps  
> there's an easier way to set things up...

allzeros                                                 === 00000000b
allzeros orone                                           === 00000001b
allzeros orone shifted                                   === 00000010b
allzeros orone shifted orone                             === 00000011b
allzeros orone shifted shifted                           === 00000100b
allzeros orone shifted orone                             === 00000101b
allzeros orone shifted orone shifted                     === 00000110b
allzeros orone shifted orone shifted orone               === 00000111b
allzeros orone shifted shifted shifted                   === 00001000b

etc...

you can't go further than eight bits, you can't shift without at least
one set bit, you can't orone if you've already orone'd without shifting
in between. attempting to shift eight times doesn't result in something
representing 00000000b which is different to allzeros but is impossible
instead.


> Hope this helps,

Very much, thanks.

-- 
Tristan Wibberley

Any opinion expressed is mine (or else I'm playing devils advocate for
the sake of a good argument). My employer had nothing to do with this
communication.