Logs: freenode/#haskell
| 2021-03-31 23:30:31 | <lambdabot> | Defined. |
| 2021-03-31 23:30:35 | × | yunusaydin quits (4eb8266d@78.184.38.109) (Quit: Connection closed) |
| 2021-03-31 23:30:37 | <dmwit> | > pointless' 10 |
| 2021-03-31 23:30:39 | <lambdabot> | [1,10,45,120,210,252,210,120,45,10,1] |
| 2021-03-31 23:30:47 | <dmwit> | yay! |
| 2021-03-31 23:31:00 | <larryba> | dmwit, does that relate to haskell in any way? using dependent types for fixed length arrays |
| 2021-03-31 23:31:58 | <dmwit> | ...what? |
| 2021-03-31 23:32:25 | <larryba> | s/dmwit/hpc |
| 2021-03-31 23:33:02 | → | tromp joins (~tromp@dhcp-077-249-230-040.chello.nl) |
| 2021-03-31 23:33:03 | <hpc> | someday, yes |
| 2021-03-31 23:33:19 | <hpc> | i considered explaining the current methods, but figured it was cleaner to point straight to the end goal |
| 2021-03-31 23:33:39 | <hpc> | then when they come back they have a better frame of reference for data kinds and whatnot |
| 2021-03-31 23:33:58 | <larryba> | seems like a waste of time for someone who is just trying to learn haskell, which is the impression I got |
| 2021-03-31 23:34:03 | <hpc> | ghc is eventually getting full dependent types |
| 2021-03-31 23:34:20 | <hpc> | yeah, i clarified first and it was academic curiosity |
| 2021-03-31 23:35:13 | × | molehillish quits (~molehilli@2600:8800:8d06:1800:49e2:dd02:cb68:846) (Ping timeout: 250 seconds) |
| 2021-03-31 23:35:27 | → | ezrakilty joins (~ezrakilty@97-126-95-37.tukw.qwest.net) |
| 2021-03-31 23:35:36 | <dmwit> | For what it's worth, I found the whole singletons thing much easier to follow once I had seen the dependent types version. |
| 2021-03-31 23:36:12 | <dmwit> | So even if you just want to learn how to do this kind of thing in today's Haskell it may not be a waste of time. |
| 2021-03-31 23:37:11 | × | tromp quits (~tromp@dhcp-077-249-230-040.chello.nl) (Ping timeout: 240 seconds) |
| 2021-03-31 23:37:22 | <larryba> | when someone new to haskell asks for fixed-length list, I think they are thinking more in terms of int array[20];, not dependent types in idris |
| 2021-03-31 23:37:30 | <dmwit> | Although reading back, another answer I would consider giving in this situation is `data ListOfLength7 a = ListOfLength7 a a a a a a a`. =P |
| 2021-03-31 23:37:58 | <dmwit> | Well, see, `int array[20]` is a really interesting declaration. This property is not actually checked by the compiler. |
| 2021-03-31 23:38:35 | <dmwit> | e.g. if you write `void foo(int array[20]); int bar[7];`, then `foo(bar)` is "well-typed" according to the C compiler. |
| 2021-03-31 23:38:38 | <larryba> | dmwit, it certainly is. sizeof array, which is evaluated at compile time, returns sizeof(int) * 20 |
| 2021-03-31 23:38:48 | <pjb> | or something like: data ListOfLength n a = a ListOfLength (n-1) a ; ListOfLength 0 a = () -- ? |
| 2021-03-31 23:38:59 | <hpc> | int array[20] is more like foo :: Array a; foo = newEmptyArray 20 |
| 2021-03-31 23:39:17 | <hpc> | because when you write your functions that operate on that array, the type signature is int[], not int[20] |
| 2021-03-31 23:39:46 | <dmwit> | pjb: That kind of thing is cromulent with dependent types, but not with plain Haskell. (There is a variant that works in today's GHC-based Haskell, but it's much more verbose.) |
| 2021-03-31 23:39:57 | <pjb> | ok |
| 2021-03-31 23:40:15 | <hpc> | and not particularly satisfying for someone to which "I'm a seasoned programmer, but new to functional programming." applies |
| 2021-03-31 23:40:18 | × | Axman6 quits (~Axman6@pdpc/supporter/student/Axman6) (Ping timeout: 240 seconds) |
| 2021-03-31 23:40:42 | × | Deide quits (~Deide@217.155.19.23) (Quit: Seeee yaaaa) |
| 2021-03-31 23:40:54 | <hpc> | tuples aren't terribly new either, anyone can write struct {a thingone; a thingtwo; ...} |
| 2021-03-31 23:40:58 | <dmwit> | larryba: Yes, but (as I allude to above) `sizeof` is not the only consumer of arrays. |
| 2021-03-31 23:41:25 | × | larryba quits (~bc8134e3@199.204.85.195) (Disconnected by services) |
| 2021-03-31 23:41:28 | <dmwit> | larryba: And indeed even `sizeof` does not survive a function-call boundary. |
| 2021-03-31 23:41:35 | → | larryba joins (~bc8134e3@1582020-static.lxtnkya3.metronetinc.net) |
| 2021-03-31 23:41:39 | <larryba> | dmwit, that's because array in void foo(int array[20]) is not an array, it is a pointer to int |
| 2021-03-31 23:42:18 | <dmwit> | larryba: Right. So in C, it's not possible to write a type that is an array of a given length and have the compiler check this property. |
| 2021-03-31 23:42:26 | <larryba> | it is C's syntactic weirdness, that applies only to function arguments |
| 2021-03-31 23:42:39 | <dmwit> | Functions are kind a core to programming. =) |
| 2021-03-31 23:43:45 | × | heatsink quits (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) (Remote host closed the connection) |
| 2021-03-31 23:43:47 | <larryba> | dmwit, that's not correct; int main() { int array[100]; sizeof array returns sizeof(int) * 100 |
| 2021-03-31 23:44:04 | <dmwit> | larryba: Right. So? |
| 2021-03-31 23:44:06 | × | geowiesnot quits (~user@87-89-181-157.abo.bbox.fr) (Ping timeout: 240 seconds) |
| 2021-03-31 23:44:24 | <larryba> | so.. compiled checked that property (length), with compile-time construct, sizeof |
| 2021-03-31 23:44:27 | <dmwit> | larryba: Just because one part of the language gets this right doesn't mean all parts of the language get it right. |
| 2021-03-31 23:44:29 | <larryba> | compiler* |
| 2021-03-31 23:44:30 | × | ezrakilty quits (~ezrakilty@97-126-95-37.tukw.qwest.net) (Remote host closed the connection) |
| 2021-03-31 23:45:23 | <dmwit> | (I am perfectly happy to ignore the bit of the language that lets you write an incorrect cast. Pretty much every language offers this.) |
| 2021-03-31 23:46:47 | <dmwit> | larryba: Or, for another example that doesn't involve function boundaries: how would I write the type "pointer to array[20]" and have the compiler check that I only ever write pointers to correct-length arrays in there? |
| 2021-03-31 23:46:55 | <larryba> | btw I'm not sure what C's array-to-pointer decay has to do with my initial point |
| 2021-03-31 23:47:36 | <dmwit> | My point is that you think `int[20]` is easy. But it isn't, and the fact that it "appears" easy in C is deceptive. |
| 2021-03-31 23:47:46 | <larryba> | so now you want bounds checking? |
| 2021-03-31 23:47:50 | <dmwit> | To do a good job of it, you more or less have to go all the way to dependent types. |
| 2021-03-31 23:47:57 | <dmwit> | No, not bounds checking. Only length checking. |
| 2021-03-31 23:48:00 | <dmwit> | Which was the original request. |
| 2021-03-31 23:48:25 | <dmwit> | I do not demand that my runtime index be checked to be in bounds. Only that arrays stored in a variable have a given length. |
| 2021-03-31 23:48:45 | → | Axman6 joins (~Axman6@pdpc/supporter/student/Axman6) |
| 2021-03-31 23:49:08 | <larryba> | void foo(int (*array)[20]) <- ignoring casts, you can only pass a pointer to array of 20 ints to this function. if you try to pass a pointer to 21 ints, you will get a compile time diagnostic |
| 2021-03-31 23:49:35 | <larryba> | but arrays in C have the knowledge of their length. you are confusing them with pointers, which is what you get when you pass an array to a function |
| 2021-03-31 23:49:47 | <larryba> | (unless you wrap it in a struct) |
| 2021-03-31 23:53:04 | <dmwit> | Okay! |
| 2021-03-31 23:53:30 | <dmwit> | There's lots of fun operations that int[20] doesn't offer. But I agree that it is better than I thought it was. |
| 2021-03-31 23:55:42 | <dmwit> | (e.g. I doubt you can implement `void concat(int (*out)[m+n], int(*a)[m], int(*b)[n])` in any meaningful way. But then C doesn't pretend to offer polymorphism in the first place.) |
| 2021-03-31 23:57:27 | <larryba> | of course you can't, but that was my point, I'm pretty sure OP just wondered if there's a fixed size list-like data structure, like plain, dumb array in C, and now he's googling about dependent types :) |
| 2021-03-31 23:58:33 | <dmwit> | Maybe! Hard to know what was in OP's head. |
| 2021-03-31 23:59:15 | → | heatsink joins (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) |
| 2021-04-01 00:00:01 | × | zopsi quits (zopsi@2600:3c00::f03c:91ff:fe14:551f) (Quit: Oops) |
| 2021-04-01 00:00:02 | × | royal_screwup21 quits (52254809@gateway/web/cgi-irc/kiwiirc.com/ip.82.37.72.9) (Quit: Connection closed) |
| 2021-04-01 00:00:21 | → | royal_screwup21 joins (52254809@gateway/web/cgi-irc/kiwiirc.com/ip.82.37.72.9) |
| 2021-04-01 00:00:36 | → | zopsi joins (zopsi@2600:3c00::f03c:91ff:fe14:551f) |
| 2021-04-01 00:00:41 | × | Graypup_ quits (Graypup@lfcode.ca) (Quit: ZNC 1.6.1 - http://znc.in) |
| 2021-04-01 00:01:05 | × | gzj quits (~gzj@unaffiliated/gzj) (Remote host closed the connection) |
| 2021-04-01 00:01:21 | → | Graypup_ joins (Graypup@lfcode.ca) |
| 2021-04-01 00:01:26 | → | gzj joins (~gzj@unaffiliated/gzj) |
| 2021-04-01 00:02:40 | → | usr25 joins (~usr25@unaffiliated/usr25) |
| 2021-04-01 00:03:19 | × | borne quits (~fritjof@vpn05.bremen.freifunk.net) (Ping timeout: 265 seconds) |
| 2021-04-01 00:03:22 | <dmwit> | larryba: For context, one FAQ, both here and on StackOverflow, is this one: https://stackoverflow.com/q/11910143/791604 . I think it's pretty reasonable to see "how do I restrict my lists to have a specific length" and for your mind to go to this place, given that history. |
| 2021-04-01 00:03:33 | × | darthThorik quits (sid39589@gateway/web/irccloud.com/x-yyblajqqwaweohku) (Ping timeout: 252 seconds) |
| 2021-04-01 00:04:12 | × | hiroaki quits (~hiroaki@2a02:8108:8c40:2bb8:461b:1426:c666:74bc) (Ping timeout: 246 seconds) |
| 2021-04-01 00:04:14 | <dmwit> | (In other words, to go from "how do I create this specific compile-time check" to "how do I go from an arbitrary compile-time check to an implementation of that check".) |
| 2021-04-01 00:04:15 | × | caasih quits (sid13241@gateway/web/irccloud.com/x-ddqtrssgnjadgsqx) (Ping timeout: 250 seconds) |
| 2021-04-01 00:04:15 | × | runeks quits (sid21167@gateway/web/irccloud.com/x-cxruzufibvrhwxbg) (Ping timeout: 250 seconds) |
| 2021-04-01 00:04:36 | <dmwit> | It's very common to ask specific questions as stand-ins for general ones. |
| 2021-04-01 00:04:41 | × | pepeiborra quits (sid443799@gateway/web/irccloud.com/x-vocwsgeawpzzbkbk) (Ping timeout: 250 seconds) |
| 2021-04-01 00:05:05 | × | royal_screwup21 quits (52254809@gateway/web/cgi-irc/kiwiirc.com/ip.82.37.72.9) (Ping timeout: 252 seconds) |
| 2021-04-01 00:05:28 | → | molehillish joins (~molehilli@2600:8800:8d06:1800:49e2:dd02:cb68:846) |
| 2021-04-01 00:05:31 | → | darthThorik joins (sid39589@gateway/web/irccloud.com/x-ncuamoriibwvdwrv) |
| 2021-04-01 00:05:57 | <dmwit> | e.g. in the linked question's comments, the asker there makes it clear that they are doing so: the question is about numbers >0, but they want to know also how to do types for non-empty lists, sorted lists, and strings that are valid CC numbers. |
| 2021-04-01 00:06:11 | → | runeks joins (sid21167@gateway/web/irccloud.com/x-hasdkvyrirwackgz) |
| 2021-04-01 00:06:13 | → | borne joins (~fritjof@vpn05.bremen.freifunk.net) |
| 2021-04-01 00:06:19 | → | caasih joins (sid13241@gateway/web/irccloud.com/x-agadrzqzqvqjptgo) |
| 2021-04-01 00:06:50 | × | Narinas quits (~Narinas@187-178-93-112.dynamic.axtel.net) (Read error: Connection reset by peer) |
| 2021-04-01 00:06:56 | → | pepeiborra joins (sid443799@gateway/web/irccloud.com/x-smlzoyfyppguwjck) |
| 2021-04-01 00:09:22 | → | Narinas joins (~Narinas@187-178-93-112.dynamic.axtel.net) |
| 2021-04-01 00:10:01 | → | conal joins (~conal@64.71.133.70) |
| 2021-04-01 00:10:04 | × | molehillish quits (~molehilli@2600:8800:8d06:1800:49e2:dd02:cb68:846) (Ping timeout: 258 seconds) |
| 2021-04-01 00:10:13 | × | Tario quits (~Tario@201.192.165.173) (Ping timeout: 252 seconds) |
All times are in UTC.