totally agree, it would also make it easier to have your editor fill in the
code for me
Lets say you have a type like this
type Direction = North|South|East | West
move: Pos -> Direction -> Pos
move pos dir =
case dir of
North -> ?rhs
South -> ?rhs
etc
What I would like is to write "case dir of" and hit <<tab>> (or some other
key) in my editor and have the case statement with holes filled in for me.
I think Idris does this already
Zach
ᐧ
On Tue, May 23, 2017 at 2:11 AM, Witold Szczerba <[email protected]>
wrote:
> 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.
>
--
Zach Kessin
Teaching Web Developers to test code to find more bugs in less time
Skype: zachkessin
+972 54 234 3956 / +44 203 734 9790 / +1 617 778 7213
--
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.
