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.
