Logs: freenode/#haskell
| 2020-10-16 16:12:49 | → | Deide joins (~Deide@217.155.19.23) |
| 2020-10-16 16:13:00 | → | LKoen joins (~LKoen@81.255.219.130) |
| 2020-10-16 16:13:03 | <blip> | non-natural |
| 2020-10-16 16:13:36 | <solonarv> | you can of course define type-level integers or rationals yourself, you just won't get nice syntax where you just write down a numeric literal |
| 2020-10-16 16:13:42 | <dolio> | Monads (and similar stuff) are useful for many things that are not directly related to 'purity'. |
| 2020-10-16 16:14:01 | <davean> | I mean you can create a TDouble Nat Nat, but defining rules for it will be "fun" |
| 2020-10-16 16:14:03 | <blip> | solonarv: yes, but that get's ugly fast |
| 2020-10-16 16:14:58 | <kuribas> | blip: I think because Naturals are used for array indexing, one of the main usecases for typelevel numbers, but Double is much less handy. |
| 2020-10-16 16:15:37 | <blip> | Well, but negatives can be nicely used for physical dimensions for example. |
| 2020-10-16 16:15:55 | <davean> | what physical dimensions can be negative? |
| 2020-10-16 16:16:03 | <davean> | weight can't be, length can't be ... |
| 2020-10-16 16:16:03 | × | gxt quits (~gxt@gateway/tor-sasl/gxt) (Ping timeout: 240 seconds) |
| 2020-10-16 16:16:21 | <kuribas> | blip: how do you use physical dimensions on type level? |
| 2020-10-16 16:16:47 | <blip> | davean: length can be, for example 5 s/m |
| 2020-10-16 16:17:04 | <davean> | blip: Theres no negative there |
| 2020-10-16 16:17:16 | <blip> | davean: yes, there are |
| 2020-10-16 16:17:18 | <davean> | kuribas: Oh thats easy, you often want to run a program for a specific case, so you pass parameterize at the type level by the static information |
| 2020-10-16 16:17:29 | <blip> | m^(-1) |
| 2020-10-16 16:17:40 | <davean> | no, theres no negative there, theres a m^-1 |
| 2020-10-16 16:17:44 | <davean> | but thats not a negative value |
| 2020-10-16 16:17:53 | <kuribas> | davean: I don't get it |
| 2020-10-16 16:17:54 | <davean> | Which is a very important thing to realize |
| 2020-10-16 16:17:58 | <blip> | well, -1 looks negative to me |
| 2020-10-16 16:18:44 | → | gxt joins (~gxt@gateway/tor-sasl/gxt) |
| 2020-10-16 16:19:11 | <blip> | 60 :: Meter^1 * Second^(-1) |
| 2020-10-16 16:19:13 | × | nineonin_ quits (~nineonine@216-19-190-182.dyn.novuscom.net) (Remote host closed the connection) |
| 2020-10-16 16:19:49 | → | nineonine joins (~nineonine@50.216.62.2) |
| 2020-10-16 16:20:18 | <davean> | blip: its a negative exponent, but not a negative value, it produces a unit and the value of the unit isn't negative. You can choose to talk about it as an exponent, or directly what it is |
| 2020-10-16 16:20:31 | <davean> | The negativeness there is just notation for the unit |
| 2020-10-16 16:21:44 | <davean> | in the same sense that subtraction isn't a negative number |
| 2020-10-16 16:22:01 | → | Wamanuz joins (~wamanuz@78-70-34-81-no84.tbcn.telia.com) |
| 2020-10-16 16:22:43 | × | dhouthoo quits (~dhouthoo@ptr-eiv6509pb4ifhdr9lsd.18120a2.ip6.access.telenet.be) (Quit: WeeChat 2.9) |
| 2020-10-16 16:23:01 | <solonarv> | right, and if you want to write down the negative exponent on the type level, you need negative type-level integers |
| 2020-10-16 16:23:02 | → | heatsink joins (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) |
| 2020-10-16 16:23:02 | <kuribas> | blip: I am missing the explanation why this would be interesting *at type level*. |
| 2020-10-16 16:23:17 | <solonarv> | I do think blip's notation is sensible and desirable |
| 2020-10-16 16:23:31 | <blip> | kuribas: you could avoid adding seconds to meters for example |
| 2020-10-16 16:23:39 | → | geekosaur joins (82659a0e@host154-014.vpn.uakron.edu) |
| 2020-10-16 16:23:46 | <solonarv> | putting units/dimensions on the type level lets you make the typechecker do dimensional analysis for you |
| 2020-10-16 16:24:08 | <kuribas> | blip: then you just need a Meter newtype and Seconds newtype. |
| 2020-10-16 16:24:43 | <kuribas> | solonarv: in that case I would just have one canonical type. |
| 2020-10-16 16:25:03 | <solonarv> | now if you want to multiply two Meter values you also need an Area newtype, if you want to divide a Meter value by a Seconds value you need a MeterPerSecond newtype... it's a profusion of newtypes! |
| 2020-10-16 16:25:47 | <blip> | kuribas: how would you possibly implement multiplication |
| 2020-10-16 16:26:01 | <phadej> | https://hackage.haskell.org/package/uom-plugin |
| 2020-10-16 16:26:07 | × | ericsagnes quits (~ericsagne@2405:6580:0:5100:ad7e:a36b:18dd:5e0b) (Ping timeout: 260 seconds) |
| 2020-10-16 16:26:23 | <kuribas> | blip: a Squared type? |
| 2020-10-16 16:26:52 | <kuribas> | like (Squared Meter) |
| 2020-10-16 16:26:55 | × | karanlikmadde quits (~karanlikm@2a01:c23:6037:1800:e990:a27c:f553:f1d1) (Quit: karanlikmadde) |
| 2020-10-16 16:27:17 | <blip> | (:*:) :: (Meter x, Second y, Mass z, ...) -> (Meter x', Second y', Mass z', ...) -> (Meter (x+x'), Second (y+y'), Mass (z + z')...) |
| 2020-10-16 16:27:29 | <solonarv> | and now you need a Cubed type, and you need to figure out division still... |
| 2020-10-16 16:27:30 | <blip> | of any SI-Dimension |
| 2020-10-16 16:27:37 | <solonarv> | there *are* libraries that do this already, mind you |
| 2020-10-16 16:27:48 | <davean> | dimensional for example |
| 2020-10-16 16:27:54 | <davean> | a few others |
| 2020-10-16 16:27:57 | <kuribas> | solonarv: or just... don't? Don't try to encode everything in types? |
| 2020-10-16 16:28:35 | <phadej> | >>> It is traditional here to cite the Mars Climate Orbiter, or the Gimli Glider |
| 2020-10-16 16:28:38 | <phadej> | (http://lamar.colostate.edu/~hillger/unit-mixups.html). |
| 2020-10-16 16:28:48 | <davean> | kuribas: so, for example, if I want to setup a control system, knowing the paraeters staticly let me generate code that optimally performs the control operation for each enumerated case |
| 2020-10-16 16:28:53 | <solonarv> | but this is actually a sensible thing to encode in types. The system of dimensions (or units) *is* a type system already, and it can be embedded into Haskell's type system. |
| 2020-10-16 16:29:17 | <phadej> | solonarv: can, but it can also be painful without compiler support. See uom-plugin paper |
| 2020-10-16 16:30:09 | → | Tuplanolla joins (~Tuplanoll@91-159-68-239.elisa-laajakaista.fi) |
| 2020-10-16 16:30:18 | → | xff0x joins (~fox@217.110.198.158) |
| 2020-10-16 16:31:55 | → | alp joins (~alp@2a01:e0a:58b:4920:d1be:ca38:a451:6036) |
| 2020-10-16 16:32:42 | → | jneira[m] joins (~jneira@191.red-37-10-143.dynamicip.rima-tde.net) |
| 2020-10-16 16:33:22 | <dolio> | 'Dimensional analysis' that physicists talk about is basically type checking. |
| 2020-10-16 16:33:34 | <kuribas> | solonarv: Squared and Cubed sounds ok to me. How many dimension do you really need? Besides, a lot more can go wrong in numerical calculations than wrong dimensions. |
| 2020-10-16 16:34:00 | <blip> | kuribas: up to ^5 |
| 2020-10-16 16:34:06 | <blip> | isn't that uncommon in physics |
| 2020-10-16 16:34:11 | <dolio> | Maybe only physics professors. |
| 2020-10-16 16:34:42 | <solonarv> | even fractional exponents come up sometimes! although admittedly not often |
| 2020-10-16 16:34:49 | <blip> | dimensional analysis: don't do only profs, that's taught in schools |
| 2020-10-16 16:35:27 | <solonarv> | yeah, I was taught DA in high school. We even properly distinguished units from dimensions. |
| 2020-10-16 16:37:18 | <blip> | if my pupils don't do DA, I slap them with a Force of 5 kg :) |
| 2020-10-16 16:37:44 | <blip> | kuribas: so you would use a newtype for Newtons? |
| 2020-10-16 16:38:07 | <kuribas> | blip: possibly? |
| 2020-10-16 16:38:10 | → | chris joins (~chris@81.96.113.213) |
| 2020-10-16 16:38:17 | <blip> | hm |
| 2020-10-16 16:38:23 | <davean> | blip: have you looked at 'dimensional', etc? |
| 2020-10-16 16:38:24 | → | ericsagnes joins (~ericsagne@2405:6580:0:5100:2c71:50df:a168:e256) |
| 2020-10-16 16:38:33 | chris | is now known as Guest68069 |
| 2020-10-16 16:38:40 | <blip> | davean: yes, but I'm using that just as an example |
| 2020-10-16 16:38:45 | <solonarv> | @hackage units - the one I remembered first when this discussion came up |
| 2020-10-16 16:38:46 | <lambdabot> | https://hackage.haskell.org/package/units - the one I remembered first when this discussion came up |
| 2020-10-16 16:39:16 | <blip> | I'm more generally interested in representing more stuff ergonomically at type level |
| 2020-10-16 16:39:25 | <blip> | I'm a bit of a TL fan |
| 2020-10-16 16:39:48 | <solonarv> | type-level (negative) integers and fractions might be within the realm of what a GHC plugin can do |
| 2020-10-16 16:39:48 | × | nados quits (~dan@107-190-41-58.cpe.teksavvy.com) (Read error: Connection reset by peer) |
| 2020-10-16 16:39:58 | × | lnlsn quits (~lnlsn@189.100.212.150) (Read error: Connection reset by peer) |
| 2020-10-16 16:40:01 | <kuribas> | type level, ergonomic and haskell don't really go together |
| 2020-10-16 16:40:08 | <kuribas> | except for simple stuff |
| 2020-10-16 16:40:14 | <blip> | don't be that negative |
| 2020-10-16 16:40:23 | <solonarv> | there is some facility within GHC plugins to add new syntax if it can be cobbled together from existing syntax |
| 2020-10-16 16:40:25 | <davean> | I don't know why you'd use a plugin for it, you can just do it if you want |
| 2020-10-16 16:40:27 | → | nados joins (~dan@107-190-41-58.cpe.teksavvy.com) |
| 2020-10-16 16:40:51 | <davean> | You have to lie and just claim laws, but thats easy |
| 2020-10-16 16:41:21 | <kuribas> | blip: I am not negative. It's nice to have it, but most of it was an afterthought. |
| 2020-10-16 16:41:22 | <blip> | Well, kind-safety is overrated |
| 2020-10-16 16:41:29 | <blip> | yeah |
| 2020-10-16 16:41:41 | <blip> | But it's getting better over time |
| 2020-10-16 16:42:19 | <kuribas> | blip: actually, that's something I miss, well kinded type level computation. For example servant is pretty ad-hoc. |
All times are in UTC.