Lambda the Ultimate

John, thank you for links to your blog!

I had some intuitive feeling, some thinks about types, I'm not scientist or mathematician, so I can talk about this only from developer/practical point of view.

I see some processes in Microsoft solutions: they borrow FP/Haskell ideas, but rethink them. I can only show some examples, my observations: nullable type is like Maybe but don't force you. Currently it raises warnings, but type-checking passes. Sure, reason #1 is backward compatibility, but IMHO not only. Example: I can have some information which I want to hardcode literally (as constants) in my application. And it will be organized as map/dictionary. Fine, but get of values will propagate 'Maybe'. I can use "fromJust" but it's not totally and leads to flame in reviews :) So, warning instead of type-check failure is possible approach in the language too: and C# does exactly this (I'm absolutely far from think that people in Microsoft are more stupid then in Haskell community ;)))

Another example: C# allows dynamic types. Hindley-Milner typing algorithm can infer types (without explicit signatures/types notations), in Python we have dynamic types, so what is the problem to hide types from programmer at whole? We have a lot of constructions on low (compiler/optimizer) level and programmer should not know about them: types can live at the same layer too (if they are necessary). For example, if function's argument type seems to expect Int and String then type can be automatically infer as Int|String, then compiler can check that programmer does not confuse both branches (one uses Int's operations, another one - String operations only), also no calls with other types, etc. Such algorithm can exist too and I don't think it's error: compiler can raise warnings about such cases but does not treat them as types violations. Mostly me, as programmer, is not interesting in types playing (HKT and other complex abstractions). I need types to help me: 1) refactoring 2) some kind of documentation. But all of this involves another problem: you can print Haskell code on the paper and you will not understand it: you need some IDE to check real type of the object: using operators are very generic and you don't know what means "handle" or "a" or "ws" (normal variable names in Haskell). You can expect good naming, but... :) _{Larry Wall, as linguist, found own solution: in English we have different "service" words, prepositions, etc. So, he uses sigils. Sigils looks fine (they exist in PowerShell even), but he introduces twigills also, which looks not so beauty ;)}

Another my observation was: strong types lead to super big set of types in the code. Most of them repeat external entities which are already strongly defined (as XML/JSON schemes, DDL, etc, etc). Microsoft offers solution with types providers - Haskell community does not understand the strongly types problems even.

Another my observation: types are "markers", "qualifier", but often we can not use them correctly/adequate to reality. Example, famous Path library of Chris Done. For example, it was implemented that Path can be Absolute|Relative (a) and File|Directory (b). So, type is "Path a b". And you can not have POSIX/NT paths in the same application :) which sure is totally wrong in enterprise applications. But more interesting is if we will have such possibilities, because in the case we need more parameters to Path. Also, I can imagine path-like manipulations with URLs. Also, there are NETBEU paths, etc. So, "Path a b" become "Path a b c d...". Or "Path (a,b,c...)", or "Path a::b::c..." (best case IMHO). So, rightly designed Path type will be complex and bad in real world usage. Which means for me: you can not use strongly types in most correct way, only some trade-off, cut-down version. Otherwise, application become very complex.

And sure my (sure very subjective) experience: bugs in Haskell programs are not less than in other languages, but more interesting is: code becomes more complex and puzzle-like, DSL-style programming is difficult in refactoring...

It's only intuitive feeling but IMHO strongly types direction is not very fine, I mean it has own serious problems in the real world.

Example with feet/metres is good: today it's easy solving with measure units of F#. There are Haskell libraries for measure units too, but they look not very good :)

Your idea about simplicity (clean semantics of method/function) is good and means easy to test it - it reminds me about Smalltalk... Small methods, TDD. But usually we write tests after code :(

Yes, idea of Path type is good, but my point was that in real world application I can have different kind of paths which can not be described only with 2 type "markers": relative/absolute and directory/file. Also my phantom type will be expanded to cover POSIX/NT path, NETBEU paths, etc. And when I think about path-join I see cases:

Path Posix Abs Dir -> Path Posix Rel Dir -> Path Posix Abs Dir

Path Posix Abs Dir -> Path Posix Rel File -> Path Posix Abs File

Path Posix Rel Dir -> Path Posix Rel Dir -> Path Posix Rel Dir

Path Posix Rel Dir -> Path Posix Rel File -> Path Posix Rel File

Path Nt Abs Dir -> Path Nt Rel Dir -> Path Nt Abs Dir

Path Nt Abs Dir -> Path Nt Rel File -> Path Nt Abs File

Path Nt Rel Dir -> Path Nt Rel Dir -> Path Nt Rel Dir

Path Nt Rel Dir -> Path Nt Rel File -> Path Nt Rel File

Path Posix Abs Dir -> Path Nt Rel Dir -> Path Posix Abs Dir

Path Posix Abs Dir -> Path Nt Rel File -> Path Posix Abs File

Path Posix Rel Dir -> Path Nt Rel Dir -> Path Posix Rel Dir

Path Posix Rel Dir -> Path Nt Rel File -> Path Posix Rel File

Path Nt Abs Dir -> Path Posix Rel Dir -> Path Nt Abs Dir

Path Nt Abs Dir -> Path Posix Rel File -> Path Nt Abs File

Path Nt Rel Dir -> Path Posix Rel Dir -> Path Nt Rel Dir

Path Nt Rel Dir -> Path Posix Rel File -> Path Nt Rel File

And here we use only 3 classifiers: Posix/Nt, Rel/Abs, File/Dir. What will happen if I try to cover URLs manipulations with the same Path concept... :) Sure, we can generalize it: with type-classes (and to separate cases at run-time) or with type-level lists (and to separate cases at compile-time, for example) - lists because we can have more generic and more specific phantom types and lists, *may be*, will allow us to skip enumeration of all classifiers. But this example shows my point: classification of real world with types can be very tedious :)

I have feeling that strongly typing and theorem prove are good tools but not in enterprise where there are a lot of exceptions from some generic rules: exceptional cases are much more than some generic and elegant rules, business logic with their details eliminates pros of these methods.

To blame an operating system problem on types seems a bit of a stretch to me :-) windows clearly has a problem with paths, whereas Unix manages to get away with a single global definition. This is a good example of my point about the wrong abstraction causing complexity in the application.

If we see a path type as a contract between all the developers working on a project, agreeing what a valid path is, then when the paths on a system are complex of course the type will be complex too, but what alternative is there? You could write documentation to describe what a valid path is, but then it has to be intelligible (as human languages tend to be vague and full of different interpretations) and it's has to be precise, and it has to be kept up to date with the code. So it seems a formal language is required for the precision and universal intelligibility, and if you have a formal language why not get the compiler to check the code against it, to make sure the documentation is up to date. So it seems to me a type system is exactly what you need. Current day type systems may not be ideal, but that is a reason to improve them, not abandon them

You could use a simple disjoint sum type for the Path, so the type would always be 'Path' and you switch between the type-tags at runtime. This is still safer than putting all your paths in a string and expecting everyone who reads/writes the string to know what it means and what is valid.

In fact the argument against types is poor, because the alternative, of just expecting everyone to know what kind of paths are valid in some string, is complete chaos, and will almost certainly be a bug magnet in any application.

BTW, I like the idea of TDD, and I try to do it as much as I can, but the reality is that you want to write the program and not the tests and it is hard to keep going with it. Often the time to write mock-services and script UI interaction is significant, and it is easier to just ad-hoc test by starting the application and clicking. Automating testing of UI interaction is also tricky but not impossible.

I don't see why the path separator would need to be lifted into a type. A path is simply a list of path components, it's up to the file system abstraction to apply whatever separator is needed.

I even question making a distinction between relative/absolute paths and file/directory. In fact, I'm not even sure why you'd do this with paths anyway, and not proper handles. Only a directory type should support path lookup.

The complexity results from simply using the wrong abstraction.

NO! Tests are the WORST weapon. They're the method of last resort.

THINKING is the best weapon. Visual appearance is important.
The compiler's type checking. A sketch of a proof.

Writing tests is a good weapon. The tests themselves are not there to find bugs, they're their to reinforce confidence attained from the OTHER methods of assurance.

"if you Google "unit tests dont reduce bugs" you will find plenty of anecdotal evidence that what unit tests do is prevent regressions"

So they reduce *future* bugs. I have a suite of regression tests for my product and they are VERY good at catching changes that break things, be they fixes or extensions. In fact I have a rule: if it passes the tests, commit, if it doesn't don't. CI servers shouldn't store artefacts unless the tests pass.