--- Day changed Tue Aug 08 2017
rntzjonsterling: yeah, that's what I figured08/08 14:02
rntzsuppose I define (or : bool -> bool -> bool) by:08/08 14:03
rntzor true _ = true08/08 14:03
rntzor _ true = true08/08 14:03
rntzor false false = false08/08 14:03
rntzin typechecking, agda will reduce (or true a) to true, but not (or a true) to true08/08 14:10
rntzis there a justification for this?08/08 14:10
rntzfull example: http://sprunge.us/EaaB08/08 14:11
rntzif agda had to be call-by-value, I'd understand, but since it's total...08/08 14:12
adamserntz: I've seen similar question on the mailing list with some discussions I think, maybe have a search there08/08 14:28
jonsterlingI don't know exactly what the semantics of pattern matching are in Agda. If you looked at these as uses of eliminators, then it would make sense why the second reduction does occur.08/08 14:47
rntzjonsterling: you mean, why it does not occur?08/08 14:48
jonsterlingoops yes08/08 14:48
rntzhokay.08/08 14:48
jonsterlingI think ultimately such a reduction would destroy an important property of agda like subject reduction or something.08/08 14:48
jonsterlingbecause, consider the case where the wildcarded pattern was for an empty type.08/08 14:49
jonsterlingi think this would let you establish false judgments in an inconsistent context.08/08 14:50
rntz... doesn't agda already let you do that?08/08 14:51
jonsterlingno08/08 14:51
rntzwhat do you mean by "establish false judgments in an inconsistent context"?08/08 14:51
jonsterlingThat would be like being able to show that "x:Void |- 4 : string"08/08 14:51
rntzah, I see.08/08 14:52
jonsterlingwe can actually do that in certain semantic type theories, but it's not supposed to happen in ITT08/08 14:52
rntzyes, that would not be how I think about agda08/08 14:52
rntzok, but now I'm not clear how wildcard-ing away an inhabitant of Void would let you do that08/08 14:52
jonsterlingI'm not certain, it was an intuitive guess ;-) One would have to think a bit to see if that really applies.08/08 14:53
rntzah, hm.08/08 14:53
rntzwell, it's definitely plausible to me that there's some metatheoretic property that you lose if you do the naive thing08/08 14:54
jonsterlingIt might not... but it seems like the sort of thing that could go wrong, esp. if you are working with a dependent function type.08/08 14:54
rntzyeah, with dependent types especially08/08 14:54
rntzmy example is a nice little perfectly symmetric case :P08/08 14:54
jonsterlingyeah! Nice thing about nuprl is that those judgmental equalities do hold; but the sad thing is you have to prove them :(08/08 14:55
byorgeyrntz: I suppose for your definition of 'or' to do what you want, there would have to some some check that the clauses are consistent08/08 16:29
byorgeyfor example, consider    foo true _ = true; foo _ true = false; foo _ _ = false08/08 16:30
byorgeyyou certainly wouldn't want   foo a true  to reduce to false in this case, because what if a turns out to be true?08/08 16:30
dolioThere are some old epigram threads about this, too.08/08 16:30
dolioMost stuff I recall is more explaining why it's not easy to add, rather than a way of adding it, though.08/08 16:33

Generated by irclog2html.py 2.7 by Marius Gedminas - find it at mg.pov.lt!