Logs: liberachat/#haskell
| 2021-06-30 20:49:33 | → | Reyu[M] joins (~reyureyuz@matrix.reyuzenfold.com) |
| 2021-06-30 20:49:37 | → | nate1 joins (~nate@108-233-125-227.lightspeed.sntcca.sbcglobal.net) |
| 2021-06-30 20:49:54 | × | eggplantade quits (~Eggplanta@2600:1700:bef1:5e10:dc49:b28b:5485:3e7e) (Ping timeout: 240 seconds) |
| 2021-06-30 20:54:50 | × | nate1 quits (~nate@108-233-125-227.lightspeed.sntcca.sbcglobal.net) (Ping timeout: 272 seconds) |
| 2021-06-30 20:55:25 | <Cale> | safinaskar: https://paste.debian.net/1202951/ |
| 2021-06-30 20:55:31 | <Cale> | There's the translation into Coq :) |
| 2021-06-30 20:57:35 | <safinaskar> | Cale: thanks a lot |
| 2021-06-30 20:58:52 | <safinaskar> | Cale: but i have read here: http://coq-blog.clarus.me/gadts-with-type-erasure-in-coq-of-ocaml.html , that this inductive types have not desirable properties |
| 2021-06-30 20:59:36 | × | MQ-17J quits (~MQ-17J@d14-69-206-129.try.wideopenwest.com) (Ping timeout: 258 seconds) |
| 2021-06-30 20:59:53 | → | MQ-17J joins (~MQ-17J@d14-69-206-129.try.wideopenwest.com) |
| 2021-06-30 21:01:54 | <Cale> | That seems to discuss difficulties with compiling OCaml's GADTs into Coq inductive types which might be reasonable concerns for someone writing a compiler that was trying to carefully preserve semantics, but I'm not sure it matters to us. |
| 2021-06-30 21:02:16 | <Cale> | Maybe? |
| 2021-06-30 21:03:52 | × | gehmehgeh quits (~user@user/gehmehgeh) (Quit: Leaving) |
| 2021-06-30 21:04:02 | × | wallymathieu quits (~wallymath@81-234-151-21-no94.tbcn.telia.com) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 2021-06-30 21:04:29 | → | wallymathieu joins (~wallymath@81-234-151-21-no94.tbcn.telia.com) |
| 2021-06-30 21:05:35 | → | mikail joins (~mikail@90.212.77.3) |
| 2021-06-30 21:06:09 | × | mjrosenb quits (~mrosenbe@nyc.schrodinger.com) (Ping timeout: 244 seconds) |
| 2021-06-30 21:06:14 | <safinaskar> | Cale: i want to write functions, which transform proofs from one logic to another. Good exastivness checking is desirable property |
| 2021-06-30 21:06:28 | <Cale> | There is exhaustiveness checking. |
| 2021-06-30 21:06:39 | <Cale> | In fact, there's full termination checking. |
| 2021-06-30 21:07:06 | <safinaskar> | Cale: that article shows that exhaustiveness checking is suboptimal (i mean analysis on case expressions) |
| 2021-06-30 21:08:12 | → | mjrosenb joins (~mrosenbe@104.225.243.2) |
| 2021-06-30 21:08:16 | <Cale> | The situation involving the trees there is not going to come up |
| 2021-06-30 21:08:29 | <Cale> | None of our stuff is parametric on arbitrary types |
| 2021-06-30 21:09:24 | × | wallymathieu quits (~wallymath@81-234-151-21-no94.tbcn.telia.com) (Ping timeout: 272 seconds) |
| 2021-06-30 21:11:12 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 256 seconds) |
| 2021-06-30 21:11:43 | <safinaskar> | Cale: ok |
| 2021-06-30 21:15:02 | × | mikoto-chan quits (~mikoto-ch@ip-213-49-189-31.dsl.scarlet.be) (Ping timeout: 265 seconds) |
| 2021-06-30 21:17:06 | × | Ariakenom quits (~Ariakenom@c83-255-154-140.bredband.tele2.se) (Ping timeout: 240 seconds) |
| 2021-06-30 21:17:14 | × | falafel quits (~falafel@pool-96-255-70-50.washdc.fios.verizon.net) (Ping timeout: 258 seconds) |
| 2021-06-30 21:17:49 | × | warnz quits (~warnz@2600:1700:77c0:5610:409d:bff0:fc58:d5c4) (Remote host closed the connection) |
| 2021-06-30 21:18:33 | → | warnz joins (~warnz@2600:1700:77c0:5610:409d:bff0:fc58:d5c4) |
| 2021-06-30 21:22:18 | <safinaskar> | Cale: do you have a blog? |
| 2021-06-30 21:22:30 | <Cale> | nope |
| 2021-06-30 21:26:59 | → | mikoto-chan joins (~mikoto-ch@ip-213-49-189-31.dsl.scarlet.be) |
| 2021-06-30 21:27:23 | × | fizbin quits (~fizbin@c-73-33-197-160.hsd1.nj.comcast.net) (Remote host closed the connection) |
| 2021-06-30 21:30:28 | × | raehik quits (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) (Ping timeout: 256 seconds) |
| 2021-06-30 21:32:36 | × | dmang quits (~dmang@user/dmang) (Remote host closed the connection) |
| 2021-06-30 21:34:46 | → | raehik joins (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) |
| 2021-06-30 21:36:22 | → | norias joins (~jaredm@c-98-219-195-163.hsd1.pa.comcast.net) |
| 2021-06-30 21:39:32 | × | wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Ping timeout: 256 seconds) |
| 2021-06-30 21:41:21 | <chris_> | hey |
| 2021-06-30 21:41:34 | <chris_> | need help with this function |
| 2021-06-30 21:41:38 | <chris_> | regarding the return type |
| 2021-06-30 21:41:51 | <chris_> | i want it to be [rational] return type |
| 2021-06-30 21:41:55 | → | eggplantade joins (~Eggplanta@2600:1700:bef1:5e10:dc49:b28b:5485:3e7e) |
| 2021-06-30 21:42:15 | <monochrom> | Foo -> [Rational] |
| 2021-06-30 21:42:31 | <chris_> | genDurations :: Int -> [Dur] |
| 2021-06-30 21:42:31 | <chris_> | genDurations n | n < 1 = [] -- edge case |
| 2021-06-30 21:42:31 | <chris_> | genDurations 1 = [1.0] -- recursive stopping point |
| 2021-06-30 21:42:31 | <monochrom> | Perhaps a more complete and informative question. |
| 2021-06-30 21:42:33 | <chris_> | genDurations n = (1/(2**(n-1))) : genDurations (n-1) |
| 2021-06-30 21:42:44 | <chris_> | type Dur = Rational |
| 2021-06-30 21:43:09 | <chris_> | i think the (1/2**n-1))) expression is returning another type |
| 2021-06-30 21:43:19 | <monochrom> | Ah right. Please use ^ |
| 2021-06-30 21:43:32 | <monochrom> | err, ^ is bad too |
| 2021-06-30 21:43:33 | × | mikail quits (~mikail@90.212.77.3) (Ping timeout: 265 seconds) |
| 2021-06-30 21:43:51 | <monochrom> | Please use ^^ |
| 2021-06-30 21:44:25 | × | dunj3 quits (~dunj3@p200300f61714a6405bb7680713e8c72a.dip0.t-ipconnect.de) (Remote host closed the connection) |
| 2021-06-30 21:44:50 | <monochrom> | That reminds me, when I teach number types I need to bring up this ^ ^^ ** business. |
| 2021-06-30 21:45:42 | <chris_> | thx @monochrom that did silent the type errors in vscode |
| 2021-06-30 21:45:43 | → | mikail joins (~mikail@2a02:c7f:bd83:fd00:55cf:122f:957a:f66f) |
| 2021-06-30 21:46:06 | <Cale> | chris_: Also, be careful if you actually wanted 1/2^^(n-1) |
| 2021-06-30 21:46:22 | <Cale> | oh, you did write that in the code |
| 2021-06-30 21:46:29 | <Cale> | just not in the other :) |
| 2021-06-30 21:46:44 | <chris_> | ye my bad, thx |
| 2021-06-30 21:47:35 | <Cale> | x^n gives you exponentiation with only nonnegative integer exponents, but x is allowed to be any sort of number at all (any instance of Num) |
| 2021-06-30 21:48:01 | <Cale> | x^^n allows negative exponents as well, but the type of x must have an instance of Fractional |
| 2021-06-30 21:49:01 | <Cale> | x**y is exponentiation where y and x have the same type, and that type must have an instance of Floating |
| 2021-06-30 21:49:48 | <Cale> | (and it allows basically arbitrary exponents then) |
| 2021-06-30 21:50:16 | <Cale> | Well, there might be restrictions depending on the type of course. |
| 2021-06-30 21:50:18 | × | acidjnk_new quits (~acidjnk@p200300d0c72b954061d05013652ae098.dip0.t-ipconnect.de) (Ping timeout: 256 seconds) |
| 2021-06-30 21:50:18 | → | fizbin joins (~fizbin@c-73-33-197-160.hsd1.nj.comcast.net) |
| 2021-06-30 21:52:07 | ← | safinaskar parts (~safinaska@109-252-90-89.nat.spd-mgts.ru) () |
| 2021-06-30 21:53:44 | × | jao quits (jao@gateway/vpn/protonvpn/jao) (Remote host closed the connection) |
| 2021-06-30 21:54:21 | <ephemient> | given that (**) is on the Floating typeclass, what other restrictions can it apply? |
| 2021-06-30 21:55:00 | × | fendor quits (~fendor@77.119.196.177.wireless.dyn.drei.com) (Remote host closed the connection) |
| 2021-06-30 21:55:00 | × | fizbin quits (~fizbin@c-73-33-197-160.hsd1.nj.comcast.net) (Ping timeout: 272 seconds) |
| 2021-06-30 21:55:53 | <chris_> | what's an Integral (and it's type) |
| 2021-06-30 21:56:00 | <ephemient> | I guess it could be non-total but in practice Float/Double will produce NaN for negative ** fractional |
| 2021-06-30 21:57:01 | <ephemient> | Integral is a typeclass of types that support integer-like operations |
| 2021-06-30 21:57:11 | <ephemient> | % :info Integral |
| 2021-06-30 21:57:12 | <yahb> | ephemient: pattern Integral :: forall {a}. Integral a => a -> Integer -- Defined in `Numeric.Lens'; type Integral :: * -> Constraint; class (Real a, Enum a) => Integral a where; quot :: a -> a -> a; rem :: a -> a -> a; div :: a -> a -> a; mod :: a -> a -> a; quotRem :: a -> a -> (a, a); divMod :: a -> a -> (a, a); toInteger :: a -> Integer; {-# MINIMAL quotRem, toInteger #-}; -- Defined in `GHC.Rea |
| 2021-06-30 21:57:29 | <ephemient> | ... not the right one |
| 2021-06-30 21:57:42 | <monochrom> | (-2) ** (0.5) does not have an answer in the real numbers |
| 2021-06-30 21:57:42 | <ephemient> | % :info Prelude.Integral |
| 2021-06-30 21:57:42 | <yahb> | ephemient: type Integral :: * -> Constraint; class (Real a, Enum a) => Integral a where; quot :: a -> a -> a; rem :: a -> a -> a; div :: a -> a -> a; mod :: a -> a -> a; quotRem :: a -> a -> (a, a); divMod :: a -> a -> (a, a); toInteger :: a -> Integer; {-# MINIMAL quotRem, toInteger #-}; -- Defined in `GHC.Real'; instance Integral Word -- Defined in `GHC.Real'; instance Integral Integer -- Defined in |
| 2021-06-30 21:58:01 | <monochrom> | but it's only checked at run time |
| 2021-06-30 21:58:17 | <monochrom> | but still, you shouldn't do it in the first place. :) |
| 2021-06-30 21:58:24 | <ephemient> | if you extend the reals with NaN then it does have an answer :) |
| 2021-06-30 21:58:40 | <monochrom> | true |
| 2021-06-30 21:58:58 | <ephemient> | of course that causes the annoyance of non-total ordering... oh well |
| 2021-06-30 21:59:46 | → | jao joins (jao@gateway/vpn/protonvpn/jao) |
| 2021-06-30 22:00:13 | × | mikoto-chan quits (~mikoto-ch@ip-213-49-189-31.dsl.scarlet.be) (Quit: mikoto-chan) |
| 2021-06-30 22:00:42 | × | acarrico quits (~acarrico@dhcp-68-142-39-249.greenmountainaccess.net) (Ping timeout: 272 seconds) |
| 2021-06-30 22:00:56 | × | Morrow quits (~MorrowM_@147.161.13.35) (Ping timeout: 252 seconds) |
| 2021-06-30 22:01:54 | <ephemient> | chris_: https://rufflewind.com/2014-08-03/haskell-numeric-type-classes-hierarchy |
| 2021-06-30 22:04:05 | → | tlaxkit joins (~hexchat@170.253.43.19) |
| 2021-06-30 22:04:57 | × | chris_ quits (~chris@81.96.113.213) (Remote host closed the connection) |
| 2021-06-30 22:05:38 | → | chris_ joins (~chris@81.96.113.213) |
All times are in UTC.