Newest at the top
| 2025-01-10 11:58:33 +0100 | alist | (~alist@user/alist) (Quit: Leaving) |
| 2025-01-10 11:53:02 +0100 | <alist> | i think i can parse it but. idk sorry to flood the chat with like this one obsession i have |
| 2025-01-10 11:52:46 +0100 | <alist> | the paper is also sort of doubly confusing because it seems to use like an old version of set-builder notation? and it sometimes uses lambdas to describe set-theoretic functions haha |
| 2025-01-10 11:50:15 +0100 | <alist> | to be honest it seems to really have worked, ive been here for two days and both times people were able to answer really specific questions about this paper really quickly |
| 2025-01-10 11:49:26 +0100 | <haskellbridge> | <sm> haha, the old "hang out for a couple of decades" manouver eh |
| 2025-01-10 11:46:41 +0100 | <alist> | im hoping for the fast track |
| 2025-01-10 11:46:35 +0100 | <alist> | haha well i dont know if i have that kind of time |
| 2025-01-10 11:46:07 +0100 | <geekosaur> | that said, I got there by hanging out here for a couple decades 🙂 |
| 2025-01-10 11:45:41 +0100 | <geekosaur> | I'm fairly weak on type theory myself but can generally follow this stuff to some extent |
| 2025-01-10 11:45:13 +0100 | <alist> | geekosaur: right i understand this. i also understand how functions are relations. i have a mathematics background, but nothing related to type theory. |
| 2025-01-10 11:44:37 +0100 | <Athas> | merijn: yes, or just check for the Z and pick the right function. It feels a bit dumb, though. |
| 2025-01-10 11:44:27 +0100 | <geekosaur> | so, mathematically a function is exactly a mapping of values in the domain (input, with some handwaving) to values in the codomain (output, with similar handwaving) |
| 2025-01-10 11:44:18 +0100 | <alist> | geekosaur: ive been staring at what you wrote for like 10 minutes now and i think maybe im starting to get it? |
| 2025-01-10 11:43:44 +0100 | <alist> | merijn: i see. well thank you anyway, you have been very kind |
| 2025-01-10 11:43:19 +0100 | <merijn> | alist: That's beyond what I can skim from the paper and it's lunchtime |
| 2025-01-10 11:43:15 +0100 | <geekosaur> | probably easiest |
| 2025-01-10 11:43:11 +0100 | <geekosaur> | ^ |
| 2025-01-10 11:43:04 +0100 | <merijn> | Athas: Crazy talk: Why not replace Z with offset 0:00? :) |
| 2025-01-10 11:42:53 +0100 | <alist> | ah yes, but the advantage i guess is that they are not the same "kind" of set as the just collections of values. they are actual mappings? |
| 2025-01-10 11:42:47 +0100 | <geekosaur> | Athas, git is the one being annoying there, it should be consistent. I think the best you can do is try both and use the one that succeeds |
| 2025-01-10 11:42:04 +0100 | <merijn> | alist: Which, can be confusing, because in some sense relations are just "more sets" depending how you squint and how rigid you like your formalisms :p |
| 2025-01-10 11:41:24 +0100 | <merijn> | alist: we view types of functions as *relations* between sets, that's what that bit is about |
| 2025-01-10 11:39:48 +0100 | <Athas> | The ISO8601 instance for ZonedTime allows the offset (but not Z), while the instance for UTCTime allows Z (but not the offset). |
| 2025-01-10 11:39:20 +0100 | <alist> | merijn: i see. and so if the "type as set" view is inconvenient, what exactly is our view? "type as ..."? |
| 2025-01-10 11:39:07 +0100 | <Athas> | I need to parse git timestamps using the "strict ISO 8601 format". It produces timestamps that look like "2025-01-09T10:06:27+01:00" or "2025-01-09T10:06:27Z". That is, the timezone is either an offset or Z (which means 0). I can't find a simple way to do this with the 'time' library. Am I missing something? |
| 2025-01-10 11:38:25 +0100 | <hellwolf> | hello |
| 2025-01-10 11:37:28 +0100 | ubert | (~Thunderbi@2a02:8109:ab8a:5a00:6af7:7356:266e:a6fb) ubert |
| 2025-01-10 11:37:25 +0100 | <Athas> | Hello Haskell friends. |
| 2025-01-10 11:35:58 +0100 | <merijn> | alist: And the "type as set" view is inconvenient specifically for functions |
| 2025-01-10 11:35:30 +0100 | <geekosaur> | basically, to do anything with values of a type, you need relations saying what can be done with them |
| 2025-01-10 11:35:30 +0100 | <merijn> | alist: ah, so I think the confusion is this: Wadler we want to specifically talk about *function* types for our theorems |
| 2025-01-10 11:33:59 +0100 | <geekosaur> | types are sets, (mathematical) functions are relations between sets/types |
| 2025-01-10 11:31:17 +0100 | <alist> | *values, not elements |
| 2025-01-10 11:31:08 +0100 | <alist> | i thought they were relations, at first. i thought the author was saying that because just naively modeling types as sets of their elements didn't work out, so we are going to use relations |
| 2025-01-10 11:30:35 +0100 | <alist> | so, what are the targets of this isomorphism you mention? what are the types mapped to? |
| 2025-01-10 11:30:11 +0100 | <alist> | sorry i was just trying to understand what you wrote and what the author wrote |
| 2025-01-10 11:28:53 +0100 | <merijn> | What is the source of confusion? |
| 2025-01-10 11:27:42 +0100 | <alist> | lol |
| 2025-01-10 11:26:07 +0100 | <merijn> | That sounds about right for reading type theory papers :D |
| 2025-01-10 11:24:57 +0100 | <alist> | ok now i am confused |
| 2025-01-10 11:23:36 +0100 | <merijn> | i.e. types as sets of elements and functions as relations between their input set and output set |
| 2025-01-10 11:22:57 +0100 | <merijn> | alist: In section 2, on the bottom of page 4 the example is basically explaining an isomorphism between "types and functions" and "sets and relations" |
| 2025-01-10 11:21:32 +0100 | <merijn> | Not that everything is built in term of those |
| 2025-01-10 11:21:26 +0100 | <merijn> | alist: The identity type is only mentioned as a special relation |
| 2025-01-10 11:21:03 +0100 | <alist> | i see i see |
| 2025-01-10 11:20:47 +0100 | <merijn> | I don't think that's intended anywhere in the paper |
| 2025-01-10 11:20:22 +0100 | <merijn> | from the constant types, which are represented as identity relations |
| 2025-01-10 11:20:15 +0100 | <merijn> | alist: "i thought the relations we are quantifying over are inductively built |
| 2025-01-10 11:19:56 +0100 | <merijn> | alist: ah, I think you misinterpreted part of the intro stuff |
| 2025-01-10 11:11:47 +0100 | <alist> | it begins with the phrase "This can be further expanded in terms of the definition[...]" |