Types
gist.github.com
gist.github.com
> In Idris, we can say "the add function takes two integers and returns an integer, but its first argument must be smaller than its second argument":
> If we try to call this function as add 2 1, where the first argument is larger than the second, then the compiler will reject the program at compile time.
> Haskell has no equivalent of the Idris type above, and Go has no equivalent of either the Idris type or the Haskell type. As a result, Idris can prevent many bugs that Haskell can't, and Haskell can prevent many bugs that Go can't. In both cases, we need additional type system features, which make the language more complex.
I really wish when people talk about dependently typed programming languages (e.g. Idris, Coq, Agda, ATS), they would mention the effort involved to get these compile time checks to happen.
These languages allow you to capture almost any program property you can think of as a type. Instead of being limited to saying function F "returns a number/list/string" like common type systems, you can capture arbitrarily complex properties like "F returns an even number", "F returns a permutation of the input list", "F always halts" or "F returns a proof of Fermat's Last Theorem". You don't get this for free and you have to help the computer verify these.
Proving F matches the type is arbitrary hard and is impossible to automated in general (e.g. the halting problem tells us we cannot always tell if a function halts). For example, consider the type "F returns a sorted permutation of the input list", where F could be an implementation of bubble sort, quicksort, merge sort, radix sort or something even more complex. Each algorithm will require a different and potentially complex proof and most of the time the programmer needs to help the computer find the proof. It's completely unlike what people are used to from type systems and is an even more massive leap than for someone moving from the type systems of e.g. C++/Java to Haskell.
I'm glad people are more aware of dependently typed languages but I feel the immense jump in how practical they are to use is severely overlooked.
It's perfectly possible to implement a sorting algorithm without proving that it actually sorts the input, or indeed returns a permutation of the input list at all.
In that sense, you can choose how much efford you want to put into it.
Sure, but my point is that any nontrivial property requires the programmer to write difficult formal mathematical proofs which is an activity completely unlike what you see in mainstream strongly typed languages (e.g. Haskell, OCaml).
Also, consider how when you start making use of generics in type systems by converting all you Object lists to String lists; you find you have to start adding generic types all over the place for any code that touches that code until the compiler errors stop. If you decided to capture permutations of input lists in a dependently typed language, the exact same thing happens except this time capturing that property for all your algorithms could be monumental task of writing complex proofs (unlike before where you're just labelling things).
So don't write the proofs then. Dependently typed languages don't require you to write proofs; they give you the ability to if you choose. Considering that it's impossible to write such proofs in OCaml or Haskell, it seems strange to complain that they're hard to write in a dependently typed language. "Hard" is strictly less difficult than "impossible".
My sole point is that when I see articles on here about dependently typed languages, the issue of how the proofs are generated and the challenges involved in doing this is overlooked almost every time. I think it's important these challenges are highlighted so people don't think dependent types are a magic wand that gives you safety with little effort.
In practice, most of the properties that a programmer (rather than, say, a mathematician using a proof assistant) would want to enforce mechanically (say, invariants of data structures) are expressible as first-order statements (lambda-bound variables are never applied). This strongly suggests that the ergonomics of dependent types could be significantly improved by deliberately limiting their expressive power. By the way, the idea isn't new: the Damas-Milner type system, which is most certainly known and proven technology, is a subset of System F-omega's type system for which type inference is possible, at the reasonable (IMO) price of not having higher-ranked or higher-kinded types. A dependently typed language with a first-order type level would benefit from reusing the basic architecture of a Damas-Milner type checker: a constraint generator and a constraint solver powered by a first-order unification engine.
Have you seen languages like DML (let's you capture linear arithmetic properties only and automates the proof of these)?
https://www.cs.bu.edu/~hwxi/DML/DML.html
> Dependent ML (DML) is a conservative extension of the functional programming language ML. The type system of DML enriches that of ML with a restricted form of dependent types. This allows many interesting program properties such as memory safety and termination to be captured in the type system of DML and then be verified at compiler-time.
What program properties are useful to capture and what properties you can mostly automate is a really interesting problem.
Yes. But what I have in mind is a little bit more ambitious. I want dependent types restricted to be parameterized by syntactic values (in the sense of ML's value restriction) of what Standard ML calls `eqtype`s. For example, correctly balanced red-black trees would be:
(* clearly eqtypes *)
datatype Color = R' | B'
datatype Nat = Z | S : Nat -> Nat
datatype Tree =
| Empty : Tree (B', Z, 'a)
| R : Tree (B', 'h, 'a) * 'a * Tree (B', 'h, 'a) -> Tree (R', 'h, 'a)
| B : Tree ('c, 'h, 'a) * 'a * Tree ('c, 'h, 'a) -> Tree (B', S 'h, 'a)https://www.dropbox.com/s/xmj7yv1i1moe0ag/Coquand2002.pdf
Drop in to #dependent on Freenode IRC, and let’s chat.
Only kidding! It stands for Satisfiability Modulo Theories https://en.wikipedia.org/wiki/Satisfiability_modulo_theories
“In computer science and mathematical logic, the satisfiability modulo theories (SMT) problem is a decision problem for logical formulas with respect to combinations of background theories expressed in classical first-order logic with equality. Examples of theories typically used in computer science are the theory of real numbers, the theory of integers, and the theories of various data structures such as lists, arrays, bit vectors and so on. SMT can be thought of as a form of the constraint satisfaction problem and thus a certain formalized approach to constraint programming.”
I'm not sure I'm any the wiser after that …
A notable building block appears to be SMT-LIB http://smtlib.cs.uiowa.edu/index.shtml
In practice you spend way more time writing proofs in these system then doing anything else. There is evidence that we don't need to limit the expressive power of our logics, just design appropriate automation for the logic. Lean, a new ITT based theorem prover from MSR, has been focused on building automation for type theory. It already has promising results that formal methods techniques can be scaled to type theory (see the website for more information on recent work).
What I'm saying is that I don't like this direction, because type inference is very important to me.
> Not to mention you can get pretty good "inference" in dependently typed programming languages just by designing an appropriate higher order unification procedure.
Such higher-order unification procedures must always be tailored towards specific use cases, since higher-order unification is in general undecidable. Effectively implementing a different type checking algorithm for every program I write doesn't feel like good use of my time.
What I want is a type system that is more honest about how much it can help me: it only promises to enforce properties expressible as first-order statements, but offers much better inference, and the remainder of my proof obligation is hopefully small enough that I can fulfill it manually.
> In practice you spend way more time writing proofs in these system then doing anything else.
Indeed, and that's what I'd like to fix.
On related note, what do you think about the Shen LISP approach where Sequent Calculus can be used for advanced typing? Does it have the expressibility and decidability benefits you described? Hadn't seen many specialists talk about it so still an unknown to me. If it does, I figure some default type systems could be created for a specific style of Shen and/or specific libraries. Or something similar done in a ML.
http://www.shenlanguage.org/learn-shen/types/types_sequent_c...
IMO, the topmost priority in a type system designed for programmers ought to be automation, not expressiveness. Programmers don't spend their time proving deep theorems. Most of what a programmer does is actually fairly boring, but it ought to be done correctly, reliably and within a reasonable time frame.
For library types, the most commonly used properties will have already been proven; you wouldn't have to write a proof that "sort" sorts a list any more than you'd have to write the sort function itself.
The computer can also be surprisingly good at proving these things in many cases. E.g. I was playing with the proof assistant Isabelle recently, and I tried to prove that given an int, a proof that twice that int is greater than 13, and a proof that four times that int is less than 29, then that int must be 7. I thought I'd have to fiddle around with induction on Peano numbers and the like, but nope, it could be proved with just a single "by arith".
Tactics are probably a usability improvement for mathematicians who are used to proving everything by hand. But for programmers used to type inference, they're a step backwards. Mathematicians typically prove much deeper results, but they do so at a much slower rate than programmers write programs.
It's unfair to just compare development time between tactic-generated programs in a dependent language with manually written programs in a non-depenendent language. The end result in the dependent language is much more valuable.
Seriously, Coq-style proof scripts are utterly unredable when they grow past a certain size. The only way to understand them is to replay them, so that you can see the intermediate hypotheses and goals.
Reminds me of the same kind of problem that arises in trying to understand the runtime behavior of nontrivial programs involving side-effects, mutable state, multithreading, etc. Sometimes the debugger is the only practical way to figure out what the program is doing. Add concurrency into the mix, and things can get tricky very quickly.
Dependently-typed programming and machine-assisted proof is still an emerging thing, and there is probably lots of room for exploring ergonomic improvements. It will be interesting to see where this goes.
In Agda, you are expected to write proofs in a functional style, similar to Haskell programs. There is a small amount of integrated automation, which helps you fill in holes in your proofs — however, the results are explicit proof terms, inserted at the right place in your program.
Systems which behave in this fashion have the de Bruijn criterion, as described in Geuvers (2009) “Proof assistants: History, ideas, and future”.
I have thought about it some time ago and came up with the following proposal:
http://matej-kosik.github.io/www/doc/coq/coq-trunk-proof-tre...
Of course, but, in any case, writing programs at the same rate mathematicians prove theorems simply isn't viable.
Sorting was just an example. Most proofs of nontrivial algorithms come with reams of hand written proofs. Happy to see examples that go against this though.
> The computer can also be surprisingly good at proving these things in many cases. E.g. I was playing with the proof assistant Isabelle recently, and I tried to prove that given an int, a proof that twice that int is greater than 13, and a proof that four times that int is less than 29, then that int must be 7. I thought I'd have to fiddle around with induction on Peano numbers and the like, but nope, it could be proved with just a single "by arith".
Doesn't that just fall into the Presburger arithmetic decision procedure? The problem is you can rarely tell when the proof assistant is going to complete the proof for you (e.g. you're fine if it's within Presburger arithmetic but not if it requires induction).
data Comp = Gt | Lt | Eq
sortBy : (a -> a -> Comp) -> List a -> List a
sortBy = ...
I know this, I'm simply pointing out that when you do decide to write a proof it can be a very challenging task (much harder than adding generic types into Java code for example).
So what?
Even proving that array indices are not accessed out of bounds within loops would be a considerable leap in the state of the art of industrial programming languages. For most cases (i.e. linear integer arithmetics), that's always automatically (dis-)provable. We have to start somewhere...
Mainstream languages will gain much more from better iterators than by a ton of effort that just proves your indexes are within bounds.
It's a super interesting and important area, I was just pointing out it was a challenging one with lots of open issues.
> In Idris, we can say "the add function takes two integers and returns an integer, but its first argument must be smaller than its second argument":
> add : (x : Nat) -> (y : Nat) -> {auto smaller : LT x y} -> Nat
> add x y = x + y
That's all well and good, if you know the values of x and y at compile time. Consider a program that reads x and y from STDIN. The user could provide an x that is equal to or larger than y (or could provide only one value, or values that are not numbers). I see no way to deal with that except to throw a runtime error. Is that what would happen?
In the case where the values are read from the external environment, first you would have to compare them before calling the function. The comparator would return either a proof that x <= y, or x > y. In the first case you plug that value into the `smaller` argument, in the second case it's your responsibility to signal whatever kind of application-specific error is appropriate (assuming x > y is some kind of erroneous condition).
It would be a type error. All the compiler would know is that "x" and "y" are strings/integers so it would tell you they were the wrong type. If you do a branch on checking they are the correct type, then in that part of the branch the compiler will know they are the correct type and allow "add" to be called.
Think about a Java program that takes a string input, converts the string input to an integer type and then passes this to a function that accepts integers only. If you just tried to pass the string to the function directly the compiler wouldn't allow it. Same thing but the type system is more expressive.
import Data.String
-- takes two integers, and a proof that x < y, and yields an integer
add :
(x : Integer) ->
(y : Integer) ->
(prf : x < y = True) -> -- require a proof that that x < y
Integer
add x y prf = x + y
main : IO ()
main = do
sx <- getLine -- read string from input
sy <- getLine -- read string from input
let Just x = parseInteger sx -- assuming int parse is ok, else error
let Just y = parseInteger sy -- assuming int parse is ok, else error
case decEq (x < y) True of -- decEq constructs a proof if x < y is True
Yes prf => print (add x y prf)
No => putStrLn "no prf, x is not less than y"
When checking argument prf to function Main.add:
Type mismatch between
x > y = True (Type of prf)
and
x < y = True (Expected type)
it's either a compile error or it's valid.
The key here is that `add` is not a function `Nat -> Nat -> Nat`, it is a function `(a : Nat) -> (b : Nat) -> LT a b -> Nat`. There are just some compiler features that allow you to avoid having to write out the full `LT a b` proof each time you want to add things!
data Nat : Type where
Zero : Nat
Succ : Nat -> Nat
Given two such values "x" and "y", how on Earth can we prove that "x < y"? What would that even look like?
Well, there's a really obvious case: we know that "x < Succ x", so we can define a value "Obv" which represents this:
Obv : (x : Nat) -> LT x (Succ x)
What about those cases where "x" and "y" differ by some other amount? We could define values for "x < Succ (Succ x)", "x < "Succ (Succ (Succ x))", and so on, but that's clearly redundant and inconvenient. Instead, we just need to spot that all of these fit the pattern "x < Succ y", where "x < y". This lets us argue by induction: if "x < y", then "x < Succ y", which we can represent using a value "Ind" like this:
Ind : (x : Nat) -> (y : Nat) -> LT x y -> LT x (Succ y)
data LT : Nat -> Nat -> Type where
Obv : {x : Nat} -> LT x (Succ x)
Ind : {x : Nat} -> {y : Nat} -> LT x y -> LT x (Succ y)
Values of type Nat include:
Zero : Nat
Succ Zero : Nat
Succ (Succ Zero) : Nat
Obv : LT x (Succ x)
Ind Obv : LT x (Succ (Succ x))
Ind (Ind Obv) : LT x (Succ (Succ (Succ x)))
In the case of "LT", these numbers start counting from one (since one number is not less than another if their difference is zero). If we define a similar type for "x <= y" it would count from zero, and the same can be done for ">" and ">=".
These types are actually really useful. They're also closely related to linked lists, vectors, etc. although they store dynamic information as well as static.
I assume this is all old hat to those with mathematical training, but I found it interesting enough to write about at http://chriswarbo.net/blog/2014-12-04-Nat_like_types.html
This is the "types as propositions, proofs as instances" Curry-Howard correspondence lightbulb: The type "x < y" is a proposition, and if you can find any z at all of that type, then z is a proof of the proposition. So by passing in such a z that has been verified to have that type, you've certified that x < y.
which has nullable types. Imagine this code:
fun useMessage(msg: Message) { .... }
val s: Message? = someSocket.readNextMessage() // Returns null if the socket has been closed.
useMessage(s)
if (s != null) useMessage(s)
Idris isn't quite the same because it's a lot more general and the proofs are explicit instead of being implicit in the control flow: Idris types don't change when you test them, you get given a proof 'object' instead. But the basic idea is the same; your program does something that proves something about the type of a runtime value and that data can be used to improve program correctness.
Before you could call "add", you would have to add a branch/condition to verify "x" and "y" met the pre-conditions. The compiler would then know from the context of where you called "add" that the pre-conditions were always met. As you couldn't guarantee the pre-conditions were always met, you would have a code branch that decides what to do when the pre-conditions aren't satisfied.
The important difference to other languages though is that the compiler enforces that you're never allowed to call "add" unless you know the inputs satisfy the pre-conditions.
y = readFromStdin
if(x < y) {
// in this scope, you have proven x < y
} else {
// in this scope, you have proven x >= y
}
Now, somewhere else in your code, you have something like:
x = readline()
y = readline()
add(x, y)
That won't compile because readline returns string and add expects integers. Somewhere between readline and add you'll have to convert the strings to integers, and that piece of code (not the add function) is the one that has to be concerned with things like the user entering "abc" where a number is expected.
As far as the add function itself is concerned, it will always be invoked with two integers; the burden of proof is on the caller.
A program like this should fail to compile! You can't feed two arbitrary numbers from stdin to the "add" function above. In order to make it compile, you'd need to add some logic that uses min/max to swap the values so x is less than y.
> A type is a collection of possible values.
A type is a proposition, and "This binding has one of these possible values" is merely one type of proposition. So a type is much more powerful than a simple set-based interpretation, even though this is how most people think about it.
For instance, in Haskell you can encode a region calculus that ensures prompt reclamation of file handles and other scarce resources [1]. The relations between nested regions to ensure correctness seems awkward to interpret as a set, but it's straightforward if you just think of types as a relation.
Most formal definitions/treatments of types I've come across do not apply to dynamic types at all; usually the typing formalism says nothing about dynamically typed programs/values other than giving them one big recursive type. What we would informally call "dynamic types" are then treated completely separately, e.g. via "tags".
While such distinctions are certainly useful, an introductory/broad-overview explanation like this seems to benefit without such complications/distractions.
I don't think misrepresenting types is the way to go. An introduction like I just gave seems simple enough, where a type is a proposition about a program, and you just then explain that most such propositions are "variable X may take on values from set Y".
It's important not to perpetuate the false notion that sets of simple sets of values suffice to explain types, because it entails the common and equally false notion that full test coverage in a dynamically typed language suffices to match the safety of a statically typed language.
Just because induction on some types is sound, does not entail that induction on all types is sound. Indeed it's not in general, even though it may be in specific languages.
(1) Induction on datatypes is a powerful tool for reasoning about programs in strict languages, and it's only possible when you regard datatypes as collections of values.
> I don't think misrepresenting types is the way to go. An introduction like I just gave seems simple enough, where a type is a proposition about a program...
chriswarbo's point is: That's one way to think about types. It's not the only way, or even the only valid way. If you're going to disagree with chriswarbo, simply ignoring his/her point and reiterating your own isn't a good way to do it.
Can you demonstrate that your definition is the only valid way to think about types? Can you demonstrate that all other ways are subsets of your way? Those would be useful replies that would actually answer chriswarbo.
> A type is a collection of possible values.
"Collection" doesn't necessarily imply "set"; perhaps the author chose this word on purpose to avoid such complaints? Would you also complain if a Web page giving an informal introduction to topology said "a space is a collection of points"? Keep in mind that in HoTT, types are spaces and points are values, and hence those two statements have similar meanings.
I know when I'm writing about technical topics, I often look for words which don't have a widely-used technical definition, since that frees me up to focus on what I want to talk about, rather than getting bogged down in the particulars of this-or-that preconceived notion. I could certainly imagine myself wanting to get across the idea of types "containing" values, and carefully choosing the word "collection" specifically to avoid the baggage associated with the word "set". Maybe the author did the same?
In such cases, I would much rather someone point out an existing field which is the same as what I describe ("Your idea of types as 'collections of values' sounds a lot like HoTT's idea that types are spaces of points"), rather than an existing field which is not what I describe yet uses a similar word ("Your use of the word 'collection' sounds a lot like 'set', which is a different theory without much relevance here")
I think it's still wrong, but let's get concrete in the more unusual type systems to check. What is the "collection of values" for a type in TyPiCal [1]?
What is the "collection of values" for substructural types, like linear types [2] or affine types [3]?
I don't think "collection", set-based or otherwise, can capture these types.
[1] http://www-kb.is.s.u-tokyo.ac.jp/~koba/typical/
[2] https://www.cs.cmu.edu/~fp/courses/linear/handouts/lintt.pdf
[3] http://users.eecs.northwestern.edu/~jesse/pubs/alms/tovpucel...
Simple enough for what?
And I don't see why a bit of pedantry about Haskell's type system requires rewriting an introduction that's expressive and actually simple, not just "simple enough" from a certain point of view.
We teach Newton's physics to children (and even many adults) even though they've been supplanted by later theories, not because we don't know what the correct answer is, but because Newtonian physics are much easier to grasp and because they still give a useful view of the world around us, even if they break down in the extremes. Why is this any different?
Did you even read my comments? I already listed one falsehood that pervades our industry because types are misunderstand in exactly this way: "It's important not to perpetuate the false notion that sets of simple values suffice to explain types, because it entails the common and equally false notion that full test coverage in a dynamically typed language suffices to match the safety of a statically typed language."
This is blatantly, perniciously false, no doubt leading many people to choose dynamically typed languages to their detriment, yet this is what a reasonable person could conclude from the definitions in this article.
Finally, Newtonian physics governs every interaction an average person will have in their lifetime. The analogy that types-as-sets will suffice for nearly every interaction with types that a programmer will have in their lifetime is simply false. The fact that some programmers don't go beyond their first introduction to types makes a wrong definition almost dangerously false, given how much of our society is run by software.
The types-as-propositions interpretation is a particularly useful one because it lets us take ideas from the field of formal logic and apply them to programming. But it is only one interpretation, and not a definition of what types are.
I don't think it's possible to give "type" a good, short definition. For me John Reynolds' definition comes closest: "Type structure is a syntactic discipline for enforcing levels of abstraction." But that's rather a mouthful, and not a good introduction to what types are.
> A type is a proposition, and "This binding has one of these possible values" is merely one type of proposition.
The type that an expression or variable has does not correspond to the proposition that that expression has a certain set of possible values! You're mixing the object-level (the language & its types) with the meta-level (assertions about the language). This is a total misunderstanding of Curry-Howard. Rather, the values an expression might take on can be interpreted as proofs of the corresponding proposition.
Right, I wasn't advancing the propositional definition as the only one, merely as one that sufficiently captures the generality, because the article's current definition of types-as-sets is insufficiently general.
As I stated in a comment on that gist, what types denote varies from one type system to another: https://gist.github.com/garybernhardt/122909856b570c5c457a6c...
The idea that types express propositions in first- or second-order logic about a program one is writing is sufficiently general for every programmer to understand the proper scope of type checking. Types-as-sets is simply false as an introductory concept.
Right.
> where every programmer in existence is using first-order and sometimes second-order logic.
I'm not so sure about this one. Perhaps by “programmer” you mean “every Haskell programmer”? Even then I'm still not sure. Are you counting “let's approximate `forall x. P(x)` with the large but finite conjunction `P(a) /\ P(b) /\ P(c) ...`” as “using first-order logic”?
Haskell programmers also use higher order logic, which is also common now in Java and C#.
I wasn't talking about types either. Most programmers I've talked to simply can't use formal logic.
Perhaps they have trouble abstracting the semantics from their preferred language and/or syntax, but that doesn't mean they don't grasp their meaning.
The pernicious conflation of subtyping and subclassing in common OO programming languages just compounds the confusion.
Subtyping = "A <: B, therefore I can start with an A, forget the details irrelevant to B, and just use it as a B."
Inheritance = "A inherits B, if I try to actually use it as a B, it promises to work. However, it might actually blow up in my face, because it was keeping its extra details secret from me and promising they wouldn't blow up."
Too harsh. Logic is hard for humans. Evolution has trained us to take lots of mental shortcuts, not to be perfect calculating machines. Even the most technically competent people rely on their intuition. What differentiates them from the rest of us is that they have trained their intuition to make it more reliable [0].
It's the job of a language designer to arrange things so that intuition doesn't mislead programmers regarding the meaning of language features. Before proposing a new feature, the designer must anticipate how programmers will think about code that uses this feature, and there better not be a mismatch between what programmers think the code means and what the code actually means.
> A inherits B, if I try to actually use it as a B, it promises to work.
There's nothing wrong with implementation inheritance per se [1]. It addresses a very common use case: you have a thing Foo, and you want to produce another thing Bar that's similar to Foo, with minor changes here and there. This describes accurately how many things work in real life. However, you can't assume that Bar can always be used where Foo is expected. Those “minor changes here and there” might have rendered Bar incompatible with Foo. Hence, “inheritance is not subtyping”. As stated above, it's the job of a language designer to anticipate this.
[0] https://terrytao.wordpress.com/career-advice/there%E2%80%99s...
[1] Other than the lack of mathematical elegance, but few things are mathematically elegant in life.
Yes, it is their job, by not allowing subclasses to be used as subtypes.
(0) Not directly mutating superclass fields. (Reading them is fine.)
(1) Not overriding non-abstract methods of the superclass.
One could also have an non-subclassing mechanism of implementation sharing, that might be declared something like this:
class Related does (method1, method2) like Base;
class Related does all except (method3) like Base;I'd be fine with something more compact for the default case of "steal all behavior except what is explicitly overridden", such as:
class Related like Base;(1) Do you think there would still be a use case for “extends”? If not, I'd rather drop it as well.
The most obvious is that it makes intent explicit in the case of multiple similarity (I prefer "similarity" to "inheritance" for non-subtyping implementation reuse.)
It might in some cases make sense to do this on an interface rather than (or in addition to) single method level; there's probably a lot to work out in the ergonomics of non-subtyping implementation reuse.
> Do you think there would still be a use case for “extends”?
Sure, classical subclassing (subtyping with implementation sharing) remains an important use case. It might be desirable to statically verify certain guarantees (some have been suggested in at least one subthread of this thread by another poster) to assure that the subtyping is reasonable, but even without such verification the use case remains important.
Keep in mind that similarity is explicitly intended to be a quick-n-dirty form of code reuse. If the programmer has enough time to refactor the code, he or she should probably factor out the common parts, and then use proper (subtyping) inheritance. In view of this, I don't think making similarity overly complicated is a good idea.
> Sure, classical subclassing (...) remains an important use case. (...) even without such verification the use case remains important.
It's precisely the lack of such verification that destroys the guarantees you can extract from Liskov's substitution principle.
I do see the attraction of the idea that all implementation sharing ultimately reflects something that can be expressed through a subtyping hierarchy adhering to the LSP, but I'm not 100% convinced that it is the case. Absent certainty on that point, I'd like to have a model of similarity that is workable when viewed as an ultimate, rather than interim, model.
Also, I think that this kind of explicitness (with similar syntax) is desirable for subtyping inheritance in languages that support multiple inheritance, so it keeps similarity in line with inheritance, with the distinction only in the relationship being expressed (so, while it may make similarity more complex, it keeps the whole language more simple but explicit.)
> It's precisely the lack of such verification that destroys the guarantees you can extract from Liskov's substitution principle.
I agree that static verification of sanity in subtyping inheritance reduces the problem of LSP violations (as, frankly, does non-static verification, such as testing frameworks using subtype relationships to automatically apply tests for supertypes to subtypes.)
The degree and type of verification (as well as other details like cherrypicking and support for multiple similarity) that is appropriate for these type of things really depends on the language. Extending Perl or Python (dynamic languages with multiple inheritance) to support similarity alongside inheritance is probably going to favor different tradeoffs than extending Java (static with single inheritance) to support similarity.
The LSP itself is never violated in a type-safe language. What's violated is the guarantees that you expected the LSP to buy you. For instance, Java doesn't promise about the meaning of non-final methods. If a programmer assumes such guarantees, the problem is with the programmer, not Java. If he wants such guarantees to hold, he has to use a different language.
Disagree. C++ added private inheritance for a good reason. There are scenarios when you want to inherit part of an implementation, but override some of the behaviour for code reuse without inheriting any kind of subtyping relationship.
There are also scenarios where you want to declare a subtype without inheriting any parent behaviour.
So ultimately subtyping is distinct from subclassing.
That's probably too extreme. Subtyping should just be explicitly declared rather than implicit when subclassing.
The nice thing about this definition is that it reveals why reflection renders a type system useless: it destroys the type system's ability to enforce abstractions.
Ehhh, it kind of is a definition. Think of it this way: a type system is a topology we lay over programs, with open sets representing observable (using finite computation) properties and closed sets representing deniable (using finite computation) properties. The finest such topology possible is the Scott topology, which can distinguish every single observable value and deniable property from every other: it encodes all the information you can have about a program without solving the Halting Problem.
Type systems, then, are coarser topologies over programs than that one, which group observably different expressions and traces into the same open sets, which are then called "types". When those types are guaranteed not to contain _|_, the divergent program, they can also be considered topological spaces, with the programs in them acting as points in the topological space.
Shouldn't that read "one kind of proposition"?
:p
Does this point of view leave out anything crucial?
That might be a simpler way of explaining it, since "proposition" is rather abstract. Or perhaps, a type defines the valid state transitions your program can undergo at any given point, ie. given the data in your program (the program state S0), the types of all of that data define a set of valid transitions to another data set (program state S1).
1 + eval(read_from_the_network())
> The unsatisfying solution used in practice is to give eval() the type Any, which is like Object in some OO languages or interface {} in Go: it's the type that can have any value. Values of type Any aren't constrained in any way, so this effectively removes the type system's ability to help us with code involving eval. Languages with both eval and a type system have to abandon type safety whenever eval is used.
No, you can give EVAL a returning type of any (T) but still make type inference work.
(+ 1 (eval (read)))
There is also a NIL type (bottom) which represent the empty set of values. If a function has a return type of NIL, it means that it does not return a value normally. This is the case for the ERROR function, or the (LOOP) expression.
What’s curious is that this is true in every language with general recursion/looping:
int f(int n) {
while (true) {}
return n + 1;
}
The type of “eval” can also be fully static; it can just return a type that you have to do case analysis or runtime type inspection on to use.
In Haskell, with a data type:
data Value = Integer Int | Text String | ...
eval :: String -> Value
foo = do
value <- read_from_the_network
let result = eval value
case result of
Integer n -> return (1 + n)
_ -> error "that was not an integer!"
eval :: String -> Dynamic
foo = do
value <- read_from_the_network
let result = eval value
case fromDynamic result of
Just n -> return (1 + n)
Nothing -> error "that was not an integer!"
Typeable a => Dynamic -> Maybe a
Yes, thanks for pointing that out.
> The type of “eval” can also be fully static; it can just return a type that you have to do case analysis or runtime type inspection on to use.
I'd say that's what type T stands for in Lisp, since you can then dynamically dispatch on the actual type of the value.
Yes! The problem is, we don’t have a static type system which would allow us to intensionally analyse syntax at runtime. See section 9 of Sheard (2001) “Accomplishments and research challenges in meta-programming”.
https://www.dropbox.com/s/pathrmr7rufkw1d/Sheard2001.pdf
If you’re interested in this subject, perhaps drop in to #dependent on Freenode IRC, or ping me on Twitter.
add : (x : Nat) -> (y : Nat) -> {auto smaller : LT x y} -> Nat
add x y = x + y
data Nat = Z | S Z deriving (Eq, Ord, Show)
data SNat (n :: Nat) where
SZ :: SNat Z
SS :: SNat n -> SNat (S n)
type family Compare (a :: Nat) (b :: Nat) :: Ordering where
Compare Z Z = EQ
Compare (S a) Z = GT
Compare Z (S a) = LT
Compare (S a) (S b) = Compare a b
type a < b = Compare a b ~ LT
type family (+) (a :: Nat) (b :: Nat) :: Nat where
Z + a = a
a + Z = a
(S a) + b = S (a + b)
add :: (a < b) => SNat a -> SNat b -> SNat (a+b)
add = ...C does not 'allow' you to do a lot of the things mentioned on this page, it just doesn't generally carry around all the information to check and make sure you don't. So the page is generally still right - it can be fairly easy to get memory-unsafe things past the compiler - though whether you want to blame the type-system or blame the compiler could be debated, probably a bit of both.
Reading past the ends of arrays is illegal, as is accessing a variable of one type through a pointer to another type. Some of these things will get checked or assumed by the compiler (And thus break code that does these things, and in some ways break them in subtle ways), but there's no guarantee that the compiler actually knows you broke the rules. This tends to be the main different from other languages like Java, where the compiler/run-time does carry around such information and thus can do such checks and does know you when you broke the rules.
With that said, while there are some things I don't like about the design of Rust overall, giving the compiler more information to be able to figure out the above is definitely one thing they did right in comparison to C. The problem C is approaching is that, even though compilers are getting smarter, enough code was already written before that was the case to result in breaking when you attempt to use 'smarter' compilers.
I disagree with saying it is 'allowed' by the type system, because a smart C compiler could throw out your code and refuse to compile it if you do such things, and in doing so would still be within the C standard. Some work has already been done on this front in `gcc` (And I would assume `clang`) - the issue tends to be that by doing this, you end-up breaking some older code that used to work fine. And since older compilers didn't enforce these rules, people aren't as aware of them.
If there's more than one C compiler, and they behave differently on this, then in practice, C has more than one type system.
I've played around with Coq a little and it certainly feels more like a proof assistant than a programming language. It was fairly confusing and unfamiliar, but interesting nonetheless. Something with slightly more traditional ergonomics might be easier to pick up.
The learning curve is almost vertical to be completely honest from personal experience. I find most tutorials are written by people with a strong background in logic, type systems and mathematics, so it's a struggle to rely only on your knowledge of mainstream programming languages as you're learning lots of new things at once (e.g. formal proofs, formal specifications, logic, pure functional programming).
It's a super interesting area if you can stick with it though so keep at it!
I'm a little used to this from Haskell, although I imagine the dependently-typed languages are even worse in that regard. Working through the Idris tutorial now and at least the syntax is familiar.
That's what I mean by the difficultly jump. Like when you go from C++ to Java or the other way around, there's a lot of familiar things to cling on to while you make the transition. With dependently typed languages, there's a massive pile of unfamiliar stuff so the steep learning curve is unavoidable really. Someone needs to write a "dependently typed programming for Java programmers guide". :)
[1] https://groups.google.com/forum/#!forum/idris-lang
[2] https://www.manning.com/books/type-driven-development-with-i...
EDIT: the pain of such a strict language, not necessarily idris in particular.
This is not entirely true in general. auto is only a best bet. It might not be able to prove something right and will fail. For example, if it has to recurse deeper than 100 constructors. In this case, the user of the function has to provide a proof himself.
See it as a bloom filter. if it doesn't fail, you're sure your function is correctly called. if it does fail, it might still be correctly called but the compiler just didn't have enough time to prove it. In that case a user needs to convince the compiler that he is right.
I find that this is a nice compromise that gets a lot of the benefits of static type systems (small, local errors as opposed to behavioural bugs, ability to express concepts and constraints) without the drawbacks (loss of interactivity, or inability to escape the type system when it's appropriate).
> without the drawbacks (loss of interactivity, or inability to escape the type system when it's appropriate).
One can absolutely have interactivity in a statically typed language, and virtually all statically typed languages support casting when you absolutely need to.
My second paragraph was only a personal take on what works for me, so YMMV, but nevertheless: I'm not arguing against static type systems in principle, but these are practical concerns rather than theoretical ones. I don't know of a mainstream static language that supports a fully dynamic REPL (Haskell's isn't great) and casting back and forth to `interface{}`, `Object`, or `Any` everywhere is a huge overhead compared to duck typing. I look forward to a future language solving those issues, but that's not the case today.
I guess I'd like to see a simple formalism.
> myself (and many others I know) being easily able to get high performance code when we need it.
That's true for a lot of languages. It doesn't make it Rust-level.
> I'm not arguing against static type systems in principle, but these are practical concerns rather than theoretical ones. I don't know of a mainstream static language that supports a fully dynamic REPL (Haskell's isn't great) and casting back and forth to `interface{}`, `Object`, or `Any` everywhere is a huge overhead compared to duck typing. I look forward to a future language solving those issues, but that's not the case today.
Shrug, not my experience. I don't know what you mean by "fully generic", but I've been very happy with the Scala REPL - I've never once thought "this would be easy in the Python REPL but I can't do it because of the type system". Casting is indeed a big overhead if you're doing it everywhere, but my experience is the cases where you need it are extremely rare.
It's not quite true that they must abandon type safety: rather, they must abandon a certain kind of compile-time type check. It's not unsafe to use eval or Any values (i.e., it won't crash the system); one must simply examine the Any value (at runtime, natch) and do stuff with it.
Type checking Idris is much simpler than Haskell.
That's true, but Haskell has come a long way since a direct comparison like that would make sense.
> I mean, this HN comments page alone has multiple threads where people don't think that the "x > y" proof example even works.
I think this is because people have some preconceived idea about what dependent typing is before they come to dependently typed languages. So, not only are they learning about dependent types, but they are also fighting their preconceived notions. That was certainly the case for me.
It's an interesting facet of the human condition; every time we learn a new tool, we have to be reminded that it's not magic.
Now, having become proficient, I have a better intuition for how to get my complex Idris programs to type check than my complex Haskell ones. Idris is actually simpler, it's not just about line counts.
Is it? How's that?
I'd already made the assertion that Idris was less complicated than Haskell.
All of this falls away in dependent type theory you can represent the whole language with a class of pesudo-terms. For example the core expressions can be captured by the below grammar:
term := x
| f x
| forall (x : Type), B x
| lambda (x : A), e
| Type
subset NonNegativeInt of Int where * >= 0;
sub fib(NonNegativeInt $nth) {
given $nth {
when 0 { 0 }
when 1 { 1 }
default { fib($nth-1) + fib($nth-2) }
}
}
The more practical part of the article is great. However, the theoretical part could use some works. Especially the terminology isn't actually clear.
Takes some example, what is "memory-safe" ? The only example makes it sounds like bound checking. And what does "no way to escape the language's type rules" mean? There are some usages of "valid program" and "invalid program" that makes my spider sense tingling as well.
> However, no dynamic language can match the speed of carefully written static code in a language like Rust.
> Any blanket statement of the form "static languages are better at x than dynamic languages" is almost certainly nonsense.
Those two quoted statements come from the article.
The section "Arguments for static and dynamic types" didn't mention a single reason why dynamic typing could be preferable over static-typing. It could at least have mentioned macro, or hand-waving claim that dynamic typing makes for prettier code at time (I think the author of python's requests library made that argument in one of the blog post).
I think the last part should be removed (ranking the language by their typed system power).
> There's a clear trend toward more powerful systems over time, especially when judging by language popularity rather than languages simply existing.
Well, it looks true since we didn't consider any dynamic language at all...
Focusing more on the "Concrete examples of type system power differences" would have been better for the article, I think. Something along the line of an example of Non-nullable type with something simple in TS, to optional/maybe monad, then dependent type that you can implement matrix multiplication (m * n) with (n * p) and got the type (m * p) back.
First and foremost, i don't think dividing people into these clear-cut "camps" is good for this discussion (and probably for most discussions too...).
Second, i very much doubt that the author is a purist of static typing, or even a strong proponent of it. He has a series of programming screencasts called Destroy All Software, and in most the episodes i've seen he uses Ruby, Bash or Python. So, unless he has dramatically changed his style since then, i don't think he has any problems using dynamically typed languages.
>> Any blanket statement of the form "static languages are better at x than dynamic languages" is almost certainly nonsense.
> Those two quoted statements come from the article.
I think author had in mind "ALL static languages are better at x than ALL dynamic languages" as a nonsense. He probably didn't have in mind that "A static language_ IS better at x than A dynamic language_" is a nonsense.
I can give you an example, from bitter experience.
In the original Pascal, the size of an array was part of the type of an array. There was no possible type for a variable-sized array. And you couldn't cast from an array of one fixed size to an array of another fixed size.
Well, we were trying to do a 2D numerical simulation on a grid, with the size of the grid being user-specified. The original version of the program used a linked list to simulate the array, since you could have an arbitrarily-long linked list. But this meant that, if the simulation was 60x60, to reference the cell directly below the current one, you had to follow 60 links to get there!
I replaced it with a 2D array of a fixed size, with the size being the largest amount we could fit into available memory (it was on an embedded system, so the amount of memory available was predictable). Of that, we used only the user-specified subset to do the simulation.
TL;DR: If you need to do something that's outside what's allowed by your type system, and there's no way to escape the language's type system, you're trapped.
* "double kilometerToMiles(double km) { return km / 1.6 }" here the types are of really low value, yet I have to type them in.
* a mutable list of generic and variable arity event handlers. Really hard to specify as a type (most languages cannot do it). Really easy to use.
* co- and contravariance and lists, the math works exactly opposite of intuition.
* when you change your mind on the types/arity beyond what your IDE can follow, it is a lot of low value work
* if your test suite has 100% coverage of arguments/return-value and field usage, you have type checked your program.
If I am going to write down types, they better be of value to me. Like types that are null or non-null, or tainted (from the user) or non-tainted. Or two numbers that are kilometers vs miles. Or only accessible under a certain lock or other preconditions. And be flow sensitive (kotlin style null checks), not make me write even more code.
But if you are a dynamic language, do be strong typed (no "1" == 1). Also be dynamic in arity, that is (part-of) a type. Don't be handwavy scoped, lexical scoping is probably the only predictable way to do scoping. Fail fast, like prevent spelling mistakes for non existing field names for example. And allow this to work: "2 * Vector(10,10)".
And from that perspective there is still quite some room for improvement in all classes of languages, I suppose, and good that there is lot of movement and experiments today.
I do agree that Java-style types aren't of much value. That catches few errors at significant cost.
Incidentally, right now this is a few positions above this posting: https://news.ycombinator.com/item?id=12350063
Better IDE support, a kind of self-documentation and increased performance come to mind. I know there are counter-examples for each of these points, but the general trend cannot be denied.
You shouldn't have to, and you wouldn't in say Haskell.
> a mutable list of generic and variable arity event handlers. Really hard to specify as a type (most languages cannot do it). Really easy to use.
You want the handlers to have types corresponding to the events they handle, right? I.e. a labelled product/coproduct (similar to HList). They do exist.
> * co- and contravariance and lists, the math works exactly opposite of intuition.
I don't understand the claim here?
> * when you change your mind on the types/arity beyond what your IDE can follow, it is a lot of low value work
In a well-designed language most of your functions will be generic, and the parts you have to change should only be the parts that your change actually affects. Obv. this ideal is not fully achieved yet, but we keep getting better at it.
> * if your test suite has 100% coverage of arguments/return-value and field usage, you have type checked your program.
Not true. That one example works for a given function does not prove the type is correct for all arguments. As a trivial example you could define a function like "def f(i) = if(i == 1000) "blah" else i". Typechecking would catch that immediately, but to catch it through testing you'd have to test every possible integer as input.
I would suggest though, that comparing haskell to javascript, is almost like comparing a train with an offroad bike. Which you choose when is a discussion at a whole different level.
As for the list of event handlers example. The point it is a trivial piece of code. Any jQuery plugin writer can do it. Yet the type math behind it is complex. Java cannot express it. Most languages cannot be generic in function arity so cannot express it. Spending time on it is not worth the trouble. And paying this penalty at API level, where ever user has to pay, is just a sin.
Some discussion from the dartlang on covariant lists: https://www.dartlang.org/articles/design-decisions/why-dart-...
The test suite idea was incorrect. Even 100% code coverage will not do. But for "normal" code, add reasonable amount of coverage. And any production runtime type error will be really surprising. And even when it does happen, the fix is clear and quick.
A personal feeling on this topic is that it is all tradeoffs. But it makes me really happy to see gradual typing gaining traction. So you can start on your offroad bike, but end on a well oiled train, where that is worth the tradeoff. So you don't have to choose up front. Perhaps when we can even get runtime guarantees on perf/object layout when the type checker is happy.
As the quote goes, dynamic typing is the belief that you can't explain to a computer why your code works, but you can keep track of it all in your head. If it's really hard to express in a given language then that's a problem with that language, but IME anything that's hard to express in statically-typed languages in general is a bad idea.
> And paying this penalty at API level, where ever user has to pay, is just a sin.
I'd say the opposite, because it's easy to cast away types when you don't need them, but it's virtually impossible to put type information back into a language that doesn't have it.
> The test suite idea was incorrect. Even 100% code coverage will not do. But for "normal" code, add reasonable amount of coverage. And any production runtime type error will be really surprising.
IME: For any given level of "I want all runtime errors to be at least this surprising", that level will be easier to achieve via types than via tests.
> A personal feeling on this topic is that it is all tradeoffs. But it makes me really happy to see gradual typing gaining traction. So you can start on your offroad bike, but end on a well oiled train, where that is worth the tradeoff. So you don't have to choose up front
IME it's ineffective - I spent years trying to get types working after the fact, but the trouble is that code that's 95% typechecked might as well be 0% typechecked. Every violation of typesafety needs to be visible right at the point where it happens if you're going to have any hope of correct code.
> Perhaps when we can even get runtime guarantees on perf/object layout when the type checker is happy.
That'd be nice. But it's going to take more advanced typing, not yes.
> "I want all runtime errors to be at least this surprising", that level will be easier to achieve via types than via tests
For the type of the values, yes, but you still need tests for the content of the values. E.g you can only index into arrays with integers, but can your code access the array out of bounds? So that level is implicitly achieved.
> but the trouble is that code that's 95% typechecked might as well be 0% typechecked
That is absolutely not my experience. Typed at module boundaries really helps, even is that is only 5% of the code. On the other hand, getting to 100% type checked can be hard in current gradual systems. Mostly because some code is hard to type, even though it works fine, and humans can reason about it fine. Though you might be right, it is probably better expressed in a more type sound way. (Unless it is parametrization on function arity that does you in, grr.)
But to me, unless you are coding in idris or such, types are like the derivative of your code. Yes they show the general "slope"; how it fits together. But it says nothing on the values that flow through it, or the correctness of the code. You still need tests, and the type checker is not much more than a spell checker. Its usefulness is not in dispute (though overestimated by some). Just that in most of todays popular languages, you pay a price that is not non trivial. The choice is a tradeoff.
So you create a path-dependent type for valid indices into a given array (or, more likely, use a safe way of expressing iteration so that you don't need to see indices directly). Yes you can check that your indexing is valid with tests, but it's more efficient to do it with types.
> That is absolutely not my experience. Typed at module boundaries really helps, even is that is only 5% of the code.
Maybe if they're enforced at those boundaries - does that happen? I'm thinking mainly of gradual typecheckers that are erased at runtime, which IME are useless, because a type error can easily propagate a long way before it's actually picked up, and you see an "impossible" error where something has a different type at runtime to its declared type.
> But to me, unless you are coding in idris or such, types are like the derivative of your code. Yes they show the general "slope"; how it fits together. But it says nothing on the values that flow through it, or the correctness of the code.
Not my experience once you get used to working with the type system. Anything that should always be true in a given part of the code, you make into part of the types. Make the types detailed enough that a function with a given signature can only have one possible meaning, and then any implementation of that function that typechecks must be correct.
But what if you could have `miles kilometersToMiles(kilometers km)`? Under the hood its the same old doubles but you would be able to catch errors such as the one that caused Surveyor failure [1].
e.g. Haskell has units[2] and dimensional[3] that allow you to do exactly that
[1] https://en.wikipedia.org/wiki/Mars_Climate_Orbiter#Cause_of_...
The most horrible argument in favor dynamic typing in my opinion. Test suits shouldn't be about checking if a return value is of expected type, that's ridiculous. It's implementing a type checker manually.
There are a lot of things statically typed languages can do to make types painless :
- (global) type inference (Crystal does that)
- co and contravariance, it is not limited to dynamically typed language
- optional parameters
- adhoc type declaration like in C# (ex {x:1,y:"a"} is a type).
- contracts
- pattern matching
- generics
- ect ... etc ...
I just dislike dynamically typed languages. Even interpreted languages should be statically typed IMHO. Again, there are multiple ways to make statically typed language painless when it comes to types.
Indeed and so they don't have to. When you have reasonable code coverage, it is really surprising to encounter type issues in production. And they are the easiest mistakes to fix. But the point is, runtime checks happen implicitly as you run the code. So no "implementing a type checker" needed ...
On the other hand my comment on when you get the equivalent of being fully type checked was incorrect. Even 100% code coverage will not guarantee it for some code.
I like both kind of languages, and use both. While you get some advantages in static languages, you do also pay a price in language semantics and effort. It is good to point that out, so we can continue making progress, like Crystal or latest C# (and latest F#!). There used to be a time when the mood was: Java is good for all, stop confusing us with your new languages.
This is absolutely false. Others have pointed this out, but types are much more general than runtime checks in dynamically typed languages. For instance, you can check at compile-time that your program doesn't have data races or deadlocks:
http://www-kb.is.s.u-tokyo.ac.jp/~koba/typical/
Or design a library in Haskell to ensure file handles and other scarce resources are promptly reclaimed:
http://okmij.org/ftp/Haskell/regions.html#light-weight
Neither of these are testable in dynamically typed languages. Static types are much more powerful than dynamic types, in general.
What about:
toMiles (Kilometers k) = Miles (k/1.6)
let x = Kilometers 5
print (toMiles x)
Anyway:
> Like types that are null or non-null, or tainted (from the user) or non-tainted.
That's Haskell.
> Or two numbers that are kilometers vs miles.
That's my example up there.
> Or only accessible under a certain lock or other preconditions.
Yep, Haskell.
> And be flow sensitive (kotlin style null checks), not make me write even more code.
That's emulating what people do in Haskell.
However, the "danger" for me lies primarily in implicit conversion. That is, Python vs Lua/JS/R. When writing large programs, some things happen implicitly and linting may not catch it.
Everything else besides implicit conversion just helps structure the programs in specific ways and helps speed them up.
For their `add` example, I imagine just having x<y somewhere is sufficient. But let's say I write a sorting implementation but the compiler can't quite figure out that it is correct. Is there a provided way to tell the compiler 'trust me, this property is now true'?
Also, I'm assuming the compiler has two classes of errors here: a counter example vs. unable to prove?
Can anyone point me to documentation on these (in Idris, preferably)?
If you wanted to prove that a list was sorted, you'd write another datatype:
IsSorted : Ord a => List a -> Type
(l : List a ** IsSorted l)
The compiler doesn't generally come up with counterexamples for you; with this style, if the proof isn't complete, it won't compile.
Ok, but do two collections with the same values always correspond to the same type?
A blue 5, and a red 5.
Five feet, or five inches.
I'm barely aware of adga adn other langs that are used for profs, but wonder how useful (and what danger ahead) could cause to design a language with this for more mundane purposes (like, for example, build websites, data manipulation, gui, etc)
However, despite all the flaws, wiki is reasonably helpful, and I doubt filling it with more opinions would be helping the case.