Threads for jonschoning
-
Probably adding a few features to my bookmarking software
-
jonschoning
2 years ago
|
link
| on:
Proposal for moderation policies: no tone policing, no pretending systemic bias doesn't exist
No tone policing.
It seems like what you disagree with in the the two examples that you listed under this point are not listed because you disagree with their tone, but because you disagree with their position.
It’s a mis-characterization to call this “tone policing”.
What you are really against is not Tone but the actual position these commenters hold .e.g saying it is Tone imples something is wrong with the way/manner they responded - i gather than any comment that opposed/challenged the parent comment, no matter the tone, would’ve produced a a similar criticism from you.
-
It’s tone policing which is being pointed out as a problem - not the tone itself, e.g. don’t call a comment aggressive because you read it like that.
-
So to be clear, in this instance of [don’t call a comment aggressive because you read it like that], from a moderation perspective, you’re OK with disagreeing with a comment (or with the implied meaning of a question), as long as one doesn’t make reference to the comment’s form directly (e.g. ‘this is aggressive’) or make an ad-hominem reference (e.g. ‘this commenter is aggressive’)?
-
Yes absolutely
-
-
-
-
Great news! I am eager to try this!
Turn on -XLinearTypes, and the first thing you will notice, probably, is that the error messages are typically unhelpful: you will get typing errors saying that you promised to use a variable linearly, but didn’t. How hasn’t it been used linearly? Well, it’s for you to puzzle out. And while what went wrong is sometimes egregiously obvious, it can often be tricky to figure the mistake out.
So, basically, GHC just got its own “Syntax error” a la OCaml… just a bit more specialized :p.
-
-
Good error reporting is easiest if it’s built into the compiler front end from the start. If a new algorithm comes along to improve the error information it’s almost never going to be a simple job to drop it into an existing compiler.
You need type information & parse information from code that’s potentially incorrect in both spaces, so any error algorithm usually has to be tightly integrated into both parts of the compiler front end. That tight integration usually means that improving compiler errors is a significant amount of work.
-
It varies. What puzzles me is that a lot of time ready to use, mergeable patches take much longer to merge than they should.
Like this talk: https://ocaml.org/meetings/ocaml/2014/chargueraud-slides.pdf
-
Do you also have a link for a patch for the improved error messages?
A lot of work has been going on to move OCaml to a new parser and improve error messages. Even though there is a lot still needed to be done, latest releases have started improving a lot. Maybe we can still extract some useful bits from that effort and try again
-
Turns out it was even made into a pull request that isn’t merged yet: https://github.com/ocaml/ocaml/pull/102
-
-
-
-
-
-
-
In logic, normal implication like A implies B means whenever you have A, you can derive B. You have tautologies like “A implies (A and A)” meaning you can always infinitely duplicate your premises.
Linear implication is a different notion where deriving B from A “consumes” A. So “A linearly implies B” is a rule that exchanges A for B. It’s not a tautology that “A linearly implies (A and A).”
The classic example is you can’t say that “$3 implies a cup of coffee” but “$3 linearly implies a cup of coffee” makes sense. So it’s a logical form that reasons about resources that can be consumed and exchanged.
Same in functional programming. A linear function from type A to type B is one that consumes an A value and produces a B value. If you use it once with an A value then you can’t use it again with the same A value.
This is nice for some performance guarantees, but also for encoding safety properties like “a stream can only be read once” etc.
-
Keynote: Linear Haskell: Practical Linearity in a Higher-Order Polymorphic Language https://skillsmatter.com/skillscasts/11067-keynote-linear-haskell-practical-linearity-in-a-higher-order-polymorphic-language
-
It can be used to model protocols with type signatures. The following is in theory what you should be able to do.
data ConsoleInput = Input String ConsoleOutput | ExitInput data ConsoleOutput = PrintLines ([String] ⊸ Console) & PrintLastLines ([String] ⊸ ()) greet :: ConsoleOutput ⊸ () greet console = let PrintLines f = console in step2 (f ["name?"]) step2 :: ConsoleInput ⊸ () step2 ExitInput = () step2 (Input input console) = let PrintLastLines f = console in f ["hello " ++ input]If you combine it with continuation passing style, you get classical linear logic and it’s a bit more convenient to use.
If you model user interfaces with types, they should be quite useful.
I’m also examining and studying them: http://boxbase.org/entries/2020/jun/15/linear-continuations/
-
-
Rust ownership is linear affine types. Linear types are similar but differ in the details. A shitty way of understanding it is affine types mimic ref counting and prevent you from having a ref count < 0. Linear types are more a way of acting like RAII in that you might create a resource but just “know” that someone later on in the chain does the cleanup.
Which I’m sure sounds similar but affine types allow for things like resource leaks but linear types should guarantee overall behavior to prevent it.
This all assumes my understanding and explanation is apt. I’m avoiding a ton of math and i’m sure the shitty analogy doesn’t hold up but behaviorally this is how I have it in my brain.
-
Linearity Design Space: https://i.imgur.com/s0Mxhcr.png
-
I’m personally of the stance that the 2020 linear ghc stuff is more <= 1 usage, and kinda misses out on a lot of really fun expressivity that can fall out of making full classical linear logic first class. But that’s a long discussion in its own right , and I’ve yet to make the time to figure out the right educational exposition on that front
-
it definitely seems more limited in scope/ambition compared to the effort ongoing for dependent types, for better or worse. Can’t say I know much about what first class linear logic would look like, but perhaps now there will be more discussion about such things.
-
The really amazing thing about full linear logic is it’s really sortah a rich way to just do mathematical modelling where everything has a really nice duality. The whole thing about linearity isn’t the crown jewel (though wonderfully useful for many applications ), it’s that you get a fully symmetric bag of dualities for every type / thing you can model.
The paper that really made it click for me was mike shulmans linear logic for constructive mathematics paper. It’s just a fun meaty read even at a conceptual level. There’s a lot of other work by him and other folks that taken together just point to it being a nice setting for formal modelling and perhaps foundations of category theory style tools too!
-
-
-
Not sure I can agree that Uniqueness types are the same as Linear types. Care to explain they’re similar sure but not the same thing and your… screenshot of a powerpoint? isn’t very illustrative of whatever point you’re trying to make here.
And from my experience with Idris, I’m not sure I’d call what Rust has Uniqueness types.
-
They are different rows in the matrix because they are different, of course.
it’s from this presentation about progress on linear ghc a little over a year ago https://lobste.rs/s/lc20e3/linear_types_are_merged_ghc#c_2xp2dx skip to 56:00
What is meant by Uniqueness types here is “i can guarantee that this function gets the unique ptr to a piece of memory” https://i.imgur.com/oJpN4eN.png
-
-
-
-
-
-
-
If the compiler can’t even report errors correctly, the feature shouldn’t ship.
Its more this is an opt-in feature with crappy error reporting for now using computer programming design features not in use in most programming languages. Its going to have rough edges. If we required everything to be perfect we’d never have anything improved. Linear types like this also might not have a great way to demonstrate errors, or the domain is new so why not ship the feature for use and figure out what kind of error reporting you want based on feedback.
-
-
Other people have sort-of said it, but not clearly enough I think. This is not a language feature being added. It is a feature-flagged experimental feature of a particular compiler. Most such compiler extensions never make it into real Haskell, and the ones that do take years after they are added to a compiler to make it to a language spec.
-
-
-
You might say “isn’t it not popular to write standards-compliant Haskell these days?” and you’d be right. Of course it’s often trendy to write nonstandard C (using, say, GNU extensions) or nonstandard HTML/JavaScript. However, ignoring the standard being trendy doesn’t mean the standard doesn’t exist, or even that it isn’t useful. I always make sure my Haskell is Haskell2010, and I try to avoid dependencies that use egregious extensions.
-
-
-
There’s a Haskell which runs on the JVM - Frege. But it makes no attempt to be compatible with the version of Haskell that GHC impements, for good reasons. Hugs is a Haskell interpreter (very out of date now, but still works fine for learning about Haskell.) There a bunch of other Haskell compilers, mostly research works that are now no longer in development - jhc, nhc98 etc etc.
But GHC is the dominant Haskell compiler by far. I don’t think there are any others in active development, apart from Frege, which isn’t interested in being compatible with GHC.
(“True Haskell” is the Haskell defined in the Haskell Report, but real world Haskell is the Haskell defined by what GHC + your choice of extensions accepts.)
-
There are other compilers and interpreters. None of them is anywhere near as popular as GHC, and usually when one does something interesting GHC consumes the interesting parts.
There is definitely a standard, though: https://www.haskell.org/onlinereport/haskell2010/
The whole reason language extensions are called “extensions” and require a magic pragma to turn on is that they are not features of the core language (Haskell) but experimental features of the compiler in question.
-
-
-
-
Overly terse error messages are bad, but they are better than wrong error messages. Some things are much harder to give helpful error messages for than others.
I wish people spend more time improving error reporting, at least in cases when the way to do it is well understood. There is no reason for say TOML or JSON parsers to just say “Syntax error”. But, YAML parsers are pretty much doomed to give unhelpful errors just because the language syntax is ambiguous by design.
And then some errors are only helpful because we know what their mean. Consider a simple example:
Prelude> 42 + "hello world" <interactive>:1:1: error: • No instance for (Num [Char]) arising from a use of ‘+’ • In the expression: 42 + "hello world" In an equation for ‘it’: it = 42 + "hello world"How helpful is it to a person not yet familiar with type classes? Well, it just isn’t. It’s not helping the reader to learn anything about type classes either.
-
-
The error they’re talking about is a kind of type error they’ve not worked with. It’s produced if you forget to construct or use a structure. I I’m guessing it’s technically “proper” but the produced error message may be difficult to interpret.
They’ve ensured it’s a feature you can entirely ignore if you want to. Everybody’s not convinced they need this.
I otherwise dunno what they’re doing and I’m scratching my head at the message. Something like “Oh cool you’ve done this… … … So where are the types?”
-
-
So you never got a C++ template error in the good olden days?
No, because I looked at the language, figured out that the people involved completely lost their fucking mind, and moved on.
Seriously though, it just got merged. It’s not released or “shipped” in any means.
They took 4 years to arrive at the current state, which I’ll approximate at roughly 10% done (impl unfinished, spec has unresolved questions, documentation doesn’t really seem to exist, IDE support not even on the radar).
So if you assume that there will be a Haskell version in the next 36 years, then this thing is going to end up in some Haskell release sooner or later.
-
So if you assume that there will be a Haskell version in the next 36 years, then this thing is going to end up in some Haskell release sooner or later.
Could you elaborate on this? If practical users of linear types will only use them if they have good error messages, and early testers want to work out the kinks now, what’s wrong with having a half-baked linear types feature with no error messages permanently enshrined in GHC 8.12?
-
-
-
-
-
This is incredible! I had no idea this effort was going on! Can anyone speak to the performance implications? I assume the back-end is making minimal use, currently, but am I correct in thinking that, in theory, this could enable performance of ergonomic linear Haskell to meet or exceed the performance of C/C++/Rust?
-
Linear types do not suddenly turn Haskell into a language in which performance is easy to reason about. In particular, (a) it is still a lazy language, (b) it still does not allow you to control how much indirection is used in the representation of your data structures, (c) it still has features like polymorphic recursion, which restrict the compiler’s ability to monomorphize all types and get rid of the vtables in polymorphic code.
-
Since you don’t seem to be someone who is interested in the language at all, I find it odd that you are responding here about completely different concerns that you have, that i’ll add, aren’t even related to the article topic.
-
First of all, I only meant to reply to a specific question. I did not intend to do any of the following: (a) suggest Haskell is a bad language to use, (b) suggest any of the raised “issues” [if they could be called that] is a terribly big deal for most use cases, (c) hurt anyone’s feelings.
Second, I am interested in all languages with substructural types. More precisely, I am interested in lightweight tools for algorithm verification, and there is a qualitative jump from what you can verify without substructural types, to what you can verify with them.
-
ok
-
-
-
-
-
I’m no expert but here is the original paper (2018)! https://doi.org/10.1145/3158093
One of the performance applications is making read and write operations work on the bits of packed (serialized) ADTs. So it removes a need to have a decoded copy of that data via serialization/deserialization. They have a graph on how this improves summing and mapping over a binary tree.
-
-
Probably adding a few more bookmarking features to https://github.com/jonschoning/espial , just added firefox bookmark imports.
-
call me when we get discriminated unions with exhaustive pattern matching
-
I built an Ergodox classic - it was very nice - but something about the layout felt a little rigid - i much preferred my kinesis advantage
-
I agree about preferring the Kinesis Advantage! I originally bought the Ergodox EZ, and though it was nice, I didn’t find it very comfortable. I ended up buying two Kinesis Advantage 2 keyboards, for work and for home, out of my own pocket. (I’m looking to sell my Ergodox EZ if anyone is interested lol)
Although I’d personally recommend the Kinesis Advantage if you’re looking for comfort, I do have to admit that I missed the additional two columns of keys for my index fingers on the Ergodox. I also miss the ability to map one key to many (like mapping
ALT-Tabto a single key, or mapping asuperkey)-
The choice of switches is also much worse for the Advantage; I think there are only two or three middling options.
-
This whole thread pushed me somewhat into the rabbit hole of reading about keyboards. It appears there is an Advantage-like layout out there now called Dactyl and Xah Lee seems to really like it. It has a later tweaked variant called Dactyl Manuform; I think they both might be interesting esp. to people torn between Ergodox and Kinesis Advantage.
-
-
I put together an ergodox classic and immediately fell in love with it. I’ve also got the ergodox infinity and the ergodox ez. One thing I’d recommend is to go with the tent kit for the ez and/or 3d printed tents for the classic. I’ve never found the ergodox uncomfortable, but tents are definitely a welcome improvement.
-
-
-
working on https://github.com/jonschoning/espial my open-source, web-based bookmarking server.
-
-
When you have over 67,000 bookmarks, as i do, I feel open-source/self-hosted becomes a higher priority due to for data ownership and performance reasons.
By moving to self-hosted, i was able to bring down my “cold-start”/“non-cached” wait time on tag filters from 30s to ~1s.
AFAICT most folks don’t have more than a couple thousand at the high end, so they probably don’t run into these perf issues — although it was my motivation, it’s probably not relevant to them.
My use case involves creating marks as part of browsing for things i want to return to later in the day, and also for long-term recall or aggregation when researching a topic, with as low/minimal-effort as possible (which is why I’ve accumulated so many)
-
-
-
-
bitemyapp
edited
5 years ago
|
link
| on:
Rich Hickey delivers rationale for choosing dynamic typing in Clojure
Not for proving theories about […]
Come now. Types establish facts and enforce useful equalities that help in writing and maintaining software. It makes the code more amenable to human comprehension and along the way it gives you mechanical assistance, which is huge. They’re also essentially “free” proofs as the only proof required is the code-that-does-the-thing-you-want-to-do. The only time this isn’t the case is if you’re using a DTPL and need to establish something not eminently obvious from a straight-forward implementation. With type inference you also don’t have to state your expectations. You can write the code that you think should work and see what type you get. In Haskell you can then flip that around, declare some types, set their implementations to
undefined, and then play with the types to see if you’re headed where you want to get. Particularly useful for library integrations. Like a “bidirectional conversation” with the compiler about what’s going on.I, for one, embrace having become a cyborg.
I don’t really want to get sucked into this debate, but I’ll note that I don’t often see Haskellers seeking this debate out like they used to. Myself included. It seems to mostly be users of untyped languages feeling insecure/defensive about it. You can do what you want, but don’t get upset when it instigates rebuttals. I think some of the communication difficulties here are related to how I didn’t really appreciate types until I grokked a language with nice types. Then I saw how there was no “trade-off”, all stages of a project or idea could become faster and easier, from ideation to EOL maintenance.
I used to use Clojure and Datomic in production and let me say that the proof is not in the pudding for what Rich is saying. Datomic was a spectacularly poorly managed product. Getting irritated with unnecessarily difficult-to-debug runtime errors in a few hundred lines of Clojure is what drove me to finally learn Haskell, so I guess I should thank Rich for that.
There’s a great thread started by Chris Done here.
Other good replies
-
It makes the code more amenable to human comprehension
No, not for everyone. I find thinking in types way more constraining than thinking in values at runtime. Apparently, there are many people like me.
and along the way it gives you mechanical assistance, which is huge.
No, it’s not huge. There’s no conclusive study showing that type checking improves quality. It usually boils down, again, to personal preference of particular people doing the coding.
I’m not against type checking in general (heck, Rust is one of my favorite languages, as is Python). But the outright arrogance of quite a few people considering type checking to be a clearly superior paradigm, here on Lobste.rs and elsewhere, starts getting on my nerves, sorry.
It seems to mostly be users of untyped languages feeling insecure/defensive about it.
That sounds like confirmation bias and doesn’t advance the discussion. Look at how every pro-dynamic typing article is upvoted (this one and one of Bob Martin’s recently) and gets shredded in the comments, with gusto.
-
No, not for everyone. I find thinking in types way more constraining than thinking in values at runtime. Apparently, there are many people like me.
Can you describe what you mean by that? Are you saying the runtime values do not correspond to any static type? When I write in a dynamic language, I still think about things in terms of what type they correspond to. Do you not do this?
-
Right… Since I keep failing to write a good blog post about it, let me use this opportunity to try and articulate this here.
Yes, runtime values do have types, but that alone is both too much and too little:
- too much in a sense that I usually don’t care about the majority of the allowed operations on this type at a particular place in my code
- too little in a sense that a type does not convey semantics (okay, it’s a string, but what it represents?)
Consider an example in (hopefully) self-descriptive Python:
def read_safe(filename): if os.path.exists(filename): return open(filename).read() return 'default_value'I don’t care here if I can, say, upcase the filename, or if it’s representable as a valid utf-8, or of any other string properties. The only thing that this code actually cares about is that this value can be checked against if a certain file exists and can be opened by this name.
Conversely, the name that I chose for this value — “filename” — already tells a programmer much more than the knowledge that it might be a string. We all know what a “filename” is. (Hickey talks about this too in that video.)
And in fact, depending on the version of Python this value can be of many different types: an array of bytes, an array of 16- or 32 bit unicode codepoints, and in later Pythons — an instance of pathlib.Path. And this particular function doesn’t care in the slightest, it works without changes. This is why I don’t like the excitement in the Python community about type annotations: as soon as this value with is annotated with any concrete type it’s coupled with irrelevant details and becomes a maintenance burden.
In a typed language we could invent an interface/trait/protocol for such a value. But then we will have to invent and maintain very granular definitions of such contracts for every possible use case, whereas in a dynamic language the value contract is defined by the way the value is actually used.
-
too little in a sense that a type does not convey semantics (okay, it’s a string, but what it represents?)
It’s pretty common in languages with good type systems that using strings for things that are more semantically rich falls away. I generally have some abstract type that can be converted to and from a string but in the business layer it remains this abstract type. So a social security number would not be a
StringbutSSNtype where its underlying representation is hidden.How would you communicate to users of the function what
filenamecan be, though? Somewhere, someone has to state what the thingsopencan validly take, right? This informalism seems convenient for you, you’re just writing a function that passes its input to another function and, hey, if they give you something thatopendoesn’t take, that’s not your problem, amirite? But what if you need to do any bit of manipulation offilenamebefore opening it? For example, the_safepart means that it won’t read from/etc/so you need to check if it starts with that. Isn’t the flexibility a hindrance now? This code suddenly balloons because it has to handle all these possible representations of a filename.Conversely, the name that I chose for this value — “filename” — already tells a programmer much more than the knowledge that it might be a string.
But what if we made an abstract type called
Pathand the only way to construct aPathwas in such a way that obeyed the operating system’s definition of what a path is?Maybe I’m getting side tracked though, I was trying to understand how you think about things in terms of runtime values, but it still feels to me like you think in terms of types, you’re just letting something else deal with it. But maybe I just don’t get it.
-
How would you communicate to users of the function what filename can be, though?
A docstring! I actually often call Python a docstring-typed language :-) The good part of this is that it’s not formal, so you can convey meaning in whatever way you feel best. This is, of course, the worst part as well because you can mislead or completely ignore the fact that your users need to know what the hell
foritemsmean in your argument list. So, to be clear, I’m not saying there’s an iron-clad solution to bad APIs, I’m saying that adequate means are available.Also, given the introspective nature of dynamic languages it’s usually fairly easy to drop down a level and just read the source code and see how those parameters are used. For example in the
ipythonshell it just requires adding a second?to an object (func?would show the docstring,func??— the source).if they give you something that
opendoesn’t take, that’s not your problem, amirite?Yes. I’m not sure how problematic you see it, though. It surely happens from time to time, but a single traceback is usually enough to see at which level of the stack something expected a different value.
But what if we made an abstract type called Path and the only way to construct a Path was in such a way that obeyed the operating system’s definition of what a path is?
That would’ve been awesome! But we didn’t. You can’t anticipate all the usage patterns and invent ideal data types for everything from the get go.
That’s a little beside the point though (unless I misunderstand something). Assumption change, and code has to be refactored.
I was trying to understand how you think about things in terms of runtime values, but it still feels to me like you think in terms of types, you’re just letting something else deal with it.
The difference is that instead of specifying a concrete type as part of the function contract I’m specifying this contract in a different way that allows a user choose whatever type they happen to have around. And yes, they’re responsible for seeing if it actually works.
The main idea of this dichotomy is not that “values don’t have types”. Of course they do. It’s just that a notion of type may not be the best (and certainly not the only) way to establish an API contract. It disallows using other un-anticipated types, and it doesn’t convey the particulars of using a value in this particular function (even if I say “this is a Path”, it fails to say that it should be
openable).Let’s push this a little further… Values have many properties by which they can be grouped with other values. Size, memory layout, origin, security context, mutability, lifetime — you name it. A “type” is usually a combination of a few of those, but ultimately it doesn’t tell you everything about the value. Only the value itself can tell you everything about itself. “Thinking in values” as opposed to “thinking in types” is the proposition to accept this fact. And yes, the flexibility of being more expressive does have downsides. Like not being able to rely on fixed memory layout to compile into an efficient machine code.
-
It disallows using other un-anticipated types, and it doesn’t convey the particulars of using a value in this particular function (even if I say “this is a Path”, it fails to say that it should be openable).
I’m not really grokking this “un-anticipated types” part of your argument, though. At some point, someone has to implement how to handle string,
Pathand all the encodings. In the case of your example, that is whoever implementedopen. So there are no un-anticipated types, we can’t pass an int in there and expectopento magically figure out what to do with it.And so, if someone needed to figure out what the type was at some point, then that means that, at the very least, we could infer the type of
filenamebased on its usage inopen. So I’m not really understanding what is being saved or won in the example you’re using.-
In this example, what’s being saved is the need to update type annotations on arguments of
read_safethat sits in the middle. While the user upstream andopendownstream care about it,read_safedoesn’t have to. In a typed language, it does.It’s not the only advantage though… Consider a different example:
def process_json(f): data = json.load(f) return process(data)Here, the only contract on
fis that it should have the.read()method returning some json. It can be of any type having many more methods. And evenjson.loaddoesn’t have to care about everything else those concrete types can do, it only cares about the subset.This is exactly what interfaces/traits/protocols are about with added flexibility of not having to define a new one for every particular use case.
So, there’s really nothing more to it than saying “don’t tell what type it is, tell me what it should do”.
-
In this example, what’s being saved is the need to update type annotations on arguments of read_safe that sits in the middle.
But either the type inference engine can figure that out on its own, or in the case of
read_safe, I could just say thatfilenamehas the same type as the input toopen, that way ifopenchanges,read_safegets it for free.Here, the only contract on f is that it should have the .read() method returning some json
Don’t you mean
.read()method returning a string?So, there’s really nothing more to it than saying “don’t tell what type it is, tell me what it should do”.
This is exactly what structural typing will do, which is what Ocaml’s object system is based on. It can infer the type of input based on what methods you call or you can specify the type based on what things it can do.
-
Yeah, language that require type annotations can be a pain. Whole-program inference is a must-have feature, IMHO.
-
-
-
-
-
-
No, not for everyone. I find thinking in types way more constraining than thinking in values at runtime. Apparently, there are many people like me.
That’s familiarity, not a difference in how your brain works.
No, it’s not huge. There’s no conclusive study showing that type checking improves quality. It usually boils down, again, to personal preference of particular people doing the coding.
We don’t have sound experimental protocols for this. Reading tea leaves on GitHub is not science.
I’m not against type checking in general (heck, Rust is one of my favorite languages, as is Python). But the outright arrogance of quite a few people considering type checking to be a clearly superior paradigm, here on Lobste.rs and elsewhere, starts getting on my nerves, sorry.
I don’t care what you believe or use. If nobody lies about the tools or practices then I won’t have to rebut anything.
That sounds like confirmation bias and doesn’t advance the discussion. Look at how every pro-dynamic typing article is upvoted (this one and one of Bob Martin’s recently) and gets shredded in the comments, with gusto.
Bob Martin’s post was even more ignorant than this talk, it deserved to get shredded if only for making preferential users of dynamic typing look dumb.
Reiterating what I said in my first post, I don’t reaaaallyyyyy want to debate this because people tend to get upset and I don’t think arguing with programmers is a good use of my time or this space. You’re going to believe what you believe until you get shocked out of it. That’s just how this thing tends to go, nobody’s actually open-minded in these threads. So why not spare ourselves the grief and get back to work?
-
It’s got nothing to do with familiarity. Types force you to express yourself in a way that can be verified statically by the type checker. A set of provable statements is necessarily a subset of all valid statements. Static typing restricts how you can express yourself, and that’s the biggest drawback of this approach.
At the end of the day, a human has to be able to read the code and understand its intent. Anything that distracts from that is a net negative in my experience. For example, you could write a 300 line sort in Idris https://github.com/davidfstr/idris-insertion-sort/blob/master/InsertionSort.idr that verifies all kinds of things statically. Understanding that it’s semantically correct is much harder than it would be for a 5 line version without types.
-
A set of provable statements is necessarily a subset of all valid statements.
You don’t typically run into incompleteness when you’re only using lightweight types like with run-of-the-mill Haskell. If your program is ill-typed in Haskell, the overwhelmingly likely scenario is that your program is just wrong or unsafe, not that it’s correct but can’t be typed.
-
That depends what you’re doing and what you consider “Hakell”. It’s not too hard to run into a need for RankNTypes in some cases (though you can usually write the code in a different way to avoid that need).
-
Sure, but at that point you’ve already accepted that there is value in avoiding formalism. At that point it’s just a matter of degrees of comfort. My view is that code should be written for human readability first and foremost, because only a human reader can decide whether it’s semantically correct or not.
-
There’s a minimum amount of formalism, but there isn’t a maximum amount of formalism. It’s necessarily a matter of degree. The argument is that most people pick way too low.
I find Haskell code more readable than the vast majority of languages, at a given level of program complexity. You seem to be assuming that Haskell is hard to read, which I don’t think is a reasonable assumption at all.
-
I find a lot of people also conflate typing with type signatures. What makes Haskell great is you can get many of the type system benefits without ever writing a type signature at all!
-
-
Sure, but at that point you’ve already accepted that there is value in avoiding formalism.
There is value in not being tied to a specific formalism. But there is little value in avoiding all formalisms altogether, unless you count the possibility of being wrong as “value”.
only a human reader can decide whether it’s semantically correct or not.
Only if the human reader can reliably prove things about programs.
-
This is something that static typing proponents have to demonstrate empirically. So far there’s no compelling evidence to suggest that projects are delivered faster with statically typed languages, have less defects, or improved ease of maintenance. Considering how long both type disciplines have been around, that’s quite the elephant in the room. I’ve heard the sentiment that it’s just too hard to test for this, but that just rings hollow to me. If something is clearly more effective that would be possible to demonstrate.
It’s a false dichotomy to claim that you either use static typing or nothing at all. The reality is the formalism of using the type system is only one approach, and other approaches appear to be equally as effective in practice. You have testing, static analsysis tools like Erlang dialyzer http://erlang.org/doc/man/dialyzer.html runtime specification tools like Clojure Spec https://clojure.org/about/spec
-
-
This is something that static typing proponents have to demonstrate empirically.
No—You have to be more careful about how you’ve selected the “burden of proof”.
You’ve placed it on requiring proof that static types provide X benefit.
One can just as well turn this around and require poof that eschewing static types provide X benefit.
We cannot a-priori place such demands in either direction.
Finally, Requiring statistically significant studies pretty much guarantees no provable claims can be made for any side; since that amounts to a social science laden with shaky assumptions and ambiguous modeling. ‘reading the tea leaves on github is not science’
(~crossposted from hn thread)
-
Requiring statistically significant studies pretty much guarantees no provable claims can be made for any side; since that amounts to a social science laden with shaky assumptions and ambiguous modeling.
It’s not a guarantee. We have the techniques and skill required to do a rigorous study, it’s just that such a study is really expensive and nobody wants to invest the money. “It’s hard” is not a reason to give up on something.
-
Very well; I eagerly await the studies then.
In the meantime, then, be skeptical about claims that attempt to discredit practices such as static typing due to an undue burden of proof requirement.
-
-
-
You’ve placed it on requiring proof that static types provide X benefit.
That’s actually a correct burden of proof. We usually put it on the person claiming something brings benefits or should be a standard practice. So, if static typing has benefits, it’s up to us who believe that to demonstrate that using logical arguments and/or evidence in the field. There’s people in the discussion doing that. So, we don’t have to worry about burden of proof since we’re doing our part. ;)
-
Claiming the same point more strongly doesn’t provide new information or absolve you from the contradiction I’ve identified
-
Yogthos correctly noted that the burden of proof is on anyone challenging the status quo. The status quo is that there’s no consensus in this forum or in programming community at large whether static typing improves software over dynamic with their style of quality assurance. Yogthos wanted anyone pushing static types as the new, status quo that we should all adopt for the claimed benefits to provide evidence of those benefits. This is the standard method of discussion. When you countered that, I reminded you of that and that’s all my comment was about.
Now you’re talking about a contradiction I have to absolve. Whatever it is will be a separate point to discuss. Burden of proof remains on anyone advocating adoption of a method with claimed benefits. They prove it. Then people should check it. Otherwise, we’d have to accept an Internet’s worth of false claims wasting time proving each one wrong. That would be a waste of time. Hence, the established direction for burden of proof.
-
-
-
-
This is something that static typing proponents have to demonstrate empirically. So far there’s no compelling evidence to suggest that projects are delivered faster with statically typed languages, have less defects, or improved ease of maintenance.
As I said elsewhere in the discussion, I’m not advocating static type systems in this discussion. Formalisms other than types do exist! However, if you want your programs to be free of defects, you have to prove them correct. Types sometimes make a very small contribution towards that goal. Tests don’t help one iota.
-
-
If you want your programs to be correct, you have to ensure they work as specified for the use cases you have.
No disagreement here. However, the claim that a program works as specified requires proof.
You can try to do that using static types, or you can use tests or a runtime contract.
Most type systems only allow you to prove very trivial things about your programs. Tests are only a feasible strategy if the space of legitimate inputs is small enough to be exhaustively searched. “Runtime contracts” are a misnomer, but assuming you meant “runtime contract checks”, well, those don’t prove your program correct.
-
Proof is a formal term and typically implies correctness for all possible cases. A program has to only demonstrate correctness for possible inputs.
Ultimately, your program has to have some sort of specification. My experience is that these specifications will not be formal in practice. You have to code your program to whatever requirements you have as best understood.
A runtime contract like Clojure Spec https://clojure.org/about/spec will allow you to encode a specification and do generative testing against it. This is a sufficient level of proof that the software works as expected for vast majority of situations.
-
Proof is a formal term and typically implies correctness for all possible cases. A program has to only demonstrate correctness for possible inputs.
What distinction are you making between “all possible cases” and “all possible inputs”?
Ultimately, your program has to have some sort of specification. My experience is that these specifications will not be formal in practice. You have to code your program to whatever requirements you have as best understood.
Of course, you can’t expect a business analyst or what-have-you to hand you a formal specification. You have to generate it yourself from the information you have been given.
A runtime contract like Clojure Spec https://clojure.org/about/spec will allow you to encode a specification
This would actually be a formal specification, assuming you have a formal semantics for Clojure! The proof that your program meets the specification is still missing, though.
and do generative testing against it.
Generative testing is a little bit smarter than unit testing, but it’s no replacement for a proof.
-
-
It’s worth noting that the first property-based testing library was QuickCheck for Haskell, so proof is no replacement for generative testing, either.
Let’s set aside for a while the matter of whether your conclusion is true or false. I fail to see how exactly your premise entails your conclusion. Are you implicitly assuming that Haskell’s type system can verify every property you could possibly care about, and even then it still wasn’t enough?
-
-
-
I think there’s a miscommunication happening here. I love formal methods to the point I spent months writing a manual on TLA+. I just don’t think it’s enough. It’s not enough to prove your program is correct: you have to obsessively test it too.
-
-
-
-
-
-
Let’s say I have inputs a and b, and a result c. If I know my input range is from 0-100, I can test that a^n + b^n = c^n for all possible inputs. However, it’s much more difficult to prove this to be the case for any input in general.
This would actually be a formal specification, assuming you have a formal semantics for Clojure! The proof that your program meets the specification is still missing, though.
I would argue that it’s not required. If I have a specification, I can do generative testing to exercise the code, and I can validate that the data coming into the system is within the accepted range.
My argument is that the effort required to provide an exhaustive proof is not justified in vast majority of situations. The business requirement is typically to produce software that works well enough that the users are happy. A proof is not a business requirement.
-
-
-
-
-
-
-
-
-
Appears I misread your comment. That said, I do think there is value in possibility of being wrong, if that means you can express yourself in a less constrained fashion. Ultimately, your formal specification can be wrong as well, so it’s really a question of where you’re going to be looking for errors.
-
Appears I misread your comment.
I didn’t even bring types into the discussion until you did.
That said, I do think there is value in possibility of being wrong, if that means you can express yourself in a less constrained fashion.
The only freedom that you get is the freedom to say nonsense. That’s not terribly useful.
Ultimately, your formal specification can be wrong as well
So you test it, more or less the same way scientists test scientific theories:
- Make predictions (i.e., logical inferences from the specification) about what the user meant in distinct cases.
- Ask the user if these predictions agree with what they expected.
-
The only freedom that you get is the freedom to say nonsense. That’s not terribly useful.
That’s absurd. You can state many things without being able to prove them. As long as you can demonstrate that the statement works within the context you’re using it, you get value out of it.
So you test it, more or less the same way scientists test scientific theories:
Which is exactly what you’d do with tests or runtime specifications.
Ultimately, we’re discussing cost benefit here. My claim is that you can deliver working software faster without using formal proofs. That’s what the business cares about at the end of the day. A company that delivers a working product that people use will outcompete the company working on a perfect product.
-
-
While we don’t have a proof, we certainly have a lot of evidence accumulated over the years. If formal proofs were indeed a requirement for developing usable software, then we’d all be using them by now. It’s really that simple.
Businesses using languages like Haskell and OCaml would outcompete those using Python, Ruby, or JavaScript. This is not what we see happening in practice though. Despite these languages having been around for many decades, they remain niche.
Now, it’s perfectly possible that once somebody is trained up sufficiently they could be just as productive. However, that seems to be a challenge as well.
At the end of the day we need languages that can be learned relatively easily by an average developer to become productive with. The more formal the language the less accessible it becomes. So economics aren’t in favor of formal methods I’m afraid.
-
If formal proofs were indeed a requirement for developing usable software, then we’d all be using them by now.
Sure, one can trivially argue they are not a requirement but we lack any reasonable amount of scientific study on if they help. I think they probably do (more understanding of / reasoning about code seems likely to help quality) but what I think is hardly science ;)
-
Businesses using languages like Haskell and OCaml would outcompete those using Python, Ruby, or JavaScript.
I don’t see how you arrive to that conclusion. Neither Haskell nor OCaml is in short supply of features that make formal verification harder than necessary.
At the end of the day we need languages that can be learned relatively easily by an average developer to become productive with.
Maybe the notion of “average developer” is the problem in the first place?
-
You still haven’t explained what sort of formal verification you advocate, or given an example of a language using it. Haskell and OCaml are the most popular formal languages I’m aware of. Are you talking about languages like Coq here?
From a business perspective, you need a tool that can be learned in a reasonable amount of time by a person you’re going to be able to hire from the pool of people available. That’s where your average developer comes from. Technology that can be used by a wider pool of people effectively will always dominate.
-
-
-
-
-
-
-
-
-
-
-
-
-
-
For example, you could write a 300 line sort in Idris https://github.com/davidfstr/idris-insertion-sort/blob/master/InsertionSort.idr that verifies all kinds of things statically. Understanding that it’s semantically correct is much harder than it would be for a 5 line version without types.
https://research.googleblog.com/2006/06/extra-extra-read-all-about-it-nearly.html
-
Sure, and these are exactly the types of bugs you will see in the real world in dynamically typed languages. I’ll let you decide if that bug was a show stopper or not for production use. Also from the link:
And now we know the binary search is bug-free, right? Well, we strongly suspect so, but we don’t know. It is not sufficient merely to prove a program correct; you have to test it too.
-
-
-
-
The Idris example is interesting but doesn’t say too much. There is lots of complicated ways things can be solved with or without types. I don’t know if the link you pasted is considered a good solution or not.
That being said, one thing that the Idris solution will give you but a dynamically typed solution won’t without extensive tests is if I modify the code in such a way that it violates the invariants, the compiler will complain. This is a major benefit of a good type system, IME.
-
However, you have to know that the invariants themselves are correct. A type specification is effectively a program that the type checker uses to analyze your original program. If a specification is as complex as the Idris example, it becomes difficult to tell whether it’s correct in any meaningful sense. So, now you just pushed the problem back, you just have a metaprogram that you have to reason about.
-
The thing you are missing:
In typed languages you often have to be wrong twice to introduce a bug: You have to get both the code and the types wrong. Getting only one of them wrong will be flagged and rejected by the compiler.
In untyped languages you usually have to be right twice to avoid a bug: Yo have to get both the code and the tests right. Getting only one of them wrong is no reliable guarantee that your bug will be found before deployment.
-
-
I’m not missing that at all. My point is that the formalism often requires you to express yourself in a specific way that can be verify. So, while you know something is self-consistent, you don’t know that it’s correct in a semantic sense.
Dynamic languages let you write much more direct code that’s easier for a human to read. Meanwhile, you can also provide specifications in a dynamic language. Take a look at Racket Contracts or Clojure Spec as examples https://clojure.org/about/spec In fact, I’d argue this provides a more rich specification than types as it focuses on semantic correctness.
-
Dynamic languages let you write much more direct code that’s easier for a human to read.
No more than any other paradigm, though, right? I don’t find Ocaml code any less readable than Python code. In most cases, the types aren’t even explicitly written in Ocaml so there is line noise or anything getting in the way.
I’ve actually been writing code in Python a bunch lately after spending a lot of time in Ocaml and I’ve noticed that I end up having to look at documentation fairly frequently, whereas in Ocaml I would generally just look at the type of a value instead. But the documentation is really hit or miss, so I’ve even found myself looking at the code for dependencies several times, I’ve only done that a few times in Ocaml.
YMMV, but your blanket claim that dynamic languages let one write code easier to read than statically typed languages doesn’t match my experience.
On top of that, ease of reading isn’t the metric I personally go by. It’s ease of refactoring. I’ve found that dynamic languages take a lot of effort to make refactoring safe, but in a language like Ocaml I have the compiler watching over my shoulder.
-
We clearly have very different experience here. I do find that Clojure code ends up being more direct than any static language I’ve used. I also find that it allows me to trivially express patterns that are challenging to encode using type systems. For example, something like Ring middleware https://github.com/ring-clojure/ring/wiki/Middleware-Patterns is difficult to do in a static context.
I do find readability is incredibly important when refactoring. I need to know what the code is doing and why to refactor it effectively.
-
You can accomplish that pattern in a statically typed language. Ocaml has a few implementations of that, one is hmap: http://erratique.ch/software/hmap
The only thing that isn’t exactly what I think you want is your key encodes the type of the value so you have to know the type you want to get out of a particular key.
I do find readability is incredibly important when refactoring. I need to know what the code is doing and why to refactor it effectively.
But how does that square with your response to @pyon in another subthread:
With a dynamic language it’s sufficient to show that the program behaves as expected for the specific use cases that you have
How do you express how the program should behave for the cases you have? Is it tests? What happens if your break the code for a valid case but that you didn’t write a test for? The problem I find when refactoring code in a dynamically typed language generally revolves around how hard it is to know what the code should do and if I change the code in a certain way (for example, make something that was an integer now a string), have I broken something users of the codebase depend on. That sort of refactoring is trivial in a statically typed language, just make the change and let the compiler tell you every other place that needs to change. IME, those changes are very difficult in a dynamically typed language.
-
-
-
I’m not missing that at all. My point is that the formalism often requires you to express yourself in a specific way that can be verify.
That’s a bit like arguing that seat belts are bad, because they make it hard to drive while standing upright in your seat. Doh!
The point is that there are hundred of thousands of people still walking on this planet that wouldn’t be around without seat belts.
Dynamic languages let you write much more direct code that’s easier for a human to read.
Let’s just disagree on that.
Take a look at Racket Contracts or Clojure Spec as examples https://clojure.org/about/spec.
The whole problem with these things is that they are optional. You can decide to use them in your own code, but if libraries are not using them you are in an uphill battle.
We have seen this problem times and times again with newer languages trying to graft on nullability information on existing libraries and spectacularly failing, despite the much smaller scope of the issue.
The main benefit of types is that they force everyone to follow their rules.
I can look at a random library’s type signatures and immediately know which things cannot happen.
-
If you use Design-by-Contract, you can do both. The Design-by-Contract preconditions, invariants, and postconditions are similar to static types where you’re bolting them on rather than being integrated in the language. Some languages, esp Eiffel and Ada/SPARK, integrate them. I doubt Python etc support it so you’d be using some language feature, maybe just the OOP stuff, to do it. The precondition checks especially would guarantee certain things about your program before you even run it with people using your library knowing more about it just looking at them. Invariant or postcondition checks can be combined with property-based or purely-random testing to catch a lot of errors in a way that highlights exactly what failed.
Now, people can get these properties wrong. However, the literature of academic and industrial deployments strongly argue that they’ll catch vastly more implementation errors in development and maintenance phases than review or testing alone.
-
-
-
However, you have to know that the invariants themselves are correct.
And in a dynamic language we don’t even know what any of the invariants are, so I don’t see this response as damning of types. In Ocaml, the sort function for lists has the type:
cmp:('a -> 'a -> int) -> 'a list -> 'a listwhich is pretty lightweight, it’s not nearly as formal as the Idris one but it still tells me important things, like that the sort implementation cannot know anything about the contained type.Essentially it feels like you’re saying there exists no invariants worth checking at compile time. Is this an accurate summary of your stance?
-
However, you have to know that the invariants themselves are correct.
So long as an understandable logic, the experience of several decades in formal specification show people find errors in requirements, design, or implementation using them. Every case study has errors caught this way with most in industry who were just using their heads and tests before reporting a drop in defects after introducing formal specs. The specs themselves are about the what more than the how which focuses the mind for review or tooling for checks. The how is usually more complex with Idris especially being a heavyweight way to do things not representative of effort/reward ratio of typical usage of either static typing or formal specs.
Now, some of these specs can get pretty big. This varies from being limitations of the spec language to intrinsic complexity of the problem. The former is something they might also screw up on. The compiler might catch some but not all of those screwups. The latter represent the complex details the programmer must get right that are implicit in non-typed or non-specified programs. As in, such complexity is always there but just invisible to compilers, checkers, and maybe the programmer depending on skill. Then, making it explicit, it can be checked by any of those. The more you want to explicitly check, the more types/specs come with the given module. Again, there’s a spectrum of effort put in vs rewards gotten out that one can use depending on importance of module and their resource constraints.
-
-
-
-
In real life, programmers do not deliberately write unreadable code in either static or dynamic type systems, because that would be pointless. It is also possible to write dynamically-typed code that is unreadably dynamic if you aren’t immersed in the local idioms (I can point to a lot of mainstream Ruby examples!). So I’m not sure what point you’re trying to make. [edited due to premature post!]
-
I completely agree that you can make a mess in any language. However, my point was that static typing necessarily restricts the number ways you can write code to those that are statically provable. A dynamic language allows you to write a statement that is not accompanied by an exhaustive proof, and proving something is often much more difficult than stating it.
For example, Fermat’s Last Theorem states that no three positive integers a, b, and c satisfy the equation a^n + b^n = c^n for any integer value of n greater than 2. That’s a really simple statement to make, and to understand. Proving that to be correct is a lot more difficult. Even when such a proof has been found, only a handful of people in the world can judge whether its correct or not.
-
A dynamic language allows you to write a statement that is not accompanied by an exhaustive proof,
Yes, but that is overly categorical.
Most typed languages also do not require exhaustive proofs, in the form of the Idris example you posted. You seem to want to create a false dichotomy, between no types on one had, and a total formally verified technique on the other (which are cumbersome).
Most proponents of static typing here aren’t advocating for full dependent-typed/verified languages (most of which are still experimental!) capable of solving Fermat’s Last Theorem in the compiler.
-
-
Is heterogeneous data something you find yourself commonly working with? Even in a language like Python it’s generally considered good practice that all entries in your containers have the same type unless there is some way to know before hand what they will be. But GADTs make that work in a statically typed language just fine.
-
Yes absolutely. Most real world data tends to be heterogeneous in my experience. This is a perfect example https://github.com/ring-clojure/ring/wiki/Middleware-Patterns You can have middleware functions that update the request and response maps by adding keys relevant to that piece of middleware, or updating existing keys. This would be pretty much impossible to do using a static language, especially if you want to be able to write middleware libraries that aren’t aware of one another.
-
Linking to my response about HMap here: https://lobste.rs/s/n6eix9/rich_hickey_delivers_rationale_for#c_keqhja
tl;dr - it isn’t pretty much impossible.
Most real world data tends to be heterogeneous in my experience.
I guess you mean heterogeneous and not known a-priori? For heterogeneous data we have things like records which let you store different kinds of data in the same thing, but you know what it is before hand.
-
-
-
-
-
-
-
-
-
-
Clojure transducers https://clojure.org/reference/transducers are difficult to type for a general case since the result depends on the runtime type of the argument. These are a core mechanic in Clojure. Ring middleware https://github.com/ring-clojure/ring/wiki/Middleware-Patterns is another example of something that’s not really possible in a typed language.
-
-
-
Ring middleware functions can modify the map in any way. They can add keys, remove keys. or change types of existing keys. The functions are defined in separate libraries that aren’t aware of one another directly. I can add a dependency and chain the middleware libraries any way I see fit. How would you express this using row types?
-
They can add keys, remove keys. or change types of existing keys. … How would you express this using row types?
That’s exactly the functionality that polymorphic row types give you.
Concretely, in some imaginary type system
-- Consumes any row type addAKey :: { r } -> { newKey :: Foo, r } -- Consumes any row type with `oldKey` field removeAKey :: { oldKey :: Foo, r } -> r -- Consumes any row type with `key` field changeTypeOfAKey :: { key :: Foo, r } -> { key :: Bar, r }-
-
-
Linking to HMap comment, I think it does what the @Yogthos is referring to:
https://lobste.rs/s/n6eix9/rich_hickey_delivers_rationale_for#c_keqhja
-
-
-
-
-
-
-
-
A set of provable statements is necessarily a subset of all valid statements.
That runs counter to Gödel’s completeness theorem: a statement in a first-order theory is provable iff it’s true in all models. In programming language terms: a statement about a program is provable iff it holds in all conforming implementations of the language the program is written in.
Now, you might only care about one language implementation (presumably the one you’re using), but some of us care about portability and freedom from irrelevant implementation details…
-
This is actually a direct result of Godel’s incompleteness theorem. It’s also known as the halting problem in CS. For example, Scala compiler has a bug where it stack overflows trying to resolve types https://github.com/scala/bug/issues/9142
You’re restricted to a set of statements that can be verified in a reasonable amount of time.
-
Gödel’s first incompleteness theorem asserts every effectively axiomatized formal system sufficiently powerful to prove basic arithmetic facts contains statements that are neither provable nor disprovable. It says nothing about the “validity” of such statements, because GFIT is a theorem in proof theory, not model theory. In particular, by Gödel’s completness theorem, the Gödel statement, just like any other statement that is neither provable nor disprovable in a theory, is true in some models and false in others. Whether that is “valid” enough for you is up to you - I prefer to work with statements (programs) that are true (run correctly) in all models (conforming implementations) of a theory (programming language).
Also note that I’m not advocating types (in this discussion). But you have to prove your programs correct, whether you use types or something else altogether. “Using types is an inefficient way to prove most things I have to prove” is a legitimate objection - one that I agree with, even! “I want to get away with not proving what I have to prove” is not.
-
No, you don’t have to prove your programs correct. That’s the key difference. With a dynamic language it’s sufficient to show that the program behaves as expected for the specific use cases that you have. With a static language you have to write it in a way that the type checker is able to prove to be exhaustively correct.
-
With a dynamic language it’s sufficient to show that the program behaves as expected for the specific use cases that you have.
So you can exhaustively test the entire space of legitimate inputs? You must have a few dozens orders of magnitude more computing power available to you than I do.
With a static language you have to write it in a way that the type checker is able to prove to be exhaustively correct.
That’s not true. As a matter of fact, I don’t do that when I use statically typed languages. Types provide basic sanity checks (e.g., modules don’t peek into each other’s internal details), but the bulk of the program’s proof of correctness is written by me, using paper and pen.
-
Of course I wouldn’t. I’d validate data at the edges using Spec https://clojure.org/guides/spec Types are not the only way to provide basic sanity checks.
-
Judging from your replies, you seem to think I’m delusional about types, even though I have been very explicit about the limited extent to which types help me. I expected it to be patently clear from my previous statements that I’m not telling you to use types. You can, of course, use whatever you wish. What I’ve actually said is:
- You have to prove your programs correct.
- To prove your programs correct, you need to use some formal system.
- Gödel’s incompleteness theorems isn’t an excuse for not proving your programs correct.
- Types sometimes relieve you from a very tiny part of the effort of proving your program correct.
- There exist formal systems other than types.
Furthermore, I originally only intended to make the first two points.
-
I disagree with the idea that you have to prove your programs correct in a general case. That can be desirable in some situations, but it’s simply not a business requirement.
The result of Godel’s incompleteness theorems is that the type checker restricts the way you’re able to express yourself to a subset of expressions that can be proved in a reasonable amount of time by the type checker. My argument is that it can result in code that’s harder for a human to understand than code that can’t be machine verified.
I think we agree on the value of types, but not on the value of formal proofs.
-
The result of Godel’s incompleteness theorems is that the type checker restricts the way you’re able to express yourself to a subset of expressions that can be proved in a reasonable amount of time by the type checker.
You keep bringing in type checkers. Didn’t you get the memo when I said “Formalisms other than types do exist!”?
My argument is that it can result in code that’s harder for a human to understand than code that can’t be machine verified.
My experience is exactly the opposite. Types don’t write much of your proof of correctness for you, but they make the parts you have to write yourself much easier to write.
-
It certainly does sound like our experiences are very divergent here. You keep talking about other formalisms, but the point I make regarding the type checker apply to those just the same. Perhaps, you can elaborate on how you believe these other formalisms avoid the problem.
-
Humans and computers have different strenghts:
-
Computers are faster and more reliable than humans at performing long calculations, especially case analyses.
-
Humans are better than computers at defining usable abstractions and jumping between them, which requires insight.
Formal systems come in varying degrees of human- and computer-friendliness. At the two extremes, we have:
-
Cellular automata usually have simple and efficiently implementable definitions (computer-friendly). However, their evolution over time is very difficult to analyze and predict (human-hostile).
-
Higher-order programming languages (i.e., whose variables can be instantiated with abstractions) allow complex hierarchical structures to be directly expressed in them (human-friendly), but the fundamental operation in their semantics, namely variable substitution, is difficult to implement both correctly and efficiently (computer-hostile).
Notably, the first-order predicate calculus lies at a sweet spot in the middle. It is simple enough to be used by humans directly, not just to define things, but also to perform actual computations (although this requires training). At the same time it is a powerful enough metalanguage for higher-order object languages (e.g., set theory).
In my view (others might not agree), the key to making verification more tractable is to intelligently split the verification effort into parts that are relatively easy for a human to perform (defining hierarchical structures and abstraction boundaries, finding loop invariants and variants) and parts that are relatively easy for a computer to perform (performing mechanical consistency checks, exhaustive searches and case analyses). Different parts might have to be performed using different formal systems, designed to exploit the strengths of whoever has to use it directly.
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
Have some thoughts on this, but first of all:
I don’t really want to get sucked into this debate … users of untyped languages feeling insecure/defensive about it.
That’s very rude of you.
Okay, on to the meat of this. I think everybody has the same misconception about dynamic typing, including a lot of people who use dynamic typing: dynamic typing and static typing are not exclusive. All static typing means is that types exist at compile time. All dynamic typing means is that types exist at runtime. Languages can be both statically typed and dynamically typed (C#). Languages can be neither (bash). Each one has benefits and drawbacks, and it happens that each one’s drawbacks cancel out the other’s benefits, which is why a lot of languages are only one or the other. But since most dynamic languages aren’t also static (because drawbacks), people conflate it with untyped and end up arguing “static vs untyped”. It doesn’t help that a lot of languages don’t really explore the power dynamic typing gives you, precisely because they choose it to avoid the overhead of static typing.
Here are some dynamic language features that would be a lot to implement in non-dynamic languages:
- J’s array manipulations have very different type signatures depending on the dimensions of your arguments and the specified rank of the verb. That allows it to do extremely fast manipulations in extremely concise syntax: see here for examples.
- The two most popular data analysis languages, Python and R, both allow for interactive, partially executable REPLs. That makes them good for exploring data before committing to a transformation or full script.
- Python also uses prototype inheritance, letting you adjust all instances of an object at runtime (for example, to add logging or caching).
- Ruby has runtime metaprogramming, which is key for how the ActiveRecord ORM works.
- I get the impression SQL would be a lot trickier to statically type but that’s just a hunch.
Now, I’m not saying these are good or bad. In some contexts, these are good features to have. In other contexts, they’re less useful than static typechecking. But there is a tradeoff that happens and there’s never a free lunch.
-
dynamic typing and static typing are not exclusive
Right, and that’s true in Haskell too. The former should be preferentially minimized.
All dynamic typing means is that types exist at runtime.
Those aren’t types, they are tags, sometimes called class tags. Types have no representation.
I get the impression SQL would be a lot trickier to statically type but that’s just a hunch.
I maintain a type-safe SQL DSL library for Haskell and it has single-handedly improved my work more than learning or using Clojure ever did.
Python also uses prototype inheritance, letting you adjust all instances of an object at runtime (for example, to add logging or caching).
I have never ever needed this and anytime I’ve run into someone that did it’s because the tooling was failing them in other places. There are far more robust and maintainable ways to solve the same problems.
I was primarily and preferentially a user of untyped programming languages until I finally got to grips with Haskell. I still use it despite being quite comfortable in and having used Python and Clojure in production because the advantages have been profound. I get you don’t share in that belief, IME, it’s usually unfamiliarity or discomfort. I didn’t like feeling stupid at first either. I tried and failed to learn Haskell many times, that’s partly why I started writing a book years ago. I gave a talk about having failed to learn Haskell over the course of several years too. I assure you it was worth it in the end.
I see you getting stuck into your idiosyncratic definition of what a type system is with
socso let me cite Robert Harper. I think the point is elaborated in PFPL as well but I don’t remember it being very accessible.-
It seems to mostly be users of untyped languages feeling insecure/defensive about it.
I get you don’t share in that belief … I didn’t like feeling stupid at first either.
I see you getting stuck into your idiosyncratic definition of what a type system is
Are you able to have a discussion with someone without making fun of them?
If I said I was comfortable programming in languages with good static type systems, would you accept that it’s possible for someone to have different preferences without being objectively wrong, or are you going to say that my experience doesn’t count?
-
-
-
Technically (I know, I know) every language has a static type system.
In shell this system has only one type (string) and there is no need for a typechecker because and value can always be used anywhere a string can be used (since they are all strings). You have some arguments about shell functions (they’re not strings… but also aren’t values).
Bash has a bit more in it. Every value in bash has the type of anonymous union across string, list, etc. There’s still only one type in the static type system, so again, no typechecker.
In Ruby, there is still only one type, but now it has a name (RbValue) and it is a tagged union. (Again, reasonable people can have arguments about if it counts as a union since new tags can be introduced at runtime. Tagged union is the most obvious thing to call it, but you might want to call it Dynamic or some such, but this does not fundamentally change the description of the static type system).
-
All dynamic typing means is that types exist at runtime.
I’m not sure how this can be true:
A type system is a tractable syntactic method for proving the absence of certain program behavior by classifying phrases according to the kinds of values they compute.
With other words, types are used to reject programs according to the rules specified by the type system at compile-time.
There might be artifacts of types encoded into the compiled program to facilitate the execution of that program, but these runtime tags are are values, not types.
-
-
-
-
-
One guy makes a claim about something that’s widely contested. It’s popular in a subset of academia. Now, it’s undeniable truth to be reinforced for all time. Am I following that argument about Pierce correctly?
I’ve seen definitions like his or those we’re getting in this thread. I’ve also seen in formal methods community that some build things on a computational basis where some tech computes something that supports the logical system (eg type system). They use a mix of logic and computation to get things done with user defining the types as they go for their specific programs, proofs, and so on. That’s a lot more like developing with languages using dynamic, strong typing far as foundational concepts. Then, some say dynamic is a subset of static but they work so differently in how they’re used. Seem like independent lines of thought much like ALGOL68 vs LISP 1.5.
I doubt the matter is settled because Pierce or any subset of CompSci says so. That experienced programmers are still arguing about it hints at this.
-
I doubt the matter is settled because Pierce or any subset of CompSci says so. That experienced programmers are still arguing about it hints at this.
That’s a bit like arguing that the shape of the earth is not settled, because there are camps advocating for a spherical model and camps arguing for a flat earth model.
To cut it short, one is science, the other one is nonsense.
-
-
-
-
-
-
-
The rationale for this change: https://lists.fedoraproject.org/archives/list/devel@lists.fedoraproject.org/message/XW7V5A3RAWYCACU2ZMPA27ARRLIZUI37/
-
-
-
letting processes opt out of death on logout by other means
just to quote the article “This operation goes through PK, and thus can be configured in a more strict or more open policy, depending on whhat the admin prefers.”
-
-
-
-
-
Actually. I think he has a point. The default behavior should for sure be to kill all processes when the user logs out, unless it is explicitly the intention of the user to let the process running. However, maybe running e.g screen is the explicit intention of the user to keep it running after logging out.
Then again, it remains a bit of a hack, because after system reboot the process will not come back anyway, I’m thinking an IRC client in screen, so you need to have some kind of system service (cron?) to make it come back after reboot anyway. So “properly” registering an application as always running in the background (and also come back after reboot) would be a good way to solve this. So if systemd makes this easy as it seems it does, then I’d consider it a win! Not sure if it does that though. (See example 5: https://www.freedesktop.org/software/systemd/man/systemd-run.html#Examples)
One use case where this is a bit awkward, and what I regularly use, is when you quickly open a screen to perform a task that takes a long time and your session gets destroyed due to roaming or lost connection.
-
-
It’s not even “this hoop, not that one"—you need to jump through both hoops. They’ve just added a hoop.
-
-
-
-
-
was hoping to see https://www.nostarch.com/carhacking on that list ;)
-
That’s the first I’ve heard about this book, and i sounds very interesting. Have you (or anyone else) read it and can give a quick review of if it’s worth the purchase or not?
-
haven’t read it - the authors were on a podcast recently http://embedded.fm/episodes/149 probably depends on how serious you want to get into playing with these things - looks nontrivial & a bit of upfront cost.
-
-
-
If there’s any connection that I thought wasn’t mentioned in the article, is was the relationship between kalman filters and hidden markov models.
-
akbiggs
edited
7 years ago
|
link
| on:
Why learning Haskell/Python makes you a worse programmer (2006)
This is from 2006, not from 2016, if you check the comments. And C# has come a long way from what the author is describing here…modern C# code for #2 would look more like this:
string.Join('\n', mylist.Select(x => x.Description()).Where(x => !string.IsNullOrEmpty(x)))which does not lose much at all in terms of readability from the Python or Haskell versions, and could be simplified further with appropriate use of helper methods.
C# gained LINQ with 3.0, which added a bunch of extension methods to collections to write much more functional code with lazy evaluation. And since then, C# has continued to grow closer to feature parity with functional programming languages. I am particularly excited for the addition of tuples + record types + pattern matching in version 7, bringing in my favorite part of Haskell + Elm https://www.kenneth-truyers.net/2016/01/20/new-features-in-c-sharp-7/
C# brings together an awesome mix of functional + imperative programming with an amazing set of tools built behind it, and I think it would be a shame to dismiss it based on this outdated blog post.
-
I’m all for more features in C#, but the way they’ve decided to implement Pattern Matching irks me. C# Pattern Matching will be more like sugar around the switch statement; likely you’ll need to either provide a “default” case, or there won’t be any warnings/errors if you “forget” one of the cases, as opposed to languages with discriminated unions built in from the start. The lack of this feature means that you don’t really get any of the productivity benefits of using the compiler to direct where to fix things when the program changes (For example, when you add a new abstract method, you’re forced to update all of the subclasses"). the C# folks are considering an additional “match” keyword that might provide this, but it’s still up in the air.
https://github.com/dotnet/roslyn/blob/features/patterns/docs/features/patterns.md https://github.com/dotnet/roslyn/blob/features/patterns/docs/features/patterns.work.md https://github.com/dotnet/roslyn/issues/8818
This post also gets submitted every few years on hn https://hn.algolia.com/?query=why-learning-haskell-python-makes-you-a-worse-programmer&sort=byPopularity&prefix&page=0&dateRange=all&type=story
-
C# Pattern Matching will be more like sugar around the switch statement; likely you’ll need to either provide a “default” case, or there won’t be any warnings/errors if you “forget” one of the cases
Ah yeah, that’s a really good point, and a shame. I had forgotten that the switch statement didn’t throw a warning/error for “forgetting”.
-
-
-
You mean right now? https://goo.gl/GG26JX
-
jonschoning
7 years ago
|
link
| on:
Cloud Haskell: Erlang-style concurrent and distributed programming in Haskell
I kind of wish they’d remove the “Erlang-style” comment - there is just so much different in Could Haskell compared to Erlang/OTP that the comparison doesn’t seem quite apt, except in the most superficial way.. The comparison makes more sense in systems like Akka which feel a lot more like erlang.
-
I would call this style Fuzzing, more than property based testing, but it’s a valid technique
-
I don’t really think there’s a hard and fast line between fuzzing and property based testing. They’re two different points on a fairly continuous spectrum. It’s easy to add properties to your fuzzers (and every fuzzer is implicitly testing the very coarse grained property “it doesn’t crash”), and every property-based test is also intrinsically fuzzing your code.
-
-
I had a talk accepted by wroc_love.rb. Due to a tight planning schedule and time spent working out logistics, I have less than two weeks to go from acceptance to giving the talk. Pretty much everything else is on hold so I can prepare. The talk is a redefinition of the Liskov Substitution Principle for folks who know inheritance is a bad idea, giving insight to why Ruby struggles with NoMethodError on nil, why all the Rails Base classes include callbacks, and how to avoid “oh what the hell now” when you get an exception five steps from where the bug. It is my second Ruby talk secretly about Haskell.
I’m also in the point of talk production where I feel stupid for ever proposing it. It’s some combination of how repeating a word over and over makes it sound meaningless, plus being close to the topic for long enough that everything feels either trivial or in need of a dozen obscure caveats. Just too close to have any perspective on what the audience will find insightful and useful. The only way I know to deal with this is giving practice runs, which I don’t have much time for. I welcome advice from experienced speakers.
Work: Achieved one year as a 0x developer. :tada::sarcastic-tone-3:
-
Here’s a few posts I have bookmarked on LSP : https://apocalisp.wordpress.com/2010/10/06/liskov-substitution-principle-is-contravariance/ http://codeofrob.com/entries/my-relationship-with-solid---the-misunderstood-l.html
-
-
Haskell can be written using braces and semicolons, just like C. However, no one does. Instead, the “layout” rule is used, where spaces represent scope. The general rule is: always indent. When the compiler complains, indent more.
I didn’t know this, are there any major haskell projects that use braces and semicolons? What is the history behind this? Why would you want to support two different syntaxes?
-
I don’t know about projects that use explicit layout (braces & semicolons), but it’s useful for reducing ambiguity that could be introduced by the layout rules. The major utility I see is in machine-generated code; machine-generating the layout syntax is hard. Also it’s useful for small snippets where again you don’t have the luxury of layout on multiple lines - e.g. typing a one-liner into a repl. There might be some other historical reasons regarding Haskell 98 and having an unambiguous grammar for other potential compiler implementations.
-
Haskell can be written using braces and semicolons, just like C. However, no one does.
Except, funny enough, by Haskell’s creator Simon Peyton Jones, who loves using explicit layout everywhere in GHC.
https://downloads.haskell.org/~ghc/7.10.2/docs/html/libraries/ghc-7.10.2/src/TcDeriv.html#tcDeriving
-
-
Attempting to predict e. coli readings at Chicago beaches.
This person doesnt understand what Bad Faith actually means. Many people including GP are now using this term as a simple perjorative just to describe things that they don’t like or disagree with. Something similar has occured with the term ‘gaslighting’.
You should take that up with Albert Camus
compare https://en.wikipedia.org/wiki/Bad_faith vs https://en.wikipedia.org/wiki/Bad_faith_(existentialism)
I’m aware.