Typed Clojure paper draft

54 views
Skip to first unread message

Ambrose Bonnaire-Sergeant

unread,
Mar 11, 2015, 10:50:24 PM3/11/15
to core.typed, clojure
Hi,

Please check out our new paper draft on core.typed's type system.

The first few pages has a lot of executable code and is intended to be accessible
to anyone. Feedback welcome! 

Thanks,
Ambrose

Ambrose Bonnaire-Sergeant

unread,
Mar 13, 2015, 11:26:01 PM3/13/15
to core.typed
Ah great catch. Here's the justification for our surprise.

1) Occurrence typing was not designed with multimethods in mind.
2) Multimethods are surprisingly easy to formalise, and straightforward to understand (B-DefMulti, B-DefMethod, B-BetaMulti in figure 9 model the core semantics for multimethods)
3) `isa?` is surprisingly easy to support with occurrence typing, even though it is the core dispatch mechanism for multimethods. Complicated tests like (isa? [(class a) (class b)] [Number Boolean]) naturally learn that `a` is a Number
and `b` is a Boolean.
4) Relating the dispatch function with the current dispatch value to learn new types via normal occurrence typing is almost always sufficient to type check the current defmethod body.

Thanks for the feedback.
Ambrose

On Fri, Mar 13, 2015 at 5:20 PM, Chris Ford <christop...@gmail.com> wrote:

I like the paper.

One small piece of feedback - I didn't understand what about the multimethods section justifies the claim of "surprising synergy" in the introduction. Perhaps you could elaborate on the novelty?

Chris

--
You received this message because you are subscribed to the Google
Groups "Clojure" group.
To post to this group, send email to clo...@googlegroups.com
Note that posts from new members are moderated - please be patient with your first post.
To unsubscribe from this group, send email to
clojure+u...@googlegroups.com
For more options, visit this group at
http://groups.google.com/group/clojure?hl=en
---
You received this message because you are subscribed to the Google Groups "Clojure" group.
To unsubscribe from this group and stop receiving emails from it, send an email to clojure+u...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

--
You received this message because you are subscribed to the Google
Groups "Clojure" group.
To post to this group, send email to clo...@googlegroups.com
Note that posts from new members are moderated - please be patient with your first post.
To unsubscribe from this group, send email to
clojure+u...@googlegroups.com
For more options, visit this group at
http://groups.google.com/group/clojure?hl=en
---
You received this message because you are subscribed to the Google Groups "Clojure" group.
To unsubscribe from this group and stop receiving emails from it, send an email to clojure+u...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.



Reply all
Reply to author
Forward
0 new messages