Logs: freenode/#haskell
| 2020-11-19 12:06:45 | <dminuoso> | boxscape: Btw, I think there's a mistake in your proof |
| 2020-11-19 12:06:48 | <boxscape> | the error message is better, you're right |
| 2020-11-19 12:06:50 | <boxscape> | dminuoso oh? |
| 2020-11-19 12:06:53 | <dminuoso> | boxscape: plus_Z :: SNat n -> Plus n Z :~: n |
| 2020-11-19 12:06:58 | <dminuoso> | boxscape: Think you mixed up the order to Plus there |
| 2020-11-19 12:07:14 | <dminuoso> | The identity is only on one side in the tyfam |
| 2020-11-19 12:07:26 | <dminuoso> | Or am I confusing things? |
| 2020-11-19 12:07:46 | <boxscape> | dminuoso the identity of Plus Z n = n is trivial, but I have to write this proof to convince ghc that the other direction works, too |
| 2020-11-19 12:08:33 | <dminuoso> | boxscape: Ohh, so `plus_Z SZ = Refl` gives us `Plus Z Z ~ Z` for the base case |
| 2020-11-19 12:08:40 | <boxscape> | right |
| 2020-11-19 12:08:51 | <dminuoso> | (Which evalutaes to Z ~ Z, dischargable because every type is automatically equal to itself) |
| 2020-11-19 12:08:58 | <dminuoso> | So we dont need to provide proof ofZ ~ Z |
| 2020-11-19 12:09:29 | × | cosimone quits (~cosimone@2001:b07:ae5:db26:d849:743b:370b:b3cd) (Quit: cosimone) |
| 2020-11-19 12:09:35 | <boxscape> | I would hope that if there were a mistake ghc would have caught it, otherwise there'd be a bug in ghc (or in my copy-paste abilites) |
| 2020-11-19 12:10:15 | <boxscape> | uh, assuming it's not the sort of mistake that makes a proof non-total |
| 2020-11-19 12:10:34 | <dminuoso> | plus_Z (SS n) | Refl <- plus_Z n = Refl |
| 2020-11-19 12:10:44 | <dminuoso> | How does this inductive step work exaclty from the constraint solvers point of view? |
| 2020-11-19 12:13:17 | <boxscape> | so, if you write plus_Z (SS n), what you have to solve is 'S (Plus n 'Z) :~: 'S n. plus_Z n has type (Plus n Z) :~: n, so by matching on that, we can unify Plus n Z with n, and we have to solve S n :~: S n |
| 2020-11-19 12:13:31 | <boxscape> | and Refl is a value with that type, so we can just write Refl |
| 2020-11-19 12:13:39 | <boxscape> | dminuoso |
| 2020-11-19 12:14:14 | <dminuoso> | "what you have to solve is 'S (Plus n 'Z) :~: 'S n" |
| 2020-11-19 12:14:21 | → | oerjan joins (~oerjan@195.206.169.184) |
| 2020-11-19 12:14:26 | <dminuoso> | do you mean `S (Plus n 'Z) ~ 'S`? |
| 2020-11-19 12:15:06 | <boxscape> | hmm I don't think I do. S by itself isn't a natural number, but S (Plus n Z) is a natural number, so that appears to be a kind error. |
| 2020-11-19 12:15:15 | <dminuoso> | err |
| 2020-11-19 12:15:37 | → | Tario joins (~Tario@201.192.165.173) |
| 2020-11-19 12:16:17 | <boxscape> | ah but |
| 2020-11-19 12:16:23 | <boxscape> | I should have used a different letter |
| 2020-11-19 12:16:32 | <dminuoso> | boxscape: Sorry I think I cut off a quote there. We want to produce a value of type: 'S (Plus n 'Z) :~: 'S n |
| 2020-11-19 12:16:32 | <boxscape> | like S (Plus m 'Z) :~: 'S m |
| 2020-11-19 12:16:42 | <dminuoso> | So we use the data constructor Refl. That requires us to solve for a constraint |
| 2020-11-19 12:16:50 | <dminuoso> | 'S (Plus n 'Z) ~ 'S n |
| 2020-11-19 12:17:26 | <boxscape> | Ah, fair. What I meant by "solve" was "we have to write a value of that type on the rhs", but the terminology was a bit off, I admit |
| 2020-11-19 12:17:59 | <dminuoso> | The pattern matching `Refl <- plus_Z n` uncovers the dictionary for the proof of the inductive hypothesis |
| 2020-11-19 12:18:07 | <boxscape> | right |
| 2020-11-19 12:18:30 | <dminuoso> | And from that we can show that (Plus n 'Z) ~ n |
| 2020-11-19 12:18:36 | <dminuoso> | (or GHC can) |
| 2020-11-19 12:18:42 | <dminuoso> | Thus leading us to conclude that |
| 2020-11-19 12:18:50 | <dminuoso> | 'S n ~ 'S n |
| 2020-11-19 12:18:52 | × | alp quits (~alp@2a01:e0a:58b:4920:7900:a63:b56e:5a9) (Ping timeout: 260 seconds) |
| 2020-11-19 12:19:08 | <boxscape> | yeah, that sounds right |
| 2020-11-19 12:19:08 | <dminuoso> | which is what Refl demands |
| 2020-11-19 12:19:18 | <dminuoso> | mmm okay |
| 2020-11-19 12:19:43 | → | heatsink joins (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) |
| 2020-11-19 12:20:02 | <dminuoso> | So the value here of :~: is that we can have it in *positive* position, such that things can *produce* proofs of this |
| 2020-11-19 12:20:12 | <dminuoso> | Whereas with => its, in effect, in negative position |
| 2020-11-19 12:20:15 | → | alp joins (~alp@2a01:e0a:58b:4920:7562:27bf:89c5:b0d) |
| 2020-11-19 12:20:18 | → | enoq joins (~textual@194-208-146-143.lampert.tv) |
| 2020-11-19 12:20:24 | <boxscape> | right |
| 2020-11-19 12:22:27 | → | Entertainment joins (~entertain@104.246.132.210) |
| 2020-11-19 12:22:51 | <dminuoso> | actually I missed one step! |
| 2020-11-19 12:22:57 | <dminuoso> | 13:18:42 dminuoso | Thus leading us to conclude that |
| 2020-11-19 12:23:15 | <dminuoso> | This requires injectivity of 'S |
| 2020-11-19 12:23:36 | <dminuoso> | Or.. mmm |
| 2020-11-19 12:23:48 | <boxscape> | I think any function would do |
| 2020-11-19 12:24:03 | <boxscape> | going the other way around would though |
| 2020-11-19 12:24:18 | × | noctux quits (~noctux@unaffiliated/noctux) (Remote host closed the connection) |
| 2020-11-19 12:24:18 | <dminuoso> | I should really reimplement the type system myself to get an idea |
| 2020-11-19 12:24:23 | × | heatsink quits (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) (Ping timeout: 256 seconds) |
| 2020-11-19 12:24:37 | × | xacktm quits (xacktm@gateway/shell/panicbnc/x-wtuwnbsvfqpgvaqk) (Quit: PanicBNC - http://PanicBNC.net) |
| 2020-11-19 12:24:47 | <dminuoso> | It's a bit mysterous what we can do with this though |
| 2020-11-19 12:25:17 | <dminuoso> | Surely the value is not to prove commutativity of peano naturals to ourselves, using GHC. |
| 2020-11-19 12:25:29 | → | noctux joins (~noctux@unaffiliated/noctux) |
| 2020-11-19 12:25:43 | <boxscape> | dminuoso the value is in using this proof for value level functions, let me see if I can think of a good example |
| 2020-11-19 12:26:01 | × | Kaiepi quits (~Kaiepi@nwcsnbsc03w-47-55-225-82.dhcp-dynamic.fibreop.nb.bellaliant.net) (Ping timeout: 264 seconds) |
| 2020-11-19 12:26:01 | → | Kaeipi joins (~Kaiepi@nwcsnbsc03w-47-55-225-82.dhcp-dynamic.fibreop.nb.bellaliant.net) |
| 2020-11-19 12:26:13 | → | invaser joins (~Thunderbi@31.148.23.125) |
| 2020-11-19 12:28:16 | <boxscape> | dminuoso hmm for example you could use it to prove things about other value level functions, like if you wanted to prove that (<>) :: Vec n a -> Vec m a -> Vec (Plus n m) a is associative, you would need associativity of Plus first |
| 2020-11-19 12:28:52 | × | ArsenArsen quits (~Arsen@fsf/member/ArsenArsen) (Quit: bye) |
| 2020-11-19 12:29:13 | → | ArsenArsen joins (~Arsen@fsf/member/ArsenArsen) |
| 2020-11-19 12:29:13 | <boxscape> | dminuoso but it can also be useful for writing some regular type-level functions with complex types without explicitly trying to prove something about them, can't quite think of an example of that right now though |
| 2020-11-19 12:30:03 | <dminuoso> | boxscape: Well but whats the value of *proving* this to GHC? |
| 2020-11-19 12:30:16 | <dminuoso> | I mean providing a proof seems only useful if there's something demanding that proof |
| 2020-11-19 12:30:47 | <__monty__> | Certified libraries? |
| 2020-11-19 12:30:54 | <boxscape> | Right, that's what I meant with the example I can't think of right now :) Though I would say a proof is also useful to convice yourself that the function you wrote is correct |
| 2020-11-19 12:30:59 | × | Entertainment quits (~entertain@104.246.132.210) () |
| 2020-11-19 12:32:25 | → | Entertainment joins (~entertain@104.246.132.210) |
| 2020-11-19 12:32:40 | <boxscape> | dminuoso also when I wrote "regular type-level functions" I mean "regular value-level functions" |
| 2020-11-19 12:37:07 | → | p0a joins (~user@unaffiliated/p0a) |
| 2020-11-19 12:37:26 | <p0a> | Hello why is this happening to `stack ghci' in every new stack project of mine? https://pastebin.com/SHVA1zET |
| 2020-11-19 12:39:07 | <__monty__> | p0a: Looks like the same filename in a lib and an executable? Not sure why it's a problem though. |
| 2020-11-19 12:39:26 | <__monty__> | Is the fully qualified name identical? |
| 2020-11-19 12:39:47 | <p0a> | I don't know how to check whta you're asking me __monty__ |
| 2020-11-19 12:39:58 | <merijn> | Who was asking about languages for low level/embedded stuff yesterday? I realised I forgot to mention a totally obvious candidate.. |
| 2020-11-19 12:40:21 | <p0a> | __monty__: what lib has the same filename as an executable? |
| 2020-11-19 12:40:40 | <p0a> | merijn: texasny-something I believe |
| 2020-11-19 12:40:54 | <__monty__> | p0a: Paths_read_binfiles |
| 2020-11-19 12:41:28 | <__monty__> | I think the problem is the module identifiers are identical and GHC doesn't know which one to pick. |
| 2020-11-19 12:41:28 | <p0a> | __monty__: I don't know if it's a problem but `stack ghci' has some weird modules loaded |
| 2020-11-19 12:41:36 | <p0a> | who decided on these names __monty__ ? |
| 2020-11-19 12:41:47 | <__monty__> | Don't know. |
| 2020-11-19 12:42:08 | <__monty__> | @hackage read-binfiles |
| 2020-11-19 12:42:08 | <lambdabot> | https://hackage.haskell.org/package/read-binfiles |
| 2020-11-19 12:42:10 | <merijn> | Paths_ modules are autogenerated by Cabal to access datafiles |
| 2020-11-19 12:42:18 | <p0a> | It happens to all my new projects __monty__ |
| 2020-11-19 12:43:13 | <merijn> | Make an issue on the stack github? Presumably they'll know how to debug what's going on |
| 2020-11-19 12:43:29 | <p0a> | ok wanted to make sure it's not something obvious |
| 2020-11-19 12:44:09 | → | mputz joins (~Thunderbi@dslb-084-058-211-084.084.058.pools.vodafone-ip.de) |
| 2020-11-19 12:45:49 | <merijn> | It might be, but I don't use stack, so who knows :p |
| 2020-11-19 12:47:59 | <boxscape> | dminuoso I ran into an example yesterday where I did need a proof, though not an equality proof, and it was on the type level, but I think should work equally well on the value level: Let's say you have an ordered list, where the cons constructor carries a proof that a cons'd element is less than the next element in the list (thus making sure it |
All times are in UTC.