Thanks for this Joey - good to hear stuff like this, putting things into perspective - hard to find in an easy digestible form.
On Thu, 26 May 2016 at 16:40 Joey Eremondi <[email protected]> wrote: > 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 <[email protected]> > 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 <[email protected]> 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 <[email protected]> >>> 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 <[email protected]> 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 < >>>>> [email protected]> 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 >>>>>> <https://en.wikipedia.org/wiki/Hindley%E2%80%93Milner_type_system#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 <[email protected]> >>>>>> 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 [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 >>>>> Your CRM Link >>>>> <http://yourcrm.link/?utm_source=email%20signature&utm_medium=email&utm_campaign=passive> >>>>> Twitter: @zkessin <https://twitter.com/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 [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 >>> Your CRM Link >>> <http://yourcrm.link/?utm_source=email%20signature&utm_medium=email&utm_campaign=passive> >>> Twitter: @zkessin <https://twitter.com/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 [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. >> > > -- > 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.
