Home freenode/#haskell: Logs Calendar

Logs: freenode/#haskell

←Prev  Next→ 502,152 events total
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.