2025/07/31

Newest at the top

2025-07-31 11:39:16 +0200tromp(~textual@2001:1c00:3487:1b00:b928:de3f:1dfd:983a)
2025-07-31 11:35:44 +0200trickard_(~trickard@cpe-54-98-47-163.wireline.com.au)
2025-07-31 11:35:30 +0200trickard(~trickard@cpe-54-98-47-163.wireline.com.au) (Read error: Connection reset by peer)
2025-07-31 11:34:15 +0200 <apache2> but if you can write the inner loop as a step that you can prove termination for, then you can have a small runner, and you know the inner loop won't get stuck
2025-07-31 11:32:59 +0200 <apache2> __monty__: I guess if you can prove things about the inner loop, you can often prove that the program doesn't terminate
2025-07-31 11:31:31 +0200 <__monty__> As soon as you have something long running like a daemon or a GUI, termination checking sounds like it should get hard to me.
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 +0200LainIwakura(~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 +0200sprout(~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 +0200caubert(~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 +0200tzh(~tzh@c-76-115-131-146.hsd1.or.comcast.net) (Quit: zzz)
2025-07-31 11:17:23 +0200Frostillicus(~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 +0200merijn(~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 +0200caubert(~caubert@user/caubert) (Ping timeout: 260 seconds)
2025-07-31 11:13:30 +0200chele(~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 +0200haritz(~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 +0200caubert(~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 +0200merijn(~merijn@77.242.116.146) (Ping timeout: 252 seconds)
2025-07-31 11:06:45 +0200kimiamania99(~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 +0200kimiamania99(~65804703@user/kimiamania) (Quit: Ping timeout (120 seconds))