Newest at the top
| 2026-04-25 13:49:09 +0000 | <ski> | (you could also, similarly, learn that an unknown type, is an instance of this or that type class) |
| 2026-04-25 13:48:50 +0000 | <raincomplex> | honestly my haskell is not very good, but just what you said about branches makes sense to me (x |
| 2026-04-25 13:47:56 +0000 | <ski> | raincomplex : makes sense ? |
| 2026-04-25 13:47:46 +0000 | <ski> | even though the type of `dict' is `Map String a', where `a' is unknown, after the `frob ...' invocation, we can *learn* more information (at run-time) about `a', by matching on `tag :: Tag a', and that knowledge is then statically (at compile-time), available in each corresponding branch |
| 2026-04-25 13:47:33 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 255 seconds) |
| 2026-04-25 13:46:40 +0000 | <ski> | so, you'd have something like `do ...; (dict,tag) <- frob ...; case tag of TagInt -> {- ok, we have a map of `Int's -}; TagDouble -> ...; TagList tag -> ...' |
| 2026-04-25 13:45:40 +0000 | <ski> | so, you get back a finite map with values of some unknown/forgotten/opaque/abstract/skolem type `a' (all values have the *same* type `a', for a single invocation of `frob'), but, when you inspect the accompanying value of type `Tag a', pattern-matching on it will inform the compiler about `a' being `Int', or `Double', or lists (possibly nested) of that |
| 2026-04-25 13:43:52 +0000 | <ski> | e.g. you could have an operation `frob :: ... -> IO (exists a. (Map String a,Tag a)', where `Tag' is defined by `data Tag :: * -> * where IntTag :: Tag Int; DoubleTag :: Tag Double; ListTag :: Tag a -> Tag [a]' |
| 2026-04-25 13:42:50 +0000 | <raincomplex> | ah right |
| 2026-04-25 13:42:32 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-04-25 13:42:26 +0000 | <ski> | a run-time check, with branching, that in particular branch(es) add additional typing assumptions |
| 2026-04-25 13:41:43 +0000 | r1bilski | (~r1bilski@user/r1bilski) (Ping timeout: 264 seconds) |
| 2026-04-25 13:41:30 +0000 | <raincomplex> | say more |
| 2026-04-25 13:40:17 +0000 | <ski> | you can have run-time checks inform compile-time types |
| 2026-04-25 13:38:21 +0000 | Alex_delenda_est | (~al_test@85.174.181.200) |
| 2026-04-25 13:31:39 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 272 seconds) |
| 2026-04-25 13:30:05 +0000 | <raincomplex> | [exa], i don't know much about julia but that definitely sounds interesting |
| 2026-04-25 13:27:53 +0000 | <raincomplex> | jreicher, right exactly |
| 2026-04-25 13:27:43 +0000 | <jreicher> | raincomplex: I didn't say there was nothing. It's more about choosing the boundary |
| 2026-04-25 13:27:05 +0000 | <[exa]> | raincomplex: oh btw, before I forget -- Julia occupies a very veeeeery interesting overlap of both design "directions"; makes an interesting study material |
| 2026-04-25 13:26:38 +0000 | <raincomplex> | if there were nothing unavoidably runtime, we wouldn't need to run programs |
| 2026-04-25 13:25:58 +0000 | <jreicher> | So if you're prepared to accept that, the real question is, what do you think is unavoidably runtime? |
| 2026-04-25 13:24:29 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-04-25 13:23:02 +0000 | <jreicher> | Compile time is better. It's the ultimate "fail fast". |
| 2026-04-25 13:22:31 +0000 | <raincomplex> | will it complain before i even run the program, or does it only complain when the runtime tries to do something that isn't allowed |
| 2026-04-25 13:22:09 +0000 | <jreicher> | Even "type system" is ambiguous. Do you mean type check? |
| 2026-04-25 13:21:45 +0000 | <raincomplex> | i think the aspect i'm considering most at this moment is the "eagerness" of the type system |
| 2026-04-25 13:20:42 +0000 | <raincomplex> | i'm using it loosely |
| 2026-04-25 13:20:36 +0000 | <jreicher> | raincomplex: "dynamic language" is something different again. The terminology is quite confused |
| 2026-04-25 13:20:35 +0000 | <raincomplex> | this is one thing that jumps out "The key idea is that many dynamically typed languages idiomatically reuse simple data structures like hashmaps to represent what in statically-typed languages are often represented by bespoke datatypes (usually defined as classes or structs)." |
| 2026-04-25 13:20:08 +0000 | <raincomplex> | this article touches on what i'm thinking about, although it's not its main focus https://lexi-lambda.github.io/blog/2020/01/19/no-dynamic-type-systems-are-not-inherently-more-open/ |
| 2026-04-25 13:17:27 +0000 | <raincomplex> | it makes big changes a lot easier to keep track of |
| 2026-04-25 13:16:51 +0000 | <raincomplex> | i really like the pattern of following the compiler errors |
| 2026-04-25 13:16:37 +0000 | <raincomplex> | often i feel like tests i write in a dynamic language are implementing a little type system |
| 2026-04-25 13:15:44 +0000 | <[exa]> | (more ideally, from type information that you don't even write because it's inferred from the rest of the program) |
| 2026-04-25 13:14:44 +0000 | <[exa]> | in haskell it's quite normal to have whole large parts of programs auto-derived just from the type information |
| 2026-04-25 13:14:07 +0000 | <[exa]> | raincomplex: ask what the types can actually do for you, constructively |
| 2026-04-25 13:13:30 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds) |
| 2026-04-25 13:13:07 +0000 | <raincomplex> | i like both static and dynamic languages, and i think i'm just trying to get my head around what i like about each, and what the tradeoffs actually are |
| 2026-04-25 13:12:34 +0000 | gmg | (~user@user/gehmehgeh) (Ping timeout: 265 seconds) |
| 2026-04-25 13:08:49 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-04-25 13:08:31 +0000 | <jreicher> | Consider how unpleasant it would be figuring out how to call an API (in any language) without knowing the types of things. |
| 2026-04-25 13:07:46 +0000 | <jreicher> | I agree with [exa]. In addition to the cost saving of a faster feedback loop for a competent community the type annotations convey semantic information to humans. |
| 2026-04-25 13:06:45 +0000 | <[exa]> | raincomplex: re development patterns, there's an interesting dynamics -- with static types you usually get the error quicker and more reliably located. So I somehow like the type-errors more than test-errors just because the interaction loop is usually much faster |
| 2026-04-25 13:06:14 +0000 | <jreicher> | Put another way, there's no point verifying a program by the time it's running. The damage is already going to be done. |
| 2026-04-25 13:06:01 +0000 | <ski> | sometimes it's called "tag checking" |
| 2026-04-25 13:05:13 +0000 | <jreicher> | In my opinion there's no such thing as a dynamically typed language in this sense. The "program verification" aspect of types disappear as soon as you don't have static type checking. What is meant by "dynamic types" is more like "dynamic dispatch", which is something different |
| 2026-04-25 13:05:02 +0000 | <ski> | raincomplex : looking into property-based testing (like e.g. QuickCheck and similar), and also (preferably higher-order) contract checking (Racket has one), would probably be helpful, as well |
| 2026-04-25 13:04:13 +0000 | <raincomplex> | i'm thinking about the development pattern of making some changes, and then fixing the errors that arise when compiling/running. in a statically typed language, the type system covers more of this than in a dynamically typed language, where you need tests (manual or automated) to trigger the errors |
| 2026-04-25 13:01:25 +0000 | <jreicher> | raincomplex: My hunch is that the infinite/finite distinction is what you're after. If you want to show that a specific set of inputs result in the right behaviour, testing will give you that. But if you're in the realm of "all possible inputs", and that all is either infinite or unfeasibly large, testing won't, but type checking might. |