I reluctantly confess that, knowing nothing about Haskell, I was lost by the 4th diagram. Presumably if you know Haskell, the line "data Maybe a = Nothing | Just a" makes sense, but I can't parse it.
The definition states "For all types a, the data type Maybe a consists of 'Nothing' or 'Just a'", where the a in 'Just a' is a value of type a.
Nothing and Just are polymorphic constructors that create the values of any "Maybe a" type.
So if you take a concrete type, say String, you get a new concrete type called "Maybe String" whose values are Nothing, Just "Hello", Just "World", etc. For Maybe Int the values are similarly Nothing (polymorphism!) and Just 1, Just 2, etc.
Extra: 'a' can be any type so Maybe (Maybe Int) is a perfectly valid type, with values like Nothing, Just Nothing, and Just (Just 1). Something like that would be useful when retrieving a "possibly empty" value from a database: Nothing means it's not in the database, Just Nothing means it's there, but it's empty, and Just (Just x) means it's there and it has a value.
e.g. loosely translating the idea of Maybe to C++ syntax (perhaps more familiar?) might give something resembling:
Maybe<int> x = Just<int>(30);
Maybe<int> y = Nothing<int>();
Given an arbitrary value of type Maybe<int> you have two cases to consider - either it is a "Nothing" which contains no further data, or it is a "Just<int>" which contains an int value.
You can think of the type Maybe<int> as being a "nullable int" type or perhaps a special collection of ints that can only contain 0 or 1 int value.
(beware: my knowledge of both haskell & c++ is not fantastic)
As for the syntax itself? It's called a tagged union. Just and Nothing are defined to be constructors for building values of type Maybe a. Just takes one argument (of any type) and Nothing takes no arguments.
Just "hello"
Nothing
data Maybe a = Nothing | Just a
Assume that a is the type String. Then Nothing is a value of type Maybe String but it's an empty box that contains no value. On the other hand Just "Hello, World!" is a box with the specified string inside.
Disclaimer: I'm not a Haskell expert. Feel free to correct me.
https://bitbucket.org/qznc/d-monad/src/1ec4ca36e46df1d0fce41...
foo (Just a) = bar a
foo (Just a) = bar a
foo Nothing = ...
The function "fromJust" which is equivalent to "getValue" is very rarely useful, and considered a smell: making that one of the primary ways to use your Maybe value is a very bad idea.
if (isNothing (m))
{ .. }
else
{ .. m.getValue() .. }
case m of
Nothing -> { .. }
Just val -> .. val ..
In Haskell, use of fromJust is considered a code smell, and is of course sometimes justified. But pretty rarely.
I actually did write the code that way the first time around. However, it ended up being a huge duplication of effort for a tiny amount of increased safety from type-checking. Literally, if I'm willing to move the checks of certain type-system-checkable properties to runtime this way, I can write 1/3 the actual lines of code.
The ideal would be to have data structures that are polymorphic over proofs of their properties, allowing the type-system to consider "unchecked AST", "generalized AST" and "specialized AST" as the instantiation of the same basic "AST" data type over three different proofs (or lack of proofs).
To restore nice, concise types, use a bunch of type synonyms.
While this is slightly cumbersome, I much prefer it over partiality.
Ideally, even this wouldn't be necessary, with structural records and variants that let you work with changing, precise types without having to declare a lot of duplicate types.
The other solution I'm thinking of in Scala (that doesn't involve Option[T].get, I mean) is to treat the properties I want "proven" as a set of methods over the data, built as a separate object or trait similar to how Scala represents type-class dictionaries. I can then write one data-structure that quantifies over the type of the proof-witness dictionary it stores as part of itself.
So when, for example, I want a fully-instantiated AST with no remaining "holes" to be filled in by static checking, I could write a function that only works on AST[FullyInstantiated]. Functions that don't care about the proof-witness are quantified over it.
It then takes a bunch of extra typing to construct the proof-witness instances, but when I'm doing that construction I will have the compiler statically checking that all types relied on by the witness are correct.
data Foo a = Bar a | Baz a | Qux a
data Foo' a = Bar a | Baz a
For one, this sounds like a perfect use case for OCaml's polymorphic variants[1]. I've always liked that particular feature. Honestly, most of the time, it seems like OCaml is the only language doing sub-typing correctly, especially in regards to type inference.
[1]: http://caml.inria.fr/pub/docs/manual-ocaml-4.00/manual006.ht...
Haskell does not have polymorphic variants, unfortunately. Happily, we can add them in as syntax sugar over multiparameter typeclasses[2]. The very first example in section 1.2 of this paper is particularly relevant here: they're showing how polymorphic variants make it easy to work with different kinds of ASTs. I don't think this is necessarily an immediately practical approach, but it's very interesting from a language design point of view.
[2]: http://guppy.eng.kagawa-u.ac.jp/~kagawa/PVH/PolymorphicVaria...
Your last example sounds like a prime case for using GADTs[3] (along with data kinds). You could write a type something like:
data Typed = Checked | Unchecked
data AST ∷ Typed → ★ where
Checked' ∷ Int → AST 'Checked
Unchecked' ∷ Int → AST 'Unchecked
Neutral ∷ Int → AST a
checked ∷ AST 'Checked → Int
checked (Checked' i) = i
[3]: http://www.haskell.org/ghc/docs/6.6/html/users_guide/gadt.ht...
This approach gives you relatively little syntactic overhead at the use site--the appropriate type is chosen based on the constructors you used. You also get nice type-safe pattern matching. I think it's a very good tool for this job. Perhaps you should consider using Haskell more one of these days ;).
Which I think I can actually do anyway just by declaring the polymorphism, or even using inclusion polymorphism on the witnesses to make Neutral a supertype of Checked and Unchecked (thus letting any function valid for Neutral ASTs operate trivially over both other kinds).
Polymorphic variants are indeed the ideal solution here, the problem being that those require either OCaml or a vastly improved subtyping system. I'm very slowly getting the logic worked out for the vastly improved subtyping system as a side-research project that's been going for years (but really got proper this past November as I started learning more of the logic behind type-theory and thus being able to reason much better about what I'm doing). For now, my own language would probably use structural-extensions and witness objects to do something like this, since it doesn't operate using the Vastly Improved Subtyping System.
At the very least, the GADT approach is not hard in Haskell. I don't see how it's any more difficult than the Scala approach. If anything, it's more natural: this is exactly the sort of use case GADTs were designed for.
The main advantage of using GADTs here is that they're simple and explicit. Sure, you could do the same thing with case classes, but it would be more awkward, and you'd really be rebuilding part of the same functionality yourself.
You don't really have to use data kinds in my example, but it makes the code nicer because you explicitly limit the types you can use as flags to 'Checked and 'Unchecked. You could have just made Checked and Unchecked empty types and stayed with normal kinds; the data kind approach is simply more elegant.
The GADT method also ensures that the pattern matching is always safe. It also preserves exhaustiveness checking, which is very nice. I'm not sure if the Scala approach can do this.
Another advantage over using witness objects (assuming I understood your idea correctly) is that you do not introduce anything new at the value level. 'Checked and 'Unchecked are only ever types, so the actual AST ends up being exactly the same as before just with a different type. I think this is a boon to clarity and simplicity. It also means that the use-site of the AST type doesn't change very much, if at all.
Really, the main idea is that this is very easy in Haskell, basically using a single simple abstraction: the GADT. Just being hidden behind a language extension does not magically make the concept any more complicated or difficult to use!
As an aside, if you want polymorphic variants, I don't see any reason not to use OCaml. It's a very nice language, and gets sub-typing right. All without sacrificing type inference.
Scala already has GADTs! http://lambdalog.seanseefried.com/posts/2011-11-22-gadts-in-... So yes, I use GADTs already.