In my moments of insanity / hammock time I've toyed with making a typed
variant of Clojure. Somewhat inspired by core.typed, but I feel that to be
effective a type system needs to be deeply integrated with the compiler and
standard library, not just a standalone tool.
Types would themselves be an abstraction, supporting the following
operations:
- Intersection with another type (N or And)
- Union with another type (U or Or)
- Checking is a type is a subclass of another type (extends?)
- Checking if a value conforms to the type (instance?)
Abstractions themselves would be possible to define as types, so you could
have the Seqable type:
(defabstraction Seqable ....)
(defn process-sequence [^Seqable s]
(let [things (seq s)] ;; guaranteed to work by type system
...)
Java classes would conform to the Type abstraction, so you can still use
Clojure-style Java type hints for interop.
Anything passed to a typed parameter would be verified to be either:
- A valid subtype, in which case everything is OK
- Something that cannot be a valid subtype, in which case you get a
compiler error
- A potentially valid value (either untyped or an intersecting type), in
which case a runtime check is inserted (and maybe an optional warning...)
Types could be parameterised, so you can have types like:
(ListOf Integer)
(Nullable String)
(ArrayOfShape [10 10])
(ExactValue "Foo")
(Or String Integer)
Occurrence typing would mean that stuff like the following is valid:
(defn foo [^(Nullable (Or String Integer)) x]
(cond
(nil? x) ....
(Integer? x) (+ x 5) ;; valid addition, can prove it is an
Integer
(String? x) (.charAt x 0) ;; no type hint required, can prove it
must be a non-null string....
))
Since branching on type is a common idiom, it would also support type-based
overloading of functions:
(defn foo
([^Null x] ....)
([^Integer x] ....)
([^String x] ....))
Untyped code would look still look like regular Clojure. Types would always
be optional.
On Sunday, 6 November 2016 07:14:39 UTC+8, Didier wrote:
>
> Spectrum (https://github.com/arohner/spectrum) seems quite interesting. I
> haven't tried spec yet, but form quick glance, it looks just as annoying as
> typed clojure to use.
>
> I think I'm imagining something simpler though. Say a system that just
> used already existing Clojure type hints, and performed compile time checks
> about to whatever level is possible given the provided annotation.
>
> So say I did:
>
> (def ^int something "test")
>
> This would fail at compile time.
>
> Similarly:
>
> (def ^String something "test")
> (inc something)
>
> It would fail at compile time.
>
> Or:
>
> (defn inc2 [^Long a]
> (inc (inc a)))
> (inc2 1.80)
>
> Would also fail.
>
> And hopefully this:
>
> (defn ^Long inc2 [^Long a]
> (inc (inc a)))
> (def temp ["test", 2.48])
> (map inc2 temp)
>
> Would also fail. Because the type checker would infer that the vector has
> String or Double as type, and inc2 expects none of these.
>
> Or:
>
> (conj ["a", "b"] "c")
>
> would still work.
>
> (conj ^Vec<String> ["a", "b"] 10)
>
> would fail.
>
> Now I don't know, maybe this is too simple, not really useful, or maybe
> its non trivial to implement. But I feel just small type checks like that
> could be useful, and they wouldn't be too burdening.
>
> On Saturday, 15 October 2016 15:14:08 UTC-7, Didier wrote:
>>
>> I know a lot of people like to say how unhelpful Java like static typing
>> is, and only more powerful type systems of the ML family add value, but
>> I've been wondering recently if for Clojure it wouldn't make more sense to
>> simply extend the type hints to enable an optional Java like static typing
>> schemI the.
>>
>> It is my understanding that ML style static typing is incredibly
>> difficult to add properly and without compromise to a dynamic language.
>> That doing so limits the scope of type inference, rendering the task of
>> adding type info more tedious then in ML languages themselves.
>>
>> ML style static typing provide enhanced safety grantees, but seem to add
>> too much complexity to Clojure to be practical. What about a Java like
>> static typing scheme though?
>>
>> I haven't found in practice that the safety of Clojure was an issue, as
>> the REPL workflow tend to promote quite a lot of testing. So I'm not too
>> worried about needing the state of the art of provable correctness for my
>> programs. What has been a biggest cause of issue to me was refactoring and
>> shared code base across a team. Those last two use cases are actually
>> pretty well handled by Java like static type checking. Is it a powerful
>> type checker, not really, but it enables most trivial type errors to be
>> caught early, and it allows easier integration points for other devs to
>> follow, as well as documentation for functions, better tools support and
>> easier refactoring, while also enabling performance optimizations.
>>
>> I have limited knowledge in typing systems, and have no idea how easy it
>> is to implement them, but as a user of Clojure, I feel like I would find an
>> optional Java like static typing a great addition, one that I am more
>> willing to use and benefit from then Typed Clojure's more complex ML style
>> type checking.
>>
>> What do other think?
>> Can anyone with better knowledge tell me if this would be feasible or if
>> adding such gradual typing system is effectively as hard as adding ML style
>> type checking?
>>
>
--
You received this message because you are subscribed to the Google
Groups "Clojure" group.
To post to this group, send email to [email protected]
Note that posts from new members are moderated - please be patient with your
first post.
To unsubscribe from this group, send email to
[email protected]
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 [email protected].
For more options, visit https://groups.google.com/d/optout.
