I think it looks like a good idea. When I am adding new a feature, very often I have such a "holes", implementation details, which I do not want to code at the time of introduction, because I am not sure the final result of my changes. So, in order to make compiler happy, I am improvising with some dump implementation just to let me go further and at the end, I have to look for them and fix.
Such a "holes" would be great. On Mon, May 22, 2017 at 8:40 PM, W. Brian Gourlie <[email protected]> wrote: > For the uninitiated, Idris <http://docs.idris-lang.org/en/latest/> is a > pure functional language with a cutting-edge type system. However, this is > not another "We should make Elm's type system more advanced by introducing > X." Rather, I ran across a feature in Idris that seems like it would fit > nicely into Elm based on the fact that it further empowers the compiler to > assist the developer, and empowers the developer to iteratively develop > their code. This feature is called holes. > > *What are holes?* > > To put it succinctly, a "hole" is a hole in your implementation. Think of > it as an expression whose value is inferred based on surrounding context, > but does not actually produce a value. Holes allow our code to type-check > while freeing the developer from actually having to worry about > implementing every part of a function or program as they're writing it. > > *How does an incomplete program compile?* > > The short answer is, it doesn't. There would need to be a distinction > between a program that satisfies the type-checker, and a program that can > be compiled. For example, there may be a hypothetical command `elm-make > --check`. Or, perhaps, a special compilation mode that would convert holes > into Debug.crash statements. > > *A practical example* > > Consider the following code: > > describeTemp : Int -> String > describeTemp temp = > if temp > 100 then > "Really hot!" > else if temp < 32 then > "Freezing" > else if temp < 0 then > ?belowZeroMessage > else > ?catchAllMessage > > In the above example, we declared two holes using the syntax `?holeName`. > The theoretical output of the type checker may be something like: > > Type Checking Succeeded! > > You have 2 holes to fill: > > 8| ?belowZeroMessage > ^^^^^^^^^^^^^^^^^ > belowZeroMessage : String > > 10| ?catchAllMessage > ^^^^^^^^^^^^^^^^ > > catchAllMessage : String > > > The example is simple and contrived, so it's not necessarily > representative of a scenario where it would be useful, but for more complex > applications where you want to build things iteratively, with > type-checking, without resorting to returning dummy values or things like > `Debug.crash`, this would be very useful! > > I'd be curious to know what everyone else thinks. > > Brian > > -- > You received this message because you are subscribed to the Google Groups > "Elm Discuss" group. > To unsubscribe from this group and stop receiving emails from it, send an > email to [email protected]. > For more options, visit https://groups.google.com/d/optout. > -- You received this message because you are subscribed to the Google Groups "Elm Discuss" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. For more options, visit https://groups.google.com/d/optout.
