Hey @edwinbrady, is it known whether the Idris 2 elaborator can be cajoled into doing sudoku?
-
-
Replying to @pigworker
I have no idea. That sounds fun. It seems plausible, at least. Suitably evil use of auto implicits might help.
2 replies 0 retweets 5 likes -
Replying to @edwinbrady @pigworker
Backtracking search during type-checking - oh yes!
1 reply 0 retweets 1 like -
Replying to @ozgurakgun @pigworker
That is, to a limited degree, what auto implicits give you. Usually (in the common case of resolving interfaces) they are at least under control but who knows what you might be able to get up to.
1 reply 0 retweets 1 like -
Replying to @edwinbrady @pigworker
(btw you should be able to solve a "valid" sudoku without backtracking search, but it requires quite sophisticated inference. a typical sudoku solver will backtrack. also, this is beside the original point, I realise...)
1 reply 0 retweets 0 likes -
Replying to @ozgurakgun @edwinbrady
The "serious" question is 'what *is* (higher-order) unification in the 1 modality?'.
1 reply 1 retweet 2 likes
Idris 2 currently does the linearity checking in a separate pass, mostly because I don't know the answer to that question. I would love to know, because it would enable all sorts of nice things in the elaborator, especially relating to proof search.
Loading seems to be taking a while.
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.