I can't prove anything about programs other people will write, unless the language itself makes guarantees about the programs they can write. Culture doesn't help one iota.
1,638 karma · joined August 18, 2013
Values indeed don't have physical identities. The problem is that, when you use a language with pervasive object identities, the values you want only exist in your head, not in the semantics of the language you are using.
> Languages like C# allow you to throw off identity altogether with pass/store by value structs.
Please teach me how to define list or tree values in C#, sensei.
Really? https://ideone.com/mmQJGr
> And the distinction between primitives and objects in Java, for our discussion here, is irrelevant.
All it takes to disabuse you of this notion is a little bit of reflection.
> That Haskell can force purity via its laziness
This is not true. Purity is enforced via the type system.
> but not required for doing FP, just like how static types aren't required for doing FP either
Completely agree here.
> but they've been preceded by LISP and ML.
ML is a functional language. Scheme already forces you to squint your eyes a lot. Lisp is not a functional language by any stretch of the term's meaning.
Only by social convention. Not enforced by the language's semantics in any meaningful way. In fact, Java does not even allow the programmer to define custom values. All values are primitives or object identities. Note that so-called “value objects” will not fix anything.
A fundamental property of functions is so-called “function extensionality”. Two functions “f, g : Foo -> Bar” are equal if and only if “f(x) = g(x)” for every “x \in Foo”. In particular, this means that there should be no equality testing operator for functions, because function equality is undecidable.
---
OCaml at least has bona fide values. It allows you to implement procedures that evaluate interesting functions (i.e. value-to-value mappings), even if it doesn't typefully distinguish a special class of procedures that are syntactically guaranteed to evaluate functions.
F# and Clojure are lost cases, though.
As for Haskell's IO and IORef (or ML's ref), there is absolutely nothing wrong with the ability to implement procedures that do other things besides evaluating functions. The problem is when you lack the ability to express interesting functions, and the root cause is the lack of a sufficiently rich universe of values.
---
Your mention of purity completely misses the point. The ability to do traditional imperative programming is a feature, not a bug! The problem here is the inability to do functional programming. The reasons for this are technical, not cultural.
btw, variants of the lambda calculus do exist where some values (so-called “reference cells”) are object identities. But a value cannot be a lambda abstraction and a reference cell at the same time.
I've tried really hard (okay, for about five minutes), but couldn't find any account of the lambda calculus that includes the following features:
(0) variadic argument lists,
(1) object identities for absolutely everything,
(2) procedures that can be manipulated in ways other than applying them to arguments.
Are you really saying that all this time my understanding of the lambda calculus has been a lie?
Exactly. To which the following must be added: Functions are mappings from values to values. It makes no sense to try to do functional programming in a language whose semantics does not provide a rich enough supply of values.
> And an FP language is one that has features, but also a culture that encourage FP as the main paradigm for solving problems.
Culture matters very little. What really matters is what the language's semantics allows.
Proof: Use the loop invariant `0 <= index <= numbers.length`. The invariant holds before the loop begins because `index == 0` (established by you) and `numbers.length >= 0` (established by the implementor of the array type) imply it.
Inductively assume that prior iterations of the loop preserved the invariant and didn't perform any invalid indexing operations. Now, every time the loop's condition is evaluated, there are two possibilities: either `0 <= index == numbers.length` or `0 <= index < numbers.length`. In the former case, the loop terminates and no further indexing operations are used, establishing the claim. In the latter case, `numbers[index]` is a valid indexing operation, and the subsequent `index++` operation does not destroy the invariant, because, given the precondition `0 <= index < numbers.length`, the operation `index++` establishes the postcondition `0 < index <= numbers.length`, which implies the invariant.
---
Note, however, that in this case it would have been more efficient to use an iterator, because the iterator's implementation already packages this proof in a reusable way, so that you don't need to reprove it every time you write a loop similar to this.
You don't need much from your language, except for a formal semantics. But, even if your language of choice doesn't have one, you can stick to a subset of it that is easy to formalize: no first-class procedures (or things that can simulate them, such as dynamic method dispatch), no non-local control flow operators (e.g. raising and handling exceptions), no non-lexical variables, just statically dispatched procedures and structured control flow constructs (selection and repetition, i.e., pattern matching and recursion).
> When a bug occurs (perhaps because your tests did not anticipate every edge case) how do you determine where the problem code is located without a stack trace?
By reasoning about every statement's intended and actual preconditions and postconditions, i.e., predicates on the program's free variables. At some point, the intended and actual preconditions of a statement-postcondition pair won't agree. But this is unreasonably hard if you need to reconstruct these preconditions and postconditions completely from scratch.
Object states are mutable, of course. But they are not values. You can't bind object states to variables. If you use objects as proxies for values that exist in your head but not in in JavaScript's semantics, that's fine, so long as you keep in mind the distinction between what you wish you were using and what you are actually using.
Type inference demands some rigidity in the type structure of a language. You must have the right amount of polymorphism: the STLC has too little, System F has too much. If you want both type operators and type synonyms, then operators can't be applied to partially applied synonyms [0], because higher-order unification is undecidable. If you want subtyping, you also have to do it in a certain way [1]. More generally, the type language must have a nice enough algebraic structure to make it feasible to solve systems of type (in)equations, because that's how inference works.
Your post contains a link to a paper [2] that contains the following passage:
> In this paper, we present a way to achieve efficient sound gradual typing. The core component of this approach is a nominal type system with run-time type information, which lets us verify assumptions about many large data structures with a single, quick check.
I have no way to confirm this claim at the moment, but it seems entirely reasonable. Checking structural types requires doing more work. But it is this very structure that makes type inference possible and useful.
So, yes, it seems that inference and gradual typing will be difficult to reconcile.
---
Footnotes:
[0] http://cstheory.stackexchange.com/questions/32260/ (I am the author of this stupid question.)
[1] http://news.ycombinator.com/item?id=13781467
[2] http://www.cs.cornell.edu/~ross/publications/nomalive/nomali...
Wherever it makes the most sense for the algorithms you want to implement.
> interactions between components
Again, driven by the needs of the algorithms, and, most importantly, their proofs of correctness.
The semantics of a programming language is what it is, not what you want it to be, unless you explicitly choose a language that allows you to express exactly what you mean.
(0) without destroying the safety guarantees of typed code,
(1) correctly assigning blame, if a runtime type error happens, to the specific untyped part of the program that causes the error.
Common Lisp's optional types don't quite fit the bill.
Hence more work has to be done on expressing solutions to big problems as the composition of solutions to smaller problems. Which is fundamentally an algorithms problem.
> Current abstraction methods are subpar: they require inherent complexity, are language specific, and are not easy to change after you've using them (unless you have adapters on every part of the code base which in it's own right becomes a mess).
Programming languages exist to implement algorithms, which in turn exist to solve problems. If your language of choice is getting in the way to implementing the algorithms you need to solve problems, you have to switch languages, not anything else.
def mul(a,b,c,d):
x = a*c + a*d + b*c
y = a*c + b*d
return x,y
def fib(n):
a,b,c,d = 0,1,1,0
while n:
while n % 2 == 0:
c,d = mul(c,d,c,d)
n //= 2
a,b = mul(a,b,c,d)
n -= 1
return a
(0) Get an element from the producer. If the producer is depleted, exit the loop.
(1) Put the element into the consumer. If the consumer is saturated, exit the loop.
With mutual recursion, you can do something like:
(* Standard ML syntax. This can be easily adapted to other languages.
*
* Naming convention:
*
* is: input stream
* os: output stream
* il: input leftovers
* ol: output leftovers
*
* Input/output are as in C++'s input/output iterators. In fact, this
* code is essentially C++'s std::transform, except not retarded.
*)
structure I : INPUT_STREAM = ...
structure O : OUTPUT_STREAM = ...
datatype result = Depleted of I.leftovers * O.stream
| Saturated of I.stream * O.leftovers
fun first (is, os) =
case I.fetch is of
I.Cont (x, is) => second (x, is, os)
| I.Done il => Depleted (il, os)
and second (x, is, os) =
case O.store (x, os) of
O.Cont os => first (is, os)
| O.Done ol => Saturated (is, ol)
(0) Assume that input streams cannot be depleted.
(1) Assume that output streams cannot be saturated. This is what C++'s `std::transform` does.
(2) Use an ugly “break” in the middle of the loop.
A programming language designer can only do so much for you. If you cannot identify errors in your programs on your own, consider switching to a different career.
> And what about programming errors that your process and your language causes?
Rigorous reasoning cannot possibly cause any problems. Rigorous reasoning helps identify and fix problems more often than not caused by prior non-rigorous reasoning.
> Programming language design is all about interactions with humans
Humans who need to reason rigorously in order to do things right, hence need to be pushed in this direction.
As for cowboy programming, Java and C# don't support it all that well, and they are very popular.