Newest at the top
| 2025-07-31 11:31:21 +0200 | <apache2> | I don't know about trivial, in languages where you can ask the type checker to check that your functions are total (like Agda) it's often *not trivial* to convince the type checker that that's the case |
| 2025-07-31 11:30:19 +0200 | LainIwakura | (~LainIwaku@user/LainIwakura) (Ping timeout: 272 seconds) |
| 2025-07-31 11:30:14 +0200 | <apache2> | it can still be a practical program, UNIX "yes" is an example of such |
| 2025-07-31 11:29:43 +0200 | sprout | (~sprout@84-80-106-227.fixed.kpn.net) (Remote host closed the connection) |
| 2025-07-31 11:29:35 +0200 | <apache2> | kuribas: in python you can write a program `while True: print("SPAM")` which clearly does not terminate |
| 2025-07-31 11:28:34 +0200 | <apache2> | it's a definition game |
| 2025-07-31 11:28:17 +0200 | <apache2> | segfaults leading to program termination is usually not, but you could define a language where that is a valid outcome |
| 2025-07-31 11:28:06 +0200 | <kuribas> | I just think most practical programs are trivially total. |
| 2025-07-31 11:26:32 +0200 | <apache2> | kuribas: throwing an exception is usually considered progress. |
| 2025-07-31 11:25:54 +0200 | <apache2> | kuribas: it's better if your aim is to prove things about the results :) it may not be better if your goal is to write a program that performs the task at hand - the more complicated the type system, the less likely the programmer is to terminate :) |
| 2025-07-31 11:25:40 +0200 | <kuribas> | An that any expression can throw any exception. |
| 2025-07-31 11:25:22 +0200 | <kuribas> | progress also disregards exceptions in many language, no? |
| 2025-07-31 11:24:11 +0200 | <__monty__> | It's interesting at least. |
| 2025-07-31 11:23:35 +0200 | <kuribas> | So total programming is better... |
| 2025-07-31 11:23:20 +0200 | <apache2> | which is a hell of a lot better than "yolo" but it doesn't mean your program will do what it was intended to do |
| 2025-07-31 11:22:51 +0200 | <apache2> | but if you can't prove that functions terminate, it's hard to talk about codomains. then you end up with "iff the function terminates, the result has the correct type" |
| 2025-07-31 11:21:28 +0200 | <apache2> | kuribas: sure, ensuring domains+codomains match up is a useful and common thing to achieve in a type checker |
| 2025-07-31 11:21:11 +0200 | caubert | (~caubert@user/caubert) caubert |
| 2025-07-31 11:20:52 +0200 | <apache2> | ie you may be able to rule out stalling Progress due to Int<->Float mismatch, but you may not be able to rule out stalling due to unterminating functions |
| 2025-07-31 11:20:27 +0200 | <kuribas> | Couldn't you say that it is about making sure the domains of functions are respected? |
| 2025-07-31 11:18:54 +0200 | <apache2> | type checking is usually used to verify that the program is internally consistent, not that it works. "internally consistent" is also a fluid concept, "with respect to which properties" is the follow-up question you can ask, and that the operational semantics should answer |
| 2025-07-31 11:18:21 +0200 | tzh | (~tzh@c-76-115-131-146.hsd1.or.comcast.net) (Quit: zzz) |
| 2025-07-31 11:17:23 +0200 | Frostillicus | (~Frostilli@pool-71-174-119-69.bstnma.fios.verizon.net) |
| 2025-07-31 11:16:49 +0200 | <kuribas> | Or a static analyser that shows some expression always throws a type error. |
| 2025-07-31 11:16:10 +0200 | <kuribas> | like with gradual typing you could have the properties failing... |
| 2025-07-31 11:15:58 +0200 | <kuribas> | true |
| 2025-07-31 11:15:43 +0200 | <apache2> | "dynamic" and "static" are fluid concepts, I'd be wary of treating conjectures that talk about "dynamic programming languages" as formal conjectures |
| 2025-07-31 11:15:40 +0200 | merijn | (~merijn@77.242.116.146) merijn |
| 2025-07-31 11:14:32 +0200 | <kuribas> | Well, maybe I misread the claim... |
| 2025-07-31 11:13:53 +0200 | <apache2> | they do* |
| 2025-07-31 11:13:47 +0200 | <apache2> | finding instances where they does not contradict a claim that they do not always hold |
| 2025-07-31 11:13:34 +0200 | caubert | (~caubert@user/caubert) (Ping timeout: 260 seconds) |
| 2025-07-31 11:13:30 +0200 | chele | (~chele@user/chele) chele |
| 2025-07-31 11:13:22 +0200 | <kuribas> | apache2: That the progress and preservation property does not hold for dynamic programming languages. |
| 2025-07-31 11:12:43 +0200 | <apache2> | re: contradiction/claim: what exactly is the claim you want to contradict? |
| 2025-07-31 11:12:26 +0200 | haritz | (~hrtz@user/haritz) (Quit: ZNC 1.8.2+deb3.1+deb12u1 - https://znc.in) |
| 2025-07-31 11:12:20 +0200 | <kuribas> | __monty__: I mean that a dynamically program always typechecks, in some trivial way. |
| 2025-07-31 11:11:15 +0200 | <kuribas> | apache2: sure, sbcl is quite good in inferring types. But still, I found I needed a lot of type annotations to make some compression algorithm efficient. |
| 2025-07-31 11:08:51 +0200 | caubert | (~caubert@user/caubert) caubert |
| 2025-07-31 11:08:41 +0200 | <apache2> | kuribas: it's not immediately useful, but it paves the way for typechecking subsets of the legal programs with a less forgiving type system, and then an optimizing compiler can work on those sub-languages. JIT compilers for dynamic languages or gradually typed languages often do something similar. |
| 2025-07-31 11:07:06 +0200 | merijn | (~merijn@77.242.116.146) (Ping timeout: 252 seconds) |
| 2025-07-31 11:06:45 +0200 | kimiamania99 | (~65804703@user/kimiamania) kimiamania |
| 2025-07-31 11:06:28 +0200 | <apache2> | __monty__: right, you can say (by definition) that raising an exception about a type mismatch is the way to handle an unexpected type, like if you have a function in the error monad that returns an error when a sumtype value has an unexpected constructor, or a integer type is negative, or whatever. then you can typecheck your valid program that legally outputs TypeError errors |
| 2025-07-31 11:06:22 +0200 | kimiamania99 | (~65804703@user/kimiamania) (Quit: Ping timeout (120 seconds)) |
| 2025-07-31 11:05:39 +0200 | Lycurgus | (~juan@user/Lycurgus) (Quit: irc.renjuan.org (juan@acm.org)) |
| 2025-07-31 11:05:10 +0200 | AVA | (~AVA@84.54.80.58) |
| 2025-07-31 11:05:00 +0200 | ljdarj | (~Thunderbi@user/ljdarj) (Ping timeout: 252 seconds) |
| 2025-07-31 11:03:43 +0200 | <__monty__> | kuribas: Runtime errors don't mean the type is invalid. Type checking is a static process. The Python program that results in a TypeError at runtime is still a valid program that would've passed typechecking. |
| 2025-07-31 11:03:09 +0200 | <apache2> | kuribas: this doesn't necessarily imply that you have Progress, but it can help. |
| 2025-07-31 10:59:19 +0200 | <apache2> | but yeah, you can model a lot of dynamically typed languages as a statically typed language where there is one GADT type, some mixed-type languages do that and even expose this "supertype" |