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

41–50 of 63 posts

Re: 1ML – unifying ML into one language

#41

Post by tel »

platz wrote: post #34
oggy wrote: post #12

Earlier quoted context omitted.

Erasing that distinction enables some goodies such as first-class type constructors, which makes it possible to manipulate types of higher kind. This in turn, presumably enables things like Generalized Algebraic Data Types.

the monad example in 1ML is: type MONAD (m : type ⇒ type) = { return a : a → m a; bind a b : m a → (a → m b) → m b }; map a b (m : type ⇒ type) (M : MONAD m) (f : a → b) (mx : m a) = M.bind a b mx (fun (x : a) ⇒ M.return b (f x)) (* : m b *) not too bad.. though I wonder if things are defined structurally instead of nominally, which monad instance are you going to get for a given expression. Haskell's "one instance p…

You have to explicitly pass the monad "vtable". If 1ML also grabs up modular implicits then you'll have a sensible way of passing implicit arguments not exactly unlike that of Haskell, but modularity and global canonicity are at odds so you have a more complex reasoning task.

Re: 1ML – unifying ML into one language

#42

Post by chongli »

munro wrote: post #40
chongli wrote: post #37

Earlier quoted context omitted.

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…

> I'd caution against referring to all such explorations as complexity. Complexity is a highly overloaded term in our field. The difference between complex & hard, easy & simple has been put very elegantly by Rich Hickey in Simple Made Easy [1]. That doesn't mean everyone agrees with his definitions, which is why he revives the word "complected" to mean objective interleaving of concepts, and pulls out "hard" from th…

Yeah, I've seen that presentation. Rich's ideas were what I had in mind when I wrote my reply.

In general, use of highly overloaded words is ambiguous in these discussions.

Re: 1ML – unifying ML into one language

#43

Post by iskander »

platz wrote: post #34
oggy wrote: post #12

Earlier quoted context omitted.

Erasing that distinction enables some goodies such as first-class type constructors, which makes it possible to manipulate types of higher kind. This in turn, presumably enables things like Generalized Algebraic Data Types.

the monad example in 1ML is: type MONAD (m : type ⇒ type) = { return a : a → m a; bind a b : m a → (a → m b) → m b }; map a b (m : type ⇒ type) (M : MONAD m) (f : a → b) (mx : m a) = M.bind a b mx (fun (x : a) ⇒ M.return b (f x)) (* : m b *) not too bad.. though I wonder if things are defined structurally instead of nominally, which monad instance are you going to get for a given expression. Haskell's "one instance p…

If you combine this with [modular implicits](http://www.meetup.com/NYC-OCaml/events/222026251/), which are hopefully going to be added to OCaml soon, then you'll get something which is nearly as syntactically neat as type classes but more powerful.

Re: 1ML – unifying ML into one language

#44

Post by platz »

iskander wrote: post #43
platz wrote: post #34

Earlier quoted context omitted.

the monad example in 1ML is: type MONAD (m : type ⇒ type) = { return a : a → m a; bind a b : m a → (a → m b) → m b }; map a b (m : type ⇒ type) (M : MONAD m) (f : a → b) (mx : m a) = M.bind a b mx (fun (x : a) ⇒ M.return b (f x)) (* : m b *) not too bad.. though I wonder if things are defined structurally instead of nominally, which monad instance are you going to get for a given expression. Haskell's "one instance p…

If you combine this with [modular implicits]( http://www.meetup.com/NYC-OCaml/events/222026251/ ), which are hopefully going to be added to OCaml soon, then you'll get something which is nearly as syntactically neat as type classes but more powerful.

More power in terms of flexibility, but the mechanism of implicits makes it less clear which instance is in scope for a given expression.

With true typeclasses, there is no ambiguity which instance will be selected (there can only be one)

This distinction is often lost when comparing true type classes with their emulation via implicts.

Sometimes "more power" is not what you want i.e. this is more of a tradeoff.

Re: 1ML – unifying ML into one language

#45

Post by rtpg »

andolanra wrote: post #33
tachyonbeam wrote: post #11

Earlier quoted context omitted.

Can you elaborate on why these are problems for ML?

One of the classic motivating examples (which is addressed in the 1ML paper) goes like this: Both trees and hash tables can be used to implement map-like data structures. You could, in ML, have an abstract signature for Map types that gets implemented sometimes by a concrete TreeMap implementation and sometimes by a concrete HashMap implementation. HashMap would be a better choice if the expected number of entries is…

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?

Re: 1ML – unifying ML into one language

#46

Post by andolanra »

rtpg wrote: post #45
andolanra wrote: post #33

Earlier quoted context omitted.

One of the classic motivating examples (which is addressed in the 1ML paper) goes like this: Both trees and hash tables can be used to implement map-like data structures. You could, in ML, have an abstract signature for Map types that gets implemented sometimes by a concrete TreeMap implementation and sometimes by a concrete HashMap implementation. HashMap would be a better choice if the expected number of entries is…

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        = newTreeMap
What is the type of mkMap? It won't actually type-check in Haskell. It can't be (Map m) => m, because it needs to have a concrete type. We could do some kind of type-level work, relect the size variable into the type level, and have a type family that decides whether the resulting type is a HashMap or a TreeMap—but that has the same problem as the OCaml example, where we're using a different language (the language of type-level computation) to talk about something that'd be simple with value-level programming.

One place where you could write this easily is in a dynamically typed language:

    def mkMap(size):
        if size > threshold:
            return HashMap()
        else:
            return TreeMap()
That is exactly why this kind of research is interesting: we'd like to capture the flexibility of idioms that dynamic languages can sometimes afford us, with the extra safety and security guarantees of a static type system!

Re: 1ML – unifying ML into one language

#47

Post by Retra »

jallmann wrote: post #20
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…

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

Re: 1ML – unifying ML into one language

#48

Post by kristianp »

tokenrove wrote: post #28
mafribe wrote: post #24

Earlier quoted context omitted.

I'd never have left the ML world had it not been for the lack of an ecosystem that's comparable to what the JVM has to offer. And my Scala programs mostly just use ML-like features, but I can't live without all those rich libraries that are lacking in ML.

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?

Re: 1ML – unifying ML into one language

#49

Post by riffraff »

brandonbloom wrote: post #36
platz wrote: post #32

Earlier quoted context omitted.

F# doesn't even have modules; although it's derived from an ML, it has cut out rather important parts of it to make it fit into the .net ecosystem.

You're not wrong, but I may phrase it differently... F# lacks modules, instead favoring objects. Although it's derived from OCaml, it has omitted complex features which don't fit in to the .net ecosystem.

but is there say, something that (S)ML's modules allow which is not possible to do with F#+.NET objects?

I.e. ML's modules can be used to create interfaces and implementations of ADTs, but so can OO interfaces and classes.

Re: 1ML – unifying ML into one language

#50

Post by mercurial »

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…

You don't need a dynamic language for that. In Java:

    Map mkMap(int size) {
        return size > threshold ? new HashMap() : new TreeMap();
    }
Post reply on HN