--- Day changed Thu Jul 20 2017
arjen-jonathanHi all; trying to find the state-of-the-art on representing higher-order-state in dep. typed total languages20/07 16:34
arjen-jonathanAny pointers to cool stuff?20/07 16:34
rntzok, I really don't understand why this isn't working: https://gist.github.com/rntz/e154fa36a6022332d061c72c224bfc3920/07 17:43
rntzcan anyone help me understand this instance inference issue I'm having^?20/07 17:44
rntzit seems really simple.20/07 17:45
doliorntz: I don't think it's really simple.20/07 18:45
dolioInferring R = (\a b -> a -> b) from R a b = a -> b is a deceptively simple case of a hard problem.20/07 18:46
dolioI would guess that's where it fails.20/07 18:46
dolioIf _->_ were a thing in itself, rather than something you have to create with a lambda expression, it might work better.20/07 18:48
rntzwell, what's confusing to me is not that it fails, but that it fails in one case but not the other20/07 19:35
rntzwhat's the extra information that's being passed in one case but not the other?20/07 19:35
rntzhm, and I don't *think* it's that _->_ is particularly special - but that is at least testable!20/07 19:36
rntzI'll go try doing it with a different type constructor than -> and see whether it still has the same behavior20/07 19:36
rntzdolio: the choice of _->_ in particular isn't the problem, at least; using Nat and _<=_ or a postulated Set with a relation has the same problem20/07 19:43
rntz(I've updated the gist & tested it in agda 2.5.2)20/07 19:43
dolioWait, it only failed in one case?20/07 19:44
rntzyes!20/07 19:44
rntzfuz works, qux fails20/07 19:44
rntzsee the comments on lines 24 & 2520/07 19:44
rntznow you see my confusion :)20/07 19:45
dolioYeah, I'm not certain about why one works and not the other.20/07 19:47
dolioI mean, using a tuple there is a little bit more cleverness it has to have.20/07 19:49
rntzyes, but it's convenient for the actual, rather larger, use-case I have20/07 19:51
rntzwhere I usually don't destructure the tuple20/07 19:51
rntz(in the larger use case, Transitive becomes "is a category", and the tuple is a category structure)20/07 19:52
rntzwell, is a quiver / set-equipped-with-a-relation / thing that could be a category if it has id & compose & laws, etc.20/07 19:52
dolioIf instead of Data.Product, you use your own inductively defined sigma, does it work?20/07 19:53
dolioI.E. instead of a record sigma?20/07 19:53
rntzoh, hm, using a data instead of a record? it would be weiiird if that made it work, but I can try20/07 19:53
rntzI'd really rather use records, though20/07 19:53
dolioI think it's pretty clever about figuring things out about records, but it's possible the inductive type would be better for something that it's doing.20/07 19:54
rntzno, replacing Data.Product with an inductively defined pair doesn't help: http://sprunge.us/hZXO20/07 19:57
dolioOkay, well, that's good, I guess. :)20/07 19:57
rntzyeah.20/07 19:57

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