Clojure's core.typed vs Haskell | Hacker News Reader

Clojure's core.typed vs Haskell

adambard.com

120 pointsllambda62 comments

A simple program is an interesting comparison, but it's kind odd to consider this to compare the whole typesystem. It's hard to understate that GHC has a /big/ typesystem and has had a significant amount of research done in it over the past 10 years and a a result there are a lot of very powerful non-trivial typing constructs. I think the real testament to the power of Haskell's typesystem is how well inference still works even in the presence of most of these non-trivial extensions.

Really, the post is about Clojure; these toy problems represent the breadth of my experience with Haskell, so I'm not really qualified to go into more depth. Certainly Haskell is said to have the most powerful type system going, and I don't see any (mainstream-ish) language displacing it any time soon.

Still, I think core.typed does pretty damn well for being a standalone library.

> Certainly Haskell is said to have the most powerful type system going,

Nah, Coq, Agda, Idris and any dependently typed language have Haskell beat -- their type systems are designed to be just as expressive as their value language. Haskell is certainly moving in this direction, especially with modern extensions. The issue is of course type inference breaks down in the face of these extensions, and Haskell is trying to maintain its powerful type inference as best it can. Certain combinations of extensions already force type annotations.

> Still, I think core.typed does pretty damn well for being a standalone library.

This is true, and I think the comparison to Haskell actually hurts the greater point you're trying to make. Haskell has full static types at its disposal, and comparing them to the optional typing of Clojure will always leave something wanting -- why draw that comparison when competing with Haskell is not the intention of the library?

Nah, Coq, Agda, Idris and any dependently typed language have Haskell beat -- their type systems are designed to be just as expressive as their value language.

That may be true, but it comes at a big cost: inference and decidability. Haskell's type system is designed to very carefully butt up against the limits of these features. Once you go full-spectrum dependent types, you lose all that.

Agda and Coq retain inference and decidability by sacrificing Turing completeness. Terminating programs must terminate provably, and non-terminating programs must make concrete progress on every iteration. I'm not familiar enough with Idris to say how it tackles this issue - I do know that it is Turing complete.

So with that said, you're absolutely right.

Another language with a Turing complete type system is Shen [1] (previous life as Qi). Just wanted to put that out there as its a Lisp dialect that really pushes Lisp out there.

[1] http://shenlanguage.org/

When it comes to awesomeness to fame ratio, I can't think of a language with a higher one than Shen. It's odd how little people talk about it. I, unfortunately, suspect it has to do with the people leading it.

I've looked at Shen a few times and, honestly, I always get turned off by the syntax. There's not enough out there explaining why I should continue past that concern, and it seems to throw out what's nice about Lisp syntax in order to get halfway to Haskell's.

I'm sure I'll take a look at it again sometime, but I'd really love some kind of intro that helped me to understand why it was worth the time investment to get to know it.

License has been a major turn off, just like Plan 9. Did they fix that yet?

> Agda and Coq retain inference and decidability by sacrificing Turing completeness.

I don't know if I would phrase it that way, but there's a more important slight of hand going on here and I think chongli was right in spirit. Haskell takes care of (most) type level things for you with inference. Coq and Agda allow you to give very precise types to things, but those very precise types involve values that are not automatically inferred for you. It's certainly not the case that you can write the same annotation-free function in Coq that you would have written in Haskell and have a very precise type inferred for you.

> Nah, Coq, Agda, Idris and any dependently typed language have Haskell beat

I just knew someone was going to correct me on that statement, hence my "mainstream-ish" qualification.

> why draw that comparison when competing with Haskell is not the intention of the library?

I've got an unhealthy obsession with syntax, and I wanted to have a reference for people to see how things look in a "real" typed language. But, while I'm here, here's a bit I just wrote on /r/haskell (someone put this link there, but of course the haskellers were unimpressed) in defense of the library:

---

Developing in Clojure tends to be a bit of an organic process, thanks to the deep REPL integration in many tools. You can evaluate arbitrary bits of your code as you go, swap things out, tweak whatever you like, and through a more-or-less exploratory process end up with a working bit of code. It's very freeing and very efficient, but if you've ever used a dynamic language for a large project, you know that this tends to create issues refactoring later unless every component is attached to a unit test. The power of core.typed is to let you, after the fact, lock down those function signatures and create what amounts to an automatic test suite.

This is the same for Haskell where it's also convenient to develop in the repl (ghci).

There's the repl, and then there's nREPL. I do like ghci, but I can't execute arbitrary chunks of Haskell directly from Vim.

This isn't a function of ghci or Haskell, that's an editor feature. If you want that kind of functionality than emacs is probably your best bet.

Though you can send arbitrary code blocks from vim using vim-slime.

[1] https://github.com/jpalardy/vim-slime

Though you can't execute arbitrary blocks of text in Haskell. Almost everything non-trivial will require adding a slew of "let"s, not all statements are available in GHCi, and state gets wiped on every reload.

When I first began developing Haskell, coming from Clojure, these issues drove me crazy. Nowadays I don't miss them too much and doubt that they're really such good features to begin with...

But it's decidedly false to claim that GHCi is as flexible as Clojure's repl. Nowadays, Clojure's repl would make me anxious. It reminds me a bit of people doing live code edits on a production server. You can't ever be quite sure what you get.

It doesn't feel like you're pushing the type system though. Can it do generics? Covariance? Higher-kinded types?

(Serious questions, though even if the answer is yes I can't really see it drawing me away from scala)

If you really want it, you can get safe dynamic typing in Haskell using the Data.Dynamic module. However, since you don't really want it, it's a library that isn't introduced in basic tutorials.

This gives you a pragmatic equivalent to no-check, but is almost never used in practice because it turns out to be unnecessary.

Also, GHC from version 7.6.1 supports a flag to defer type errors until run time[1]: -fdefer-type-errors. This is not support for dynamic types, but still gives even more flexibility in type-error handling.

[1] http://ghc.haskell.org/trac/ghc/wiki/DeferErrorsToRuntime

Every now and then I reinvent Data.Dynamic. By this point I'm pretty far into the realm of "probably not worth it", but hitting Data.Dynamic is usually an unignorable indication that I'm going to regret this code.

I'd be curious to see how Typed Racket compared, too.

There would be annotations in the same places as Typed Clojure, except :no-check would be replaced by type soundness-preserving runtime assertions. There would be no need for :no-check anyway; Typed Racket's base annotations are complete AFAIK.

It is a little clearer to me how this works with things like primitives, but how do you annotate a function that takes a map as input and returns a list? (defn my-keys [m] (keys m))

Edit: Just found Seqable. Looking into it now. This link helped me a lot. https://github.com/clojure/core.typed/wiki/Types

Ambrose pointed me at this link for documentation of core.typed's convenience type wrappers (Vec, Seq, List etc.): http://clojure.github.io/core.typed/#clojure.core.typed/Seq

(ns my-ns (:require [clojure.core.typed :as t :refer [ann]]))

(ann my-keys (All [a] [(t/Map a Any) -> (t/Coll a)])

nice, thanks!

Pretty close to clojure, problem 1: https://gist.github.com/anonymous/6764863

> As seen at the top, it was necessary to annotate mod. It has the no-check flag on it, which is basically how you tell core.typed to just take your word on this one. That's something you can't do in Haskell, but I'm not sure whether or not that's a good thing.

Isn't the reason why you need to do it because you're importing a non-typed symbol? Wouldn't the only situation where you'd need to do that in Haskell be at FFI?

(and a nitpick: `putStrLn $ show` can be replaced with a simple `print` call)

Of course you can do this in Haskell:

http://www.haskell.org/ghc/docs/7.6.2/html/libraries/base/Un...

I'll save the value judgement for another time, but I'd like to point out an important difference:

As the word "unsafe" implies, these Haskell primitives forego type safety in addition to type correctness. That means you can get segfaults and other undefined behavior at runtime. Such a type error on the JVM will simply produce an exception at runtime.

This is why we have Data.Dynamic which does safe dynamic types.

It almost never comes up because it turns out to be virtually useless, but that's a story for another time.

> it turns out to be virtually useless

That's debatable, however Data.Dynamic is built on top of Data.Typeable, which provides a lower level runtime type safety facility. I think we can both agree Typable has lots of interesting uses.

Typeable is interesting in theory and generic traversals are a godsend, but usually I find that when I'm reaching for that particular hammer I should check twice.

I'll agree it's best to avoid fully open unions when you can, but some (super useful) things truly don't work that way. Check out http://okmij.org/ftp/Computation/monads.html#ExtensibleDS for a cool example.

I always think of Control.Exception as the poster child for open unions.

Perfect, since exceptions are a subset of effects! Check out http://math.andrej.com/eff/ and its literature.

The difference is that Haskell does not check types at runtime like Clojure does (which is the point of strong static typing), so if the type is wrong it becomes as unsafe as C.

> Integer is less useful as a type than hoped. AnyInteger seems to be more permissive, and works more often. I'm sure there is a good reason for this.

This is with about 15 minutes of looking at core.typed. Isn't this because the type Interger is actually java.lang.Integer, but (type 1000) is java.lang.Long?

Also, AnyInteger isn't that permissive. It's defined as (U Integer Long clojure.lang.BigInt BigInteger Short Byte). The big difference would be that Haskell's Int is bounded so AnyInteger is more like Haskell's Integer.

That would be the reason, yeah. I had forgotten that Clojure tends to use Longs for everything.

The Haskell could use a list comprehension...

    divBy x y = y `mod` x /= 0
    divBy3or5 x = divBy 3 x || divBy 5 x
    euler1 n = sum [x | x <- [0..n], divBy3or5 x]
    
    main = print $ euler1 1000

Personally, I'd switch out lines 2 and 3 to:

    euler1 n = sum [x | x <- [0..n], divBy 3 x, divBy 5 x]

Compared with the Clojure (correct me if I'm wrong):

    (defn euler1 [n] (reduce + (filter (fn [x] (or (div-by 3 x) (div-by 5 x)))) (range n)))

Edit: Note - Clojure code doesn't fit into a HN one-liner.

You could shave off a precious few characters using the function reader syntax:

    (defn euler1 [n] (reduce + (filter #(or (div-by 3 %) (div-by 5 %)))) (range n)))

Or if you're into comprehensions:

    (defn euler1 [n] (reduce + (for [x (range n) :when (or (div-by 3 x) (div-by 5 x))] x)))

Apples vs vacuum cleaners

Is this (at the end of problem 1)

    (defn div-by [x y] (== 0 ))(mod y x)

a typo or a Clojure feature?

Not being familiar with core.typed: does it support parametric polymorphism? Can you dispatch based on types (e.g. typeclasses)?

Yes, Clojure has "protocols", which allow multiple dynamic dispatch on generic functions.

http://clojure.org/protocols

Right, but protocols are not based on core.typed's annotations. There is no way to dispatch on the return type of a function, for example.

> There is no way to dispatch on the return type of a function, for example.

A feature, in my opinion.

See https://news.ycombinator.com/item?id=6459968

A feature, in my opinion.

Well, Clojure's a different language so it doesn't matter as much. If Clojure had enforced purity and pervasive laziness (a la Haskell) it'd be a real pain to use monads without polymorphic operators for them.

You're assuming that Haskell's monadic approach is the ultimate approach to managing effects (which include delayed evaluation). Personally, I prefer the model in Eff [1] and proven as an alternative to monad transformers (although, still a single-layer monad in Haskell) [2]. Eff's approach utilizes capabilities [3], called "effect instances", to restrict access to effects. Much nicer, in my opinion. Hence, I've been experimenting with the ideas in Clojure [4].

[1]: http://math.andrej.com/eff/

[2]: http://lambda-the-ultimate.org/node/4786

[3]: http://erights.org/elib/capability/ode/ode-capabilities.html

[4]: https://github.com/brandonbloom/cleff

I don't know enough about the theory to argue either way. I just really like Haskell's monad libraries (as well as applicative functors and lenses). If you're able to build a library that's as general, flexible and powerful in Clojure I will be really excited!

I'm not at all sure about it, but I wonder if you could combine multimethods with core.typed's `cf` to accomplish this.

What a waste of an article. 8 lines of code for haskell, 19 lines for clojure. The problem is easily solved in one line. I seriously don't care that's he comparing core.type, when you start trying to write langauges the same way, you lose the advantage that they provide.

1 line of python.

print sum(filter(lambda x: (x % 3 == 0) or (x % 5 == 0), range(1, 1000)))

clojure

(apply + (filter #(or (= 0(mod % 3)) (= 0(mod % 5))) (range 1 1000)))

In Haskell it could be sum $ filter (\x -> mod x 3 == 0 || mod x 5 == 0) [1..1000] but I don't think that detracts from the article. He said up front his solution was over-engineered. That's nice in this case, because it lets us see how the type annotations look for very small, simple functions so we can get an idea what they looked like. I know some Haskell and Clojure, but I'd never actually looked at core.typed. This was a nice, basic intro to it.

Even better, you can save 7 characters with:

    sum [x | x <- [1..1000], mod x 3 == 0, mod x 5 == 0]

But as you say, that wasn't the point of the article.

This version is easily the clearest yet.

> I seriously don't care that's he comparing core.type

...so you object to his solutions because you don't care about the point of the article, which is what forces him into those specific solutions.

> I seriously don't care that's he comparing core.type [sic]

Well then I'm afraid the article has nothing to offer for you.

IMHO, your code is much harder to read than his. It looks like its been run through a minifier. I'd rather maintain his code.

The clojure code is pretty idiomatic and clear to anyone that's done work in lisp-like languages.

As someone who has done work in lisp-like languages, I would call the clojure code legible but not "clear". It's perfectly fine for a one-off solution, but I wouldn't consider it acceptable for anything I planned on coming back to in a few months.

I don't know when I cross that line of someone who's done work in lisp-like languages, but I've made two or three small hobby projects in clojure and contributed a bug fix to http-clj and am well versed in the source code of seesaw. I don't usually see code like that in those projects.

More idiomatic Python, and quite clear IMHO

    print sum(x if x % 3 == 0 or x % 5 == 0 else 0 for x in range(1, 1000))

Yeah, a list comprehension is the easiest way to write it in any of the languages. I think it's a little clearer/shorter to do print sum(x for x in range(1, 1000) if x % 3 == 0 or x % 5 == 0)

Reply on news.ycombinator.com