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

2017-05-23 Thread W. Brian Gourlie 
This looks really cool! Unfortunately, being a plugin for a specific 
text-editor makes it quite limiting.

On Tuesday, May 23, 2017 at 12:45:20 AM UTC-5, Aaron VonderHaar wrote:
>
> 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")
>
> On Mon, May 22, 2017 at 10:06 PM, Zachary Kessin  > wrote:
>
>> 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 <> (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 > > 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 >> > wrote:
>>>
 For the uninitiated, Idris  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 elm-discuss...@googlegroups.com .
 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 elm-discuss...@googlegroups.com .
>>> 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

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

2017-05-23 Thread 'Rupert Smith' via Elm Discuss 
On Tuesday, May 23, 2017 at 6:45:20 AM UTC+1, Aaron VonderHaar wrote:
>
> 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.

-- 
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 elm-discuss+unsubscr...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

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

2017-05-22 Thread 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")

On Mon, May 22, 2017 at 10:06 PM, Zachary Kessin  wrote:

> 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 <> (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 
> 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 
>> wrote:
>>
>>> For the uninitiated, Idris  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 elm-discuss+unsubscr...@googlegroups.com.
>>> 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 elm-discuss+unsubscr...@googlegroups.com.
>> 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 <+972%2054-234-3956> / +44 203 734 9790
> <+44%2020%203734%209790> / +1 617 778 7213 <(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
> email to elm-discuss+unsubscr...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.
>

-- 
You received this message because you are

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

2017-05-22 Thread 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.

On Mon, May 22, 2017 at 4:11 PM, Witold Szczerba 
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 
> wrote:
>
>> For the uninitiated, Idris  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 elm-discuss+unsubscr...@googlegroups.com.
>> 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 elm-discuss+unsubscr...@googlegroups.com.
> 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 elm-discuss+unsubscr...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

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

2017-05-22 Thread 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 <> (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 
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 
> wrote:
>
>> For the uninitiated, Idris  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 elm-discuss+unsubscr...@googlegroups.com.
>> 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 elm-discuss+unsubscr...@googlegroups.com.
> 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 elm-discuss+unsubscr...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

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

2017-05-22 Thread 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.

On Mon, May 22, 2017 at 8:40 PM, W. Brian Gourlie 
wrote:

> For the uninitiated, Idris  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 elm-discuss+unsubscr...@googlegroups.com.
> 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 elm-discuss+unsubscr...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

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

2017-05-22 Thread W. Brian Gourlie 
For the uninitiated, Idris  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 elm-discuss+unsubscr...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.