[elm-discuss] Idris holes - Thoughts for Elm?

[W. Brian Gourlie]

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

[Witold Szczerba]

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.

Post by W. Brian Gourlie
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*
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`.
Type Checking Succeeded!
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
For more options, visit https://groups.google.com/d/optout.

[Zachary Kessin]

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
ᐧ

Post by Witold Szczerba
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.

Post by W. Brian Gourlie
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*
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
Type Checking Succeeded!
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
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
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
[phone] / [phone] / [phone]

[Aaron VonderHaar]

If you haven't seen it already, https://atom.io/packages/elmjutsu has
support for creating case statement scaffolds (search the README for
"Insert case/of")

Post by Zachary Kessin
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
ᐧ

Post by Witold Szczerba
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.

Post by W. Brian Gourlie
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*
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
Type Checking Succeeded!
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
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
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
[phone] <+972%2054-234-3956> / [phone]
<+44%2020%203734%209790> / [phone] <(617)%20778-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
For more options, visit https://groups.google.com/d/optout.

['Rupert Smith' via Elm Discuss]

Post by Aaron VonderHaar
If you haven't seen it already, https://atom.io/packages/elmjutsu has
support for creating case statement scaffolds (search the README for
"Insert case/of")

Elmjutsu is also already making use of 'type holes' to infer types, but it
is hacked without explicit support from the compiler:

https://atom.io/packages/elmjutsu#infer-type
http://blog.jenkster.com/2016/11/type-bombs-in-elm.html

Some improved compiler support certainly wouldn't hurt.

[Aaron VonderHaar]

I think you could easily experiment with this style of development without
any syntax changes:

```
module Holes exposing (hole)

hole : String -> a
hole name =
Debug.crash ("unfilled hole: " ++ name)
```

and replace elm-make with:

```
#!/bin/bash

set -ex

elm-make "$@"
echo "Type Checking Succeeded!"
! grep -R "import Holes" src
```

The replacement `elm-make` script will fail if there are still holes to
fill.

Post by Witold Szczerba
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.

Post by W. Brian Gourlie
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*
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
Type Checking Succeeded!
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
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
For more options, visit https://groups.google.com/d/optout.

[Christopher Anand]

I know some programmers who define “undefined” in this way, so that type inferencing works but if you try to run your program without finishing it, you find out right away. :)

What this doesn’t address is the issue of working in a REPL where it would be better to run, but have the appropriate placeholder appear. Since much Elm work is front-end, it would make sense to put the appropriate “Under construction” template in place of the undefined in development mode, but turn them into errors in deployment mode.

We have started using holes with default values in teaching children, and so far so good. But we haven’t figured out case expressions yet.

Christopher

Post by Aaron VonderHaar
```
module Holes exposing (hole)
hole : String -> a
hole name =
Debug.crash ("unfilled hole: " ++ name)
```
```
#!/bin/bash
set -ex
echo "Type Checking Succeeded!"
! grep -R "import Holes" src
```
The replacement `elm-make` script will fail if there are still holes to fill.
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.
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
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
Type Checking Succeeded!
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.
For more options, visit https://groups.google.com/d/optout <https://groups.google.com/d/optout>.
--
You received this message because you are subscribed to the Google Groups "Elm Discuss" group.
For more options, visit https://groups.google.com/d/optout <https://groups.google.com/d/optout>.
--
You received this message because you are subscribed to the Google Groups "Elm Discuss" group.
For more options, visit https://groups.google.com/d/optout <https://groups.google.com/d/optout>.

['Dave Keen' via Elm Discuss]

I'm constantly faking this by putting:

someThing : Int

when I know that its not an Int, and then letting the compiler tell me what
it thinks it is supposed to be!

Post by W. Brian Gourlie
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*
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`.
Type Checking Succeeded!
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