Great article. At a hack night last night we took a crack at implementing some of it in PureScript. Turns out pretty nice. So far at least. :-)
Looks like the same approach used in Haskell’s HoleyMonoid library, which is also used to implement the excellent formatting lib.
Worst part? Being smack dab in the middle of two communities that are almost polar opposites. Many people coming to Elm from JavaScript want Elm to be more like JavaScript, and many people coming from Haskell want Elm to be more like Haskell. I see Elm as its own thing—neither “JavaScript enhanced” nor “Haskell simplified"—and I’ve sometimes struggled to engage constructively with groups who don’t see it the same way.
Pretty good point, I agree with it completely.
He’d probably get less guff if he’d quit slurring the Haskell community and their priorities so that they can position themselves (Elm) as the “good guys”.
Reminds me too much of (Bill) Clinton’s 1990s triangulation tactic.
Feldman’s Twitter feed is an exercise in bad faith.
I think the Elm community has a bit of an unfortunate backstory with the Haskell community. A few too many people have demanded typeclasses like it’s a necessary human right. A few too many have patronisingly explained what a typeclass is, as if Evan doesn’t even know Haskell(!) After a while that gets exhausting.
Unfortunately, because of that I think when someone who knows Haskell comes into Elm-land, the guard goes up. Often for good reason. As a result, on the Elm side that’s led to a bit of a culture of, “if you want to learn FP, you’re extremely welcome; but if you already know it, we’re not interested in your opinion.” Perhaps not that dramatically, but that’s my reading of the structure.
I totally agree with Richard that Elm’s under no obligation to be more like anything. It’s doing a great job being its own thing.
(For the record, I like typeclasses, but I don’t think they’re the only solution to the problem. I think Elm should solve the problem, but it isn’t as urgent as other things. And I believe there are more powerful languages in this space, but Elm’s still leading the field for shipping working SPAs.)
You do you, but I’m not going to entertain excuses for people encouraging ignorance and fear to enhance their own importance. The inauguration is bad enough, I don’t need this in my day job.
At NoRedInk, we ensure that all functions have a type signature. The rare exception is when we have a function inside a let binding. As a result, we never need type holes - every type of every function is plainly laid out to see. I can’t think of a time when working on production code when I’ve thought “oh, I don’t know what type this should be”.
On my personal projects, I usually start by defining the hard parts with a type signature and go from there. Type holes would be useful for the “in between” parts, the ones who sit underneath the hard part (e.g helper functions). That being said, using --warn
is plenty fine for me in those situations. There are other things I would much rather have first :)
I ensure all functions have a type signature too. I still find type holes very useful, for when I’m building up a new function, and for when I can’t remember the arguments to some other function I’m calling. (elm-oracle helps with the latter case, if & when it works. But type bombs always work.)
Holes are useful, but actually I think a better example is this:
sum : a -> Int
sum xs =
List.foldl (+) 0 xs
Here, a
is our type hole. How do I know it’s a type hole? Because it’s too generic - based on the usage of the function + : number -> number -> number
, Elm knows that a
can only possibly be List number
. As such, it gives us this error:
The type annotation for `sum` does not match its definition.
2| sum : a -> Int
^^^^^^^^
The type annotation is saying:
a -> Int
But I am inferring that the definition has this type:
List number -> number
Hint: A type annotation is too generic. You can probably just switch to the type
I inferred. These issues can be subtle though, so read more about it.
<https://github.com/elm-lang/elm-compiler/blob/0.17.0/hints/type-annotations.md>
Same in principle as your example of giving an incorrect type, but it also has the added advantage of telling you when your abstract signatures need to be exact, allowing you to start there and drill down into the real type as you implement the function.
I think you’re saying, “If you picked a simpler example, it would be easier to see what’s going on, and then you wouldn’t need type holes.”
I’m saying, when you can’t see what’s going on, that’s when type holes become useful. They can help you out of the fog.
That’s why I deliberately picked an example that’s more complex than sum
. I wanted something you can just about follow, but would appreciate some help with.
That’s not what I’m saying, actually :) With your example:
Now imagine as you are implementing tally, you just start by returning (number, number')
tally : a -> (number, number')
tally _ = (0, 0)
then we start to say, okay, great, now we want to start implementing the more complicated parts. We’re not sure how generic we can be, or what a
should be yet. This compiles fine.
Then, we implement tally as you did -
tally : a -> (number, number')
tally xs =
List.foldl
(\x ( trues, falses ) ->
if x then
( trues + 1, falses )
else
( trues, falses + 1 )
)
(0, 0)
xs
which throws the error below:
The type annotation is saying:
a -> ( number, number' )
But I am inferring that the definition has this type:
List Bool -> ( number, number' )
It’s the same principle as your type bomb - however, it lets you keep the variables free until they need to be more specific, rather than jumping straight to a outwardly wrong data type.
Excellent, thanks for clarifying my misunderstanding.
So my next question is, how do you do this for values in the implementation? If you didn’t know what (0, 0)
should be, what would you do?
You can wack a Debug.crash
there , like this:
tally : a -> (number, number')
tally xs =
List.foldl
(\x ( trues, falses ) ->
if x then
( trues + 1, falses )
else
( trues, falses + 1 )
)
(Debug.crash "")
xs
which’ll give you the same error as above! If you switch it out to a -> b
, then it’ll still tell you that it guessed List Bool -> ( number, number' )
. Which is the same as --warn
at that point
No, I mean if you do:
tally : List Bool -> ( number, number' )
tally xs =
List.foldl
(\x ( trues, falses ) ->
if x then
( trues + 1, falses )
else
( trues, falses + 1 )
)
(Debug.crash "")
xs
…how do you get Elm to tell you that Debug.crash ""
should be a ( number, number' )
? How do you get a type-hole at the value level?
Ah, gotcha - take it as an arg!
tally : a -> b -> c
tally init xs =
List.foldl
(\x ( trues, falses ) ->
if x then
( trues + 1, falses )
else
( trues, falses + 1 )
)
init
xs
which’ll give you:
2| tally : a -> b -> c
^^^^^^^^^^^
The type annotation is saying:
a -> b -> c
But I am inferring that the definition has this type:
( number, number' ) -> List Bool -> ( number, number' )
not quite perfect but it works
Hmm…if it’s all the same to you, I’ll stick with my approach. It’s less invasive. And I won’t give up hope for some compiler-level support. :-)
So we have the bottom type (⊥), this reads like it should just be implemented as the top type (⊤). While the top type is valid syntax in most programming languages (void *, interface{}, all of python, etc), it would be neat to have syntax for Elm and others that merely passes lexing/parsing, but does not pass compilation.
Am I misunderstanding what the top type is or what this post is complaining about?
Sort of. It’s not that the syntax is valid or invalid - the post desires a way to explicitly say “hey, I know part of the type of this function. Tell me what this type variable should be!”, which the compiler guesses for you based on the implementation of that function.
It still does. It’s an overloaded acryonym. Wikipedia lists five different computing-related articles for it. https://en.wikipedia.org/wiki/ADT
GADTs are what you get when you add non-syntactic type equalities to ADTs.
Normal equality on types is generally considered to be syntactical equivalence modulo beta-reduction. Beta-reduction is the reduction rule (λx. e) e' → e[x/e']
, aka function application. So for example, the types list a
and list a
are equivalent. So are the types (λx. list x) a
and list a
.
Non-syntactic type equality is when the context influences type equalities. Let’s say in our scope we have a variable co
with type (a ~ b)
, and we want to know if list a
and list b
are equivalent. The answer is yes, because we can use co
to rewrite a
to b
. Types like (a ~ b)
are called coercions, and if you have one in scope, that is proof of a particular equality.
Here is an example from the link that @taylorfausak posted:
data Expr a where
I :: Int -> Expr Int
B :: Bool -> Expr Bool
Add :: Expr Int -> Expr Int -> Expr Int
Mul :: Expr Int -> Expr Int -> Expr Int
Eq :: Expr Int -> Expr Int -> Expr Bool
This is syntactic sugar for the following:
data Expr a = I Int (a ~ Int)
| B Bool (a ~ Bool)
| Add (Expr Int) (Expr Int) (a ~ Int)
| Mul (Expr Int) (Expr Int) (a ~ Int)
| Eq (Expr Int) (Expr Int) (a ~ Bool)
That is, when you create an I
, you have to supply a proof that the type variable a
is Int
. When you create a B
, you have to supply a proof that the type variable a
is Bool
. Etc. When you perform a case
on an Expr a
you then get the appropriate coercions in scope for rewriting. This is how the evaluator from the link works:
eval :: Expr a -> a
eval (I n) = n
eval (B b) = b
eval (Add e1 e2) = eval e1 + eval e2
eval (Mul e1 e2) = eval e1 * eval e2
eval (Eq e1 e2) = eval e1 == eval e2
When we perform a pattern match and the case is I n
, we return the Int
n
. But, we needed to actually return an a
, per the type signature! No problem, we have a coercion from a ~ Int
handy in our scope, and can use that to rewrite, and thus make the example type check. The other cases work similarly.
Misc facts:
You can build coercions in languages with higher-kinded polymorphism. a ~ b
can be represented using a Leibniz equality ∀f : ⋆ → ⋆. f a → f b
.
Adding coercions to the type system makes type inference undecidable. This is why you generally have to supply a type signature on a function that uses GADTs.
Proving that two types are equivalent modulo a context is undecidable in the general case. Consider equalities between type functions, or, equivalently, between polymorphic types (a proof that ∀x. e = ∀x. e'
isn’t much different than a proof λx. e = λx. e'
)
For more information, System F with Type Equality Coercions may be useful.
GADTS are Generalised ADTs, so they’re a more flexible version of the same idea.
I’d like to do a follow-up on GADTs, but I want to find a good concrete example first. (One that isn’t a parser!)
I can’t say I fully grok GADTs, but conceptually they seem similar. This page does a good job explaining the differences between ADTs and GADTs in terms of a concrete example.
The way I understand it, all the “cases” in a regular ADT all have the same type. A GADT lets you define the “cases” such that different cases might appear differently to the type system, which allows you to make stronger guarantees (since you can, for example, abstract over subsets of the cases).
For example, in @cmm’s expression example, you can tell the type system that a particular Expr
“case” can only be built out of other Expr
cases parameterized upon Int
, rather than accepting any Expr
case (and hoping for the best).
The URL appears to be incorrect on the header link. It goes to the blog rather than the article, which is at http://blog.jenkster.com/2016/06/functional-mumbo-jumbo-adts.html
instead.
Odd, it pulled the title correctly. I can’t change the URL, hopefully a moderator can jump in for us!
Is anyone using Purescript? I’ve seen it mentioned a few times, but it seems to get even less attention than Elm or ReasonML, despite appearing to be older and more actively developed than either of those projects.
We’re using PureScript on our project at Standard Chartered Bank, along with a Haskell backend. It’s working really well. :-)
Don’t forget Fable :). I think purescript is probably extremely useful for an extremely small demographic. So there are probably a few people using it a lot.