Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

1ML – unifying ML into one language

mpi-sws.org

Post reply on HN
Print view View original

51–60 of 63 posts

Re: 1ML – unifying ML into one language

#51

Post by skrebbel »

chongli wrote: post #37
drudru wrote: post #13

I know this is not popular. I think ML has a clean syntax and simple but powerful semantics. I enjoyed coding in it. It just looks better than OCaml. Haskell is, I think, even cleaner, but there is a tendency for developers to explore the possibilities available in Haskell and then increase the complexity. It would be great to see the ML community unify and provide an offering that would give it the kind of support t…

explore the possibilities available in Haskell and then increase the complexity. I'd caution against referring to all such explorations as complexity. Complexity is a highly overloaded term in our field. Sometimes it refers to the number of steps a given algorithm takes to compute (as a function of the input). Sometimes it refers to the depth and breadth of a program's syntax tree as well as its tendency to branch ou…

What the...? You know full well what kind of complexity the GP refers to, and it's not cyclomatic or algorithmic complexity, and definitely not unfamiliarity.

Is this a new kind of HN trolling? Instead of directly disagreeing with an argument on it's merits, you call a commenter out on possibly ambiguous terminology and use that to dismiss the entire comment?

Your entire lecture is true, but it does not apply to the sentence you quoted at all. That sentence is about some Haskellers' tendency to sacrifice readability in favor of better static checks. He could've written "difficult to understand" instead of "complex" and his comment wouldn't have changed meaning and your entire comment would've been void.

Re: 1ML – unifying ML into one language

#52

Post by octatoan »

andolanra wrote: post #46
rtpg wrote: post #45

Earlier quoted context omitted.

how does that end up working for typechecking? does the Map module end up having all the properties of the intersection of these elements? The Map example seems pretty easily solvable via Haskell through typeclasses or the more standard OOP-y languages through interfaces, but am I missing something? Does SML not have the tools for this right now?

There are very much ways of expressing that computation in SML—or in Haskell or other languages—but not in the language of modules . Haskell typeclasses would have a similar problem. Consider the following pseudocode: class Map m where {- some implementation -} instance Map HashMap where {- ... -} instance Map TreeMap where {- ... -} mkMap :: Int -> {- ??? -} mkMap size | size > threshold = newHashMap | otherwise = n…

If I remember correctly, isn't this one of the problems Idris and Agda are good at solving?

Re: 1ML – unifying ML into one language

#53

Post by rtpg »

andolanra wrote: post #46
rtpg wrote: post #45

Earlier quoted context omitted.

how does that end up working for typechecking? does the Map module end up having all the properties of the intersection of these elements? The Map example seems pretty easily solvable via Haskell through typeclasses or the more standard OOP-y languages through interfaces, but am I missing something? Does SML not have the tools for this right now?

There are very much ways of expressing that computation in SML—or in Haskell or other languages—but not in the language of modules . Haskell typeclasses would have a similar problem. Consider the following pseudocode: class Map m where {- some implementation -} instance Map HashMap where {- ... -} instance Map TreeMap where {- ... -} mkMap :: Int -> {- ??? -} mkMap size | size > threshold = newHashMap | otherwise = n…

Thanks for the explanation, this is illuminating

I'm still kind of unsure of why (Map m) => Int -> m isn't a valid type signature for this though..

Re: 1ML – unifying ML into one language

#54

Post by pjmlp »

Retra wrote: post #47
jallmann wrote: post #20

Earlier quoted context omitted.

Are you referring to Standard ML, rather than the ML family of languages? 1ML is a new language in the ML family, rather than an extension of SML or OCaml. Consolidating the module and expression languages in 1ML will lead to even cleaner semantics. From the abstract of the Andreas Rossberg paper: > In this “1ML”, functions, functors, and even type constructors are one and the same construct; likewise, no distinction…

Every time I think of unifying various language features like this, I end up imagining that I'd just reinvent LISP and look like a fool...

I think that attempt was called Scheme.

Re: 1ML – unifying ML into one language

#55

Post by cannam »

kristianp wrote: post #48
tokenrove wrote: post #28

Earlier quoted context omitted.

Yeti is pretty nice if you have to work on the JVM: http://mth.github.io/yeti/

That project looks dead, the last commit was November 2013?

The last tagged release was November 2013. The last commit was this week.

Re: 1ML – unifying ML into one language

#56

Post by andolanra »

rtpg wrote: post #53
andolanra wrote: post #46

Earlier quoted context omitted.

There are very much ways of expressing that computation in SML—or in Haskell or other languages—but not in the language of modules . Haskell typeclasses would have a similar problem. Consider the following pseudocode: class Map m where {- some implementation -} instance Map HashMap where {- ... -} instance Map TreeMap where {- ... -} mkMap :: Int -> {- ??? -} mkMap size | size > threshold = newHashMap | otherwise = n…

Thanks for the explanation, this is illuminating I'm still kind of unsure of why (Map m) => Int -> m isn't a valid type signature for this though..

That type means something slightly different: (Map m) => Int -> m doesn't mean that it returns some Map type, it means it returns any Map type. We could write a function of that signature, but that would imply that the caller/context would choose what type of Map it returns (and so it would not depend on the integer argument.)

Think about what it means if a type variable has no typeclass constraint: the type t isn't just a specific unknown type, it's literally any type. Similarly, C t => t isn't a specific unknown instance of a typeclass, it's any instance of that typeclass. If we tell Haskell that we're returning an instance C t => t and then try to give some concrete type, Haskell won't allow it, because it wants that type to encompass any possible type that implements C, not just the one we happened to use.

One way of making the above code work in Haskell is to use an existential type, which expresses that we're talking about some (not any) map type, but we'd have to wrap it inside a different constructor:

    -- this expresses that a SomeMap constructor contains some kind
    -- if Map, but we can't tell which one:
    data SomeMap = SomeMap (forall m. Map m => m)

    -- We can now express this by hiding the choice of Map inside the
    -- SomeMap type:
    mkMap :: Int -> SomeMap
    mkMap size | size > threshold = SomeMap newHashMap
               | otheriwse        = SomeMap newTreeMap
which is, again, a solution with some advantages and some disadvantages.

Re: 1ML – unifying ML into one language

#57

Post by andolanra »

octatoan wrote: post #52
andolanra wrote: post #46

Earlier quoted context omitted.

There are very much ways of expressing that computation in SML—or in Haskell or other languages—but not in the language of modules . Haskell typeclasses would have a similar problem. Consider the following pseudocode: class Map m where {- some implementation -} instance Map HashMap where {- ... -} instance Map TreeMap where {- ... -} mkMap :: Int -> {- ??? -} mkMap size | size > threshold = newHashMap | otherwise = n…

If I remember correctly, isn't this one of the problems Idris and Agda are good at solving?

We could in fact write mkMap in Idris with very little change, and give it a proper type:

    -- This might not be the best/cleanest way of writing it, as my
    -- Idris is a little rusty, but this will work:
    mkMap : (size: Int) -> (if size > threshold then HashMap else TreeMap)
    mkMap size with (size > threshold)
      | True  = newHashMap
      | False = newTreeMap
So yes, although again, other tradeoffs are made to allow this kind of radical expressiveness.

Re: 1ML – unifying ML into one language

#59

Post by fab13n »

Retra wrote: post #47
jallmann wrote: post #20

Earlier quoted context omitted.

Are you referring to Standard ML, rather than the ML family of languages? 1ML is a new language in the ML family, rather than an extension of SML or OCaml. Consolidating the module and expression languages in 1ML will lead to even cleaner semantics. From the abstract of the Andreas Rossberg paper: > In this “1ML”, functions, functors, and even type constructors are one and the same construct; likewise, no distinction…

Every time I think of unifying various language features like this, I end up imagining that I'd just reinvent LISP and look like a fool...

That's often true within dynamically typed languages, but statically typed languages definitely don't feel Lispy. Moreover, messing with static type systems involves much more maths than hacking.

Re: 1ML – unifying ML into one language

#60

Post by capisce »

chongli wrote: post #37
drudru wrote: post #13

I know this is not popular. I think ML has a clean syntax and simple but powerful semantics. I enjoyed coding in it. It just looks better than OCaml. Haskell is, I think, even cleaner, but there is a tendency for developers to explore the possibilities available in Haskell and then increase the complexity. It would be great to see the ML community unify and provide an offering that would give it the kind of support t…

explore the possibilities available in Haskell and then increase the complexity. I'd caution against referring to all such explorations as complexity. Complexity is a highly overloaded term in our field. Sometimes it refers to the number of steps a given algorithm takes to compute (as a function of the input). Sometimes it refers to the depth and breadth of a program's syntax tree as well as its tendency to branch ou…

Accidental complexity is one of the biggest enemies of productivity in the programming world.
Post reply on HN