/home/laney/.irssi/irclogs/Freenode/#agda.log-20170228

--- Day changed Mon Feb 27 2017
wedifyholy moly i thought i was finally ready to published my dependently typed chess expressions library only to just now realize i haven't done anything to enforce the king not being in check when it ends its move27/02 01:54
wedifythat adds a ton more work27/02 01:54
wedifyi like how the holes give a concrete feel to progress. 'ok i have ten problems now' 'now eight' 'now twelve'27/02 02:34
{AS}wedify: you also need to ensure that you can not put the king in check if you move another piece 27/02 08:58
{AS}Like if you guard your king with a rook against an attacking piece, then you can not move the rook27/02 08:58
{AS}wedify: do you also support castling and en passant? 27/02 09:00
akrAC : ∀ {A B : Set} → {P : A → B → Set} → (∀ a → Σ[ b ∈ B ] P a b) → Σ[ f ∈ (A → B) ] (∀ a → P a (f a))27/02 09:48
akrdoes that seem okay? there also seems to be a dependent version I found here: http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Libraries.SomeCombinators27/02 09:48
akralso, can I postulate the extensional version and derive LEM without too much work? :)27/02 09:50
akrthat should basically be the Diaconescu's theorem, which seems nontrivial27/02 09:51
{AS}akr: Diaconescu's theorem only works for constructive _set_ theory27/02 09:54
{AS}not constructive type theory27/02 09:54
akroh, so I can't do it in Agda, unless I first formalise constructive set theory or something?27/02 09:54
{AS}akr: Yeah27/02 09:55
{AS}I mean if you could derive LEM it would be unsound 27/02 09:55
akrhmm, wait, so you're saying I can't even state the extensional choice in Agda?27/02 09:56
akras in, postulate27/02 09:56
{AS}akr: hmm27/02 09:56
{AS}how would you postulate it?27/02 09:57
akrI'm not sure :) but we have setoids…27/02 09:57
akrhttp://r6.ca/blog/20050604T143800Z.html27/02 09:57
{AS}akr: I mean you can use the classical existential instead of the constructive one27/02 09:58
{AS}but then you introduce a classical construct already27/02 09:58
{AS}In any case, my point is that if you want lem, just postulate it27/02 09:58
akroh, that reminds me: how do you define classical ∀ and ∃ in Agda?27/02 09:59
{AS}akr: classical is the same as constructive for forall27/02 09:59
akr{AS}: I don't want LEM, I'm just playing with these things :)27/02 09:59
akr{AS}: oh, so the classical ∃ϕ is ¬∀¬ϕ?27/02 10:00
{AS}akr: yeah27/02 10:00
akrI don't see why ∀ is the same between classical and constructive though, where should I look for an explanation?27/02 10:01
akror is it obvious somehow? :)27/02 10:03
{AS}akr: I think it has something to do with elimination forms27/02 10:04
{AS}I am unsure the precise reason27/02 10:04
akrI see, so I'd have to look into MLTT27/02 10:05
akrone of these days… :)27/02 10:05
akr{AS}: thank you, I have to go now27/02 10:05
{AS} OK, bye27/02 10:05
aphorismeWhen checking a dependent type, should I evaluate to NF first?27/02 12:27
{AS}aphorisme: usually WHNF is used27/02 12:40
aphorisme{AS}: so I go recursively down the type? Since, when evaluating, I should type check it first, or?27/02 12:41
{AS}aphorisme: you would type check the type before the values yes27/02 12:41
{AS}aphorisme: you might consider https://github.com/sweirich/pi-forall27/02 12:41
aphorismeAh!27/02 12:42
aphorismeNice.27/02 12:42
aphorismeThanks, {AS}.27/02 12:42
{AS}np! :)27/02 12:42
wedify{AS}: that's a good one. i didn't think of that. i support castling but not en passant. i will though, one step at a time27/02 20:41
wedifyit's neat how programming this forces me to make explicit all sorts of things that i take for granted27/02 20:42

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