Proposal: Type-First Development with Elm

[ThomasKagan]

The nice thing about elm type annotations is that they aren’t embedded within the definition. Eg:

myfunction : Int -> Int  
myfunction n = n + 1

as opposed to

myfunction n : Int -> Int = n + 1

This syntax has benefits for documentation, clarity, gradual typing, and so forth. But I see untapped potential for Type-First Development with this system. Just as it sounds, this allows the programmer to write the type signature without having to stub the implementation.

The way things are, writing just myfunction : Int -> Int causes a compiler error, asking for myfunction to be implemented. But the compiler could just as easily let me leave the type signature there, but enforce that I don’t call myfunction. Rather than wasting time stubbing, I’m free to build up my concept of a module just by how I think the types will interplay among its functions.

As a bonus, this naturally lets me build datastructures with the unimplemented function. Suppose I have the trivial data type type MyType = AFunction (Int -> Int). Then I could call AFunction myfunction and use this for other things, just as long as I don’t actually call myfunction anywhere in my code. This lets me focus on implementing other functions without having to come up with some suitable stub that I just have to hope I don’t accidentally call somewhere, perhaps misleading a test.

If Elm chooses to accept this suggestion, then Elm will be a language where you can
* Write just the implementation of a function
* Write the implementation of a function and then the type signature
* (new) Write just type signature of a function
* Write the type signature of a function and then the implementation
completing the last square of the 2x2 matrix.

[rupert]

I quite often code this way. I might write something like:

myFunction : Int -> Int
myFunction _ = 0

Or

myFunction : Int -> Int
myFunction _ = Debug.crash "not implemented yet"

If you just had a type signature, and no implementation, what behaviour would you expect at runtime if the function is called? I presume Debug.crash "not implemented yet" would be the most suitable choice; you don’t want unimplemented functions sneaking through undetected.

Stubbing in a Debug.crash by hand is no real hardship, and also gives me something to grep for, which a completely missing function definition would not.

[luke]

Exactly. And just one more point on this, since Debug.crash "something" unifies with any type, you can use it to stub anything without even listing the arguments

myFunction: Int -> String -> Bool -> { hello : World } -> (a -> b -> b) -> List a -> List b
myFunction =
    Debug.crash "type-driven development!"

[jwoLondon]

Currently if you mistype a function name in either the type signature or the function definition, the compiler flags the problem when the two don’t match. I find this quite helpful. Under the OP proposal that wouldn’t get caught. I favour @rupert and @luke approaches which have little cost in practice while supporting healthy type-first development.

[mattpiz]

I also agree on the fact that Debug.crash is very useful, and have used it extensively for this purpose. I could see though how not needing any implementation while the function is not in the call tree could be great. When I am just sketching some API, any additional text that clutters my visual space and attention is good to get rid of. Maybe there is a good idea for editor support if not language support.

[ThomasKagan]

I like that you bring up the point of visual space. A few have mentioned that the small amount of extra typing isn’t a big deal. But I think the main reason this idea appealed to me isn’t the saved keystrokes but the aesthetic of the page. I’ve seen a couple talks on functional programming that talk about groups of functions by showing slides listing their type signatures. I think it would be neat if those slides were valid elm because of their aesthetic appeal and concision.

[luke]

I want to treat this as an opportunity to talk about how I analyze proposals in preparation for and during core discussions . I’ll start by saying that I think that this is a good idea in the abstract and I totally accept the legitimacy of the justifications offered. I want to draw a major distinction between this idea and, like, a package that wraps jQuery or something. This is thoughtful and not, to me, in conflict with Elm’s philosophy.

Now, I can’t predict the future and Evan ultimately makes these calls, but I don’t think this is going to be implemented and here’s why:

There are many factors that go into considering an idea, but a decent way to do a quasi-objective evaluation of a new feature idea is to consider:

To what greater degree does the feature enable an Elm user to achieve the goals Elm proposes to help with beyond what is already possible?

This is budgeted against:

• the long term pedagogical cost of introducing a new thing Elm can do that people will learn and teach and think about and discuss
• the potential to impact other future changes that are currently under consideration
• the cost of implementation and maintenance

For this feature, we’ve already established it’s possible and reasonable (and pretty nice, IMO) to do type-driven development with Debug.crash. In a language without this possibility this might be a huge win, but we already have it so there’s no gain. Then let’s consider the aesthetic improvements. Is minimizing clutter for a specific style of development worth the default costs of a feature as listed above, and then is it worthy of prioritization among existing work? I don’t think so. The implementation wouldn’t be a big deal, but maintenance is more unpredictable. I don’t think there’s a huge risk of impeding future progress beyond the unforeseeable. There could definitely be a pedagogical cost, as error messages would have to be reconsidered and teaching materials that deal in type signatures would need to reflect the new behavior. It seems like a purely optional feature but I don’t think that’s really true in practice. New Elm users are bound to encounter it quickly and wonder what it means to be able to write a type signature with no definition.

All of the same goes for making nice slides.

Anyway, this isn’t like an official policy or anything. It’s just my approach to evaluating stuff and I’ve found it useful in synthesizing my opinions during core discussions.

Just to finish up on maybe more of an upbeat note,

Maybe there is a good idea for editor support if not language support.

I mentioned before that I don’t think this as a language feature is really an optional advanced feature in practice. But! If it were implemented as an editor feature then it would be truly opt-in and also have none of the other costs I talked about. Maybe a plugin could insert the Debug.crash calls in secret or insert them and automatically code-fold them so that the compiler is still happy with the contents of the file. It’s worth exploring! Like I said, I think this is a nice idea in general.

[ThomasKagan]

Thanks for your input here, @luke. I think you bring up a good point–prioritization among existing work. This feature certainly isn’t essential, and in that sense I think timing comes into play. Perhaps this feature could be reconsidered later in elm’s life cycle after it’s confident it has solved the problem it has set out to solve. The maturity of elm and its community plays an important role in considering features to implement, a point which Evan talks about in Let’s be Mainstream! IIRC.

To what greater degree does the feature enable an Elm user to achieve the goals Elm proposes to help with beyond what is already possible?

This quote, to me, reflects the sentiment that elm core is looking for practical and essential features surrounding practical and essential problems. I think this strategy makes sense for elm at this point.

What I ask is if these sorts of features targeting not-so-practical (theoretical) or not-so-essential (aesthetic) problems should be self-moderated. Is this discord looking for only the features submitters think have a chance at implementation in the real world, or is it to look for general ideas? Let’s say I have a couple other ideas along the lines of this sort of thing, looking more or less for how the elm community feels about them rather than with the intention of promoting it to implementation. Are those ideas worth posting here, or should I instead pitch them in, e.g., the #elm-discuss slack? In essence, does this thread belong here?

[rupert]

automatically code-fold them

That would be a neat editor feature - a button or keyboard shortcut to jump to a folded view of your code where you just see the type signatures. Perhaps if you click one of the folded signatures you then jump to that point with the code unfolded - would help with navigation around larger files.

[ThomasKagan]

In VSCode you can view and jump to all of the symbols in a file with a go-to-symbol shortcut. It would be awesome if the dropdown would show the type signatures next to the name of each symbol.

[Sidney]

It would be awesome if the dropdown would show the type signatures next to the name of each symbol.

elmjutsu does this! https://imgur.com/a/jBKdGHN

[alexkorban]

Yesterday I saw somebody tweeting that he is building something like that for VS Code:

jlengrand (jlengrand)

[MarkHamburg]

This is a useful idea and far from radical. After all, one can code in C and let the linker identify functions that are reachable in the call graph but not yet implemented. This is arguably better than relying on runtime exceptions from something like Debug.crash. That said, stub implementations, even if they crash, allow the rest of the code to get up and running.

Mark

[drathier]

I do this all the time. At work, I write the types of endpoints/functions of my go/js/python api’s in elm right away, so that the compiler can help me find cases I’ve missed, while I design the api. Super useful!

[ThomasKagan]

I know, right! I think drafting with elm’s type notation can help in any language

[rupert]

A small project that could be spun off the Elm compiler, is to write a cut-down version that just compiles modules and types. Once past the type checker these modules and types would be written out in a format that can be consumed easily, and on top of that a set of code generators would be written. These would generate stubbed out code in go/js/phython/java/whatever.