It’s a bold decision, but it’s well-argued. I wish them luck!
That opening argument does seem to miss out an important point about compiler rewrites though…
When a language gets rewritten in itself, it’s not just a proof that rewrites can be successful, or that “older + wiser = better”. It’s also a chance to put the language’s design and implementation to the test.
Think you’ve designed the best language for writing programs? Prove that design by using it to write your compiler! Maybe you’ll find it’s not as pleasant to use as you thought, and you’ll have to rework the design.
Think your compiler’s fast? Prove it by having to live with the compile times yourself! Maybe you’ll find it’s not as fast in practice as it is in benchmarks, and you’ll have to optimise the implementation.
In writing your language in itself, you’ll inevitably find problems that you missed, and that will force you to make improvements to your language. It’s classic dogfooding, with every improvement you make for yourselves translating into benefits for your users too.
Or to put that another way, a project this large will inevitably find problems with Zig, and any feedback will go into making Zig better. That’s good for programming in general, but is it a lost opportunity to have made Roc better? Perhaps… 🤔
There’s a flip side to this. By dogfooding your language this way, you will inevitably make its design more catered towards writing compilers. Which may not be what you want, depending on your target audience.
Yeah, there are some use cases that I’m just intentionally not targeting with Roc, and compilers are one of them.
That’s not to say I would discourage someone from writing a compiler in Roc if they want to, but rather that it’s a non-goal to make Roc be a language that’s great for writing a compiler in (except perhaps unintentionally). 😄
You are hereby challenged to explain exactly how to achieve folding of function bodies in vanilla vim. I am 0.7 sure that this isn’t actually possible without what amounts to writing your own regex-based mini parser, but I’d love to be proven wrong.
(Though, as with many things in the vast space of possibilities, it’s be useful if this incantation had a dedicated name such that people could start to even consider if they need it)
I’m not sure how precisely you want to fold function bodies vs other long noisy top-level constructs (structs, macro_rules), but if you’re satisfied with a 95% solution then vanilla vim has this:
Obviously the color scheme is quite a bit more Dwarf Fortress -ish than the nicely shaded screenshot in the blog, but that’s part of the charm of an ancient CLI tool.
No, level-based folding is not enough. It will incorrectly not fold any top-level functions, and it will incorrectly fold any inline modules, as far as I understand.
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.
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.
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.
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.
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.
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.
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
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' )
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 Intn. 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')
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).
It’s a bold decision, but it’s well-argued. I wish them luck!
That opening argument does seem to miss out an important point about compiler rewrites though…
When a language gets rewritten in itself, it’s not just a proof that rewrites can be successful, or that “older + wiser = better”. It’s also a chance to put the language’s design and implementation to the test.
Think you’ve designed the best language for writing programs? Prove that design by using it to write your compiler! Maybe you’ll find it’s not as pleasant to use as you thought, and you’ll have to rework the design.
Think your compiler’s fast? Prove it by having to live with the compile times yourself! Maybe you’ll find it’s not as fast in practice as it is in benchmarks, and you’ll have to optimise the implementation.
In writing your language in itself, you’ll inevitably find problems that you missed, and that will force you to make improvements to your language. It’s classic dogfooding, with every improvement you make for yourselves translating into benefits for your users too.
Or to put that another way, a project this large will inevitably find problems with Zig, and any feedback will go into making Zig better. That’s good for programming in general, but is it a lost opportunity to have made Roc better? Perhaps… 🤔
There’s a flip side to this. By dogfooding your language this way, you will inevitably make its design more catered towards writing compilers. Which may not be what you want, depending on your target audience.
True, true. 😅
Yeah, there are some use cases that I’m just intentionally not targeting with Roc, and compilers are one of them.
That’s not to say I would discourage someone from writing a compiler in Roc if they want to, but rather that it’s a non-goal to make Roc be a language that’s great for writing a compiler in (except perhaps unintentionally). 😄
I’m curious to know if there’s a vim plugin that does this.
I don’t think it needs a plugin. The built-in folding configuration options should do it. See
:help fold-foldtext. 🙂You are hereby challenged to explain exactly how to achieve folding of function bodies in vanilla vim. I am 0.7 sure that this isn’t actually possible without what amounts to writing your own regex-based mini parser, but I’d love to be proven wrong.
It is possible in neovim with tree sitter:
https://old.reddit.com/r/neovim/comments/1g41rjy/can_neovim_do_this_already_with_treesitter/ls0cf4b/
(Though, as with many things in the vast space of possibilities, it’s be useful if this incantation had a dedicated name such that people could start to even consider if they need it)
I’m not sure how precisely you want to fold function bodies vs other long noisy top-level constructs (structs, macro_rules), but if you’re satisfied with a 95% solution then vanilla vim has this:
Screenshot: https://i.imgur.com/Q5XwLJx.png
Obviously the color scheme is quite a bit more Dwarf Fortress -ish than the nicely shaded screenshot in the blog, but that’s part of the charm of an ancient CLI tool.
No, level-based folding is not enough. It will incorrectly not fold any top-level functions, and it will incorrectly fold any inline modules, as far as I understand.
Awesome intereview! I’ve never seen this youtube channel before but am definitely subscribing.
You can also get it as a podcast. Developer Voices and Software Unscripted are my two favorites in this area.
The host of Software Unscripted is on Lobsters: @rtfeldman
Not sure about Developer Voices.
Yup, I’m the Developer Voices host and I’m over here: @krisajenkins
👋🙂
Also, we’ve been on each others’ podcasts! [cue Spider Man meme]
Kris on Software Unscripted: https://podcasts.apple.com/us/podcast/hiring-functional-programmers-with-kris-jenkins/id1602572955?i=1000577649734
Me on Developer Voices: https://youtu.be/DzhIprQan68?si=gxdXbUXvRx48pbA_
Kudos! You did a great job interviewing Drew, I loved the curiosity you brought to the conversation and it seemed like you were genuinely interested.
Oh wow! I remember him from a talk about treating “effects as data.” 1 It’s definitely foundational to how I think about side-effects
This looks like Lua not Scratch ;)
😁
Kris, your podcast is amazing! Thank you for putting in the work :)
I can second that. There’s a lot of patience with guests letting them just describe things themselves.
Thanks! I’m glad if you’re enjoying them as much as I’m enjoying putting them together. :-)
Much love. Keep it up! 🙏
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.
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.
We’re using PureScript on our project at Standard Chartered Bank, along with a Haskell backend. It’s working really well. :-)
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. :-)
https://github.com/krisajenkins/regexfsm
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.
See also
git add -i.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.
And also, “Hey, I know part of this function. Tell me what this type of this term should be!”
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
--warnis 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:
Here,
ais 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 thatacan only possibly beList number. As such, it gives us this error: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')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
ashould be yet. This compiles fine.Then, we implement tally as you did -
which throws the error below:
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.crashthere , like this: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 guessedList Bool -> ( number, number' ). Which is the same as--warnat that pointNo, I mean if you do:
…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!
which’ll give you:
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. :-)
Submitted! :-D
Looks like the same approach used in Haskell’s HoleyMonoid library, which is also used to implement the excellent formatting lib.
Yes, it’s exactly the same, and directly inspired by the latter. :-)
Huh. I learned in college (15 years ago) that ADT stood for Abstract Data Type!
It still does. It’s an overloaded acryonym. Wikipedia lists five different computing-related articles for it. https://en.wikipedia.org/wiki/ADT
Is an ADT the same as a GADT?
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 typeslist aandlist aare equivalent. So are the types(λx. list x) aandlist a.Non-syntactic type equality is when the context influences type equalities. Let’s say in our scope we have a variable
cowith type(a ~ b), and we want to know iflist aandlist bare equivalent. The answer is yes, because we can usecoto rewriteatob. 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:
This is syntactic sugar for the following:
That is, when you create an
I, you have to supply a proof that the type variableaisInt. When you create aB, you have to supply a proof that the type variableaisBool. Etc. When you perform acaseon anExpr ayou then get the appropriate coercions in scope for rewriting. This is how the evaluator from the link works:When we perform a pattern match and the case is
I n, we return theIntn. But, we needed to actually return ana, per the type signature! No problem, we have a coercion froma ~ Inthandy 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 ~ bcan 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!)
Heh… Every example I can think of is 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 otherExprcases parameterized uponInt, rather than accepting anyExprcase (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.htmlinstead.Odd, it pulled the title correctly. I can’t change the URL, hopefully a moderator can jump in for us!
Fixed.
Ah I see the problem now. My blog wasn’t generating the correct
canonicallink in the header.