Re: [elm-discuss] Static Tzpe Checking in Elm vs Java

[Joey Eremondi]

I feel Elm with dependent types is probably just Idris. They seem to have
similar pragmatic philosophies, started from Haskell but have been
gradually breaking in ways to make things nicer, try to make good error
messages, etc. I'd love to see what TEA looks like in Idris though. And it
compiles to JS!

The big thing with dependent types is that they make inference impossible,
forcing annotations to be added at weird places. Error message generation
for dependent types is a nightmare: I'm doing my thesis on improving error
messages right now, but it is far from a solved problem. Likewise, you can
only write terminating functions, which adds a degree of awkwardness to
code, especially anything involving Integers. So a lot of Elm's strengths
would go away if it were to become a dependently typed language. Adding
these features in a controlled way that didn't hurt inference for the rest
of the language would be cool, but this is an open problem.

The thing with Elm is, a lot of the pieces were already there to be put
together. The typechecking of Elm is not revolutionary, and type inference
is a well understood problem. Elm put them together in a really clean,
practical, usable way, and targeted JS, which everyone needs.

Once you move into dependent types, there's less of a consensus on what
"next-generation" would look like. We know how to do type checking, but
(limited) inference, efficient checking, message generation, are all
undergoing research right now.

Hopefully I'm not sounding too much like a downer! I'm excited for what
dependent types can offer, but I think we're still a ways away from a
language that could be as clean as Elm.

On Thu, May 26, 2016 at 3:30 AM, John Orford  wrote:

> the first rule of Elm Type Club is you don't have to talk about types.
>
> adding them back into the mix'd prob be hairy for a lot of people - then
> again if you could do it in a v friendly way, there's lotsa benefits... I
> heard Matz of Ruby fame talk about something similar once.
>
> On Thu, 26 May 2016 at 12:17 Zachary Kessin  wrote:
>
>> I have thought about the idea of building a next gen elm with idris style
>> dependent types. To be called "Pine" of course ;)
>>
>> Mind you I have neither the skills nor the time to do such a thing. But
>> its a cool idea
>>
>> Zach
>> ᐧ
>>
>> On Thu, May 26, 2016 at 9:56 AM, John Orford 
>> wrote:
>>
>>> Thanks for the answers guys,
>>>
>>> Summing up, because the language is more restricted (doesn't have a lot
>>> of the Java kitchen sink semantics for example) the type system can more
>>> precisely describe what's going on in the program...
>>>
>>> Meaning that when you are type checking, it is a much more precise test
>>> of the program's internal consistency, leading to more robustness.
>>>
>>> i have been reading the Idris book, would be interested whether anyone
>>> has any comparisons on using coding dependently typed languages vs Elm or
>>> whatever.
>>>
>>> It must become overkill eventually! But I like how Idris feels so far,
>>> and I like the extra inference features you get from the extra type
>>> precision too...
>>>
>>> Zachary Kessin  schrieb am Mi., 25. Mai 2016 04:13:
>>>
 A major issue is the "Maybe". In Java a type can be null so you always
 have to check for that. WHile in Elm there is difference between "Maybe
 User" and "User". So the type system will prevent any form of null pointer
 exception.

 Zach
 ᐧ

 On Tue, May 24, 2016 at 10:06 PM, Joey Eremondi <
 joey.eremo...@gmail.com> wrote:

> Are you interested in the actual type checking algorithms, or just the
> type systems?
>
> Big differences of the type systems:
>
> * Elm has tagged union types, meaning that you can make a value that
> many have one of many types, and pattern match on its possible variants.
>
> * Elm has type inference, Java does not. When you declare a variable
> in Java, you need to know what type it is. There's no such need in Elm.
>
> * Elm has first-class functions, so variables can have type a -> b,
> and you can build arbitrarily complicated types using function types, put
> them in tuples, etc.
>
> * Java has classes, subtyping, inheritance, etc. Elm doesn't have
> that, because subtyping gets in the way of inference, and because it's not
> nearly as necessary when you don't have mutable data.
>
> There are many other differences between the languages, but they're
> not necessarily differences in the type system. For example, Java has
> mutable variables and Elm does not, but there are strongly typed 
> functional
> languages, like ML, which have mutable variables.
>
> As for the actual typechecking algorithms, Elm uses something like 
> Algorithm
> W
> ,

Re: [elm-discuss] Static Tzpe Checking in Elm vs Java

[John Orford]

the first rule of Elm Type Club is you don't have to talk about types.

adding them back into the mix'd prob be hairy for a lot of people - then
again if you could do it in a v friendly way, there's lotsa benefits... I
heard Matz of Ruby fame talk about something similar once.

On Thu, 26 May 2016 at 12:17 Zachary Kessin  wrote:

> I have thought about the idea of building a next gen elm with idris style
> dependent types. To be called "Pine" of course ;)
>
> Mind you I have neither the skills nor the time to do such a thing. But
> its a cool idea
>
> Zach
> ᐧ
>
> On Thu, May 26, 2016 at 9:56 AM, John Orford 
> wrote:
>
>> Thanks for the answers guys,
>>
>> Summing up, because the language is more restricted (doesn't have a lot
>> of the Java kitchen sink semantics for example) the type system can more
>> precisely describe what's going on in the program...
>>
>> Meaning that when you are type checking, it is a much more precise test
>> of the program's internal consistency, leading to more robustness.
>>
>> i have been reading the Idris book, would be interested whether anyone
>> has any comparisons on using coding dependently typed languages vs Elm or
>> whatever.
>>
>> It must become overkill eventually! But I like how Idris feels so far,
>> and I like the extra inference features you get from the extra type
>> precision too...
>>
>> Zachary Kessin  schrieb am Mi., 25. Mai 2016 04:13:
>>
>>> A major issue is the "Maybe". In Java a type can be null so you always
>>> have to check for that. WHile in Elm there is difference between "Maybe
>>> User" and "User". So the type system will prevent any form of null pointer
>>> exception.
>>>
>>> Zach
>>> ᐧ
>>>
>>> On Tue, May 24, 2016 at 10:06 PM, Joey Eremondi >> > wrote:
>>>
 Are you interested in the actual type checking algorithms, or just the
 type systems?

 Big differences of the type systems:

 * Elm has tagged union types, meaning that you can make a value that
 many have one of many types, and pattern match on its possible variants.

 * Elm has type inference, Java does not. When you declare a variable in
 Java, you need to know what type it is. There's no such need in Elm.

 * Elm has first-class functions, so variables can have type a -> b, and
 you can build arbitrarily complicated types using function types, put them
 in tuples, etc.

 * Java has classes, subtyping, inheritance, etc. Elm doesn't have that,
 because subtyping gets in the way of inference, and because it's not nearly
 as necessary when you don't have mutable data.

 There are many other differences between the languages, but they're not
 necessarily differences in the type system. For example, Java has mutable
 variables and Elm does not, but there are strongly typed functional
 languages, like ML, which have mutable variables.

 As for the actual typechecking algorithms, Elm uses something like 
 Algorithm
 W
 ,
 but a more advanced, constraint-based version which helps with speed and
 can actually accept a few more programs.
  Typechecking is based on unification.
 I can't speak too much about Java, but I imagine they're using
 something like abstract interpretation to typecheck.

 On Tue, May 24, 2016 at 10:49 AM, John Orford 
 wrote:

> Can someone /wittily/ sum up the experience of type checking in Java
> vs something pure like Elm?
>
> I feel purity, preciseness and descriptiveness is the main difference
> somehow...
>
> Java is too long in the distant past for me, but it's something I love
> about Elm and never really cared for in languages like Java etc.
>
> --
> 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
>>> Your CRM Link
>>> 
>>> Twitter: @zkessin 
>>> Skype: zachkessin
>>>
>>> --
>>> 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 

Re: [elm-discuss] Static Tzpe Checking in Elm vs Java

[Zachary Kessin]

I have thought about the idea of building a next gen elm with idris style
dependent types. To be called "Pine" of course ;)

Mind you I have neither the skills nor the time to do such a thing. But its
a cool idea

Zach
ᐧ

On Thu, May 26, 2016 at 9:56 AM, John Orford  wrote:

> Thanks for the answers guys,
>
> Summing up, because the language is more restricted (doesn't have a lot of
> the Java kitchen sink semantics for example) the type system can more
> precisely describe what's going on in the program...
>
> Meaning that when you are type checking, it is a much more precise test of
> the program's internal consistency, leading to more robustness.
>
> i have been reading the Idris book, would be interested whether anyone has
> any comparisons on using coding dependently typed languages vs Elm or
> whatever.
>
> It must become overkill eventually! But I like how Idris feels so far,
> and I like the extra inference features you get from the extra type
> precision too...
>
> Zachary Kessin  schrieb am Mi., 25. Mai 2016 04:13:
>
>> A major issue is the "Maybe". In Java a type can be null so you always
>> have to check for that. WHile in Elm there is difference between "Maybe
>> User" and "User". So the type system will prevent any form of null pointer
>> exception.
>>
>> Zach
>> ᐧ
>>
>> On Tue, May 24, 2016 at 10:06 PM, Joey Eremondi 
>> wrote:
>>
>>> Are you interested in the actual type checking algorithms, or just the
>>> type systems?
>>>
>>> Big differences of the type systems:
>>>
>>> * Elm has tagged union types, meaning that you can make a value that
>>> many have one of many types, and pattern match on its possible variants.
>>>
>>> * Elm has type inference, Java does not. When you declare a variable in
>>> Java, you need to know what type it is. There's no such need in Elm.
>>>
>>> * Elm has first-class functions, so variables can have type a -> b, and
>>> you can build arbitrarily complicated types using function types, put them
>>> in tuples, etc.
>>>
>>> * Java has classes, subtyping, inheritance, etc. Elm doesn't have that,
>>> because subtyping gets in the way of inference, and because it's not nearly
>>> as necessary when you don't have mutable data.
>>>
>>> There are many other differences between the languages, but they're not
>>> necessarily differences in the type system. For example, Java has mutable
>>> variables and Elm does not, but there are strongly typed functional
>>> languages, like ML, which have mutable variables.
>>>
>>> As for the actual typechecking algorithms, Elm uses something like Algorithm
>>> W
>>> ,
>>> but a more advanced, constraint-based version which helps with speed and
>>> can actually accept a few more programs.
>>>  Typechecking is based on unification.
>>> I can't speak too much about Java, but I imagine they're using something
>>> like abstract interpretation to typecheck.
>>>
>>> On Tue, May 24, 2016 at 10:49 AM, John Orford 
>>> wrote:
>>>
 Can someone /wittily/ sum up the experience of type checking in Java vs
 something pure like Elm?

 I feel purity, preciseness and descriptiveness is the main difference
 somehow...

 Java is too long in the distant past for me, but it's something I love
 about Elm and never really cared for in languages like Java etc.

 --
 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
>> Your CRM Link
>> 
>> Twitter: @zkessin 
>> Skype: zachkessin
>>
>> --
>> 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
Your CRM Link

Re: [elm-discuss] Static Tzpe Checking in Elm vs Java

[Zachary Kessin]

A major issue is the "Maybe". In Java a type can be null so you always have
to check for that. WHile in Elm there is difference between "Maybe User"
and "User". So the type system will prevent any form of null pointer
exception.

Zach
ᐧ

On Tue, May 24, 2016 at 10:06 PM, Joey Eremondi 
wrote:

> Are you interested in the actual type checking algorithms, or just the
> type systems?
>
> Big differences of the type systems:
>
> * Elm has tagged union types, meaning that you can make a value that many
> have one of many types, and pattern match on its possible variants.
>
> * Elm has type inference, Java does not. When you declare a variable in
> Java, you need to know what type it is. There's no such need in Elm.
>
> * Elm has first-class functions, so variables can have type a -> b, and
> you can build arbitrarily complicated types using function types, put them
> in tuples, etc.
>
> * Java has classes, subtyping, inheritance, etc. Elm doesn't have that,
> because subtyping gets in the way of inference, and because it's not nearly
> as necessary when you don't have mutable data.
>
> There are many other differences between the languages, but they're not
> necessarily differences in the type system. For example, Java has mutable
> variables and Elm does not, but there are strongly typed functional
> languages, like ML, which have mutable variables.
>
> As for the actual typechecking algorithms, Elm uses something like Algorithm
> W
> ,
> but a more advanced, constraint-based version which helps with speed and
> can actually accept a few more programs.
>  Typechecking is based on unification.
> I can't speak too much about Java, but I imagine they're using something
> like abstract interpretation to typecheck.
>
> On Tue, May 24, 2016 at 10:49 AM, John Orford 
> wrote:
>
>> Can someone /wittily/ sum up the experience of type checking in Java vs
>> something pure like Elm?
>>
>> I feel purity, preciseness and descriptiveness is the main difference
>> somehow...
>>
>> Java is too long in the distant past for me, but it's something I love
>> about Elm and never really cared for in languages like Java etc.
>>
>> --
>> 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
Your CRM Link

Twitter: @zkessin 
Skype: zachkessin

-- 
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] Static Tzpe Checking in Elm vs Java

[Joey Eremondi]

Are you interested in the actual type checking algorithms, or just the type
systems?

Big differences of the type systems:

* Elm has tagged union types, meaning that you can make a value that many
have one of many types, and pattern match on its possible variants.

* Elm has type inference, Java does not. When you declare a variable in
Java, you need to know what type it is. There's no such need in Elm.

* Elm has first-class functions, so variables can have type a -> b, and you
can build arbitrarily complicated types using function types, put them in
tuples, etc.

* Java has classes, subtyping, inheritance, etc. Elm doesn't have that,
because subtyping gets in the way of inference, and because it's not nearly
as necessary when you don't have mutable data.

There are many other differences between the languages, but they're not
necessarily differences in the type system. For example, Java has mutable
variables and Elm does not, but there are strongly typed functional
languages, like ML, which have mutable variables.

As for the actual typechecking algorithms, Elm uses something like Algorithm
W
,
but a more advanced, constraint-based version which helps with speed and
can actually accept a few more programs.
 Typechecking is based on unification.
I can't speak too much about Java, but I imagine they're using something
like abstract interpretation to typecheck.

On Tue, May 24, 2016 at 10:49 AM, John Orford  wrote:

> Can someone /wittily/ sum up the experience of type checking in Java vs
> something pure like Elm?
>
> I feel purity, preciseness and descriptiveness is the main difference
> somehow...
>
> Java is too long in the distant past for me, but it's something I love
> about Elm and never really cared for in languages like Java etc.
>
> --
> 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] Static Tzpe Checking in Elm vs Java

[John Orford]

Can someone /wittily/ sum up the experience of type checking in Java vs
something pure like Elm?

I feel purity, preciseness and descriptiveness is the main difference
somehow...

Java is too long in the distant past for me, but it's something I love
about Elm and never really cared for in languages like Java etc.

-- 
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.