erisco 2017-02-04 21:48:18
GHC doesn't yet support impredicative polymorphism
erisco 2017-02-04 21:56:20
one solution would be to carry the SingI context around everywhere... but that would be rather burdensome
erisco 2017-02-04 21:58:06
it is sort of strange because Haskell whines there are two SingI instances for Nat
erisco 2017-02-04 21:58:38
but then there are exactly two cases for Nat
erisco 2017-02-04 21:59:21
I dunno, maybe the underlying implementation just wouldn't work
erisco 2017-02-04 22:11:09
ah ha, I figured out something that seems good
erisco 2017-02-04 22:13:29
I worked my way to the grand proof of (a :<= b) := ((a :< b) :\/ (a := b)) lol
nilof_ 2017-02-04 22:20:08
...The minesweep clear operation is a rather interesting problem to solve without mutation
Axman6 2017-02-04 22:26:13
how so? a nieve implementation involves just iterating a set of coordinates and their empty neighbours until the set doesn;t change
nilof_ 2017-02-04 22:27:31
Yes, but it's easy to make it behave badly asymptotically
Axman6 2017-02-04 22:28:26
how big di you plan to make you games? =)
nilof_ 2017-02-04 22:29:09
well, I would like a 50 x 50 grid to be possible
Axman6 2017-02-04 22:29:40
doesn't sound too bad
nilof_ 2017-02-04 22:29:41
well, to be fair that shouldn't be too bad
erisco 2017-02-04 22:29:43
computers can eat that for breakfast
nilof_ 2017-02-04 22:30:59
But I'm curious about how to make it perform similarly to the imperative queue & mutable grid approach where you do a breadth first traversal
nilof_ 2017-02-04 22:31:37
I think a lazy data structure is what I need here
Axman6 2017-02-04 22:34:53
might be able to do something efficient using efficient using lazy arrays
Axman6 2017-02-04 22:36:50
tfc: The book you're reading is about as good as it gets
tfc 2017-02-04 22:36:58
Axman6: thx
erisco 2017-02-04 22:42:28
hm, I think type family injectivity might be too conservative
erisco 2017-02-04 22:42:59
http://lpaste.net/352101
