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.
