The `(define-class (Eq :a) ...)` block is defining a type class called `Eq` with a type parameter named `:a`. Think of this as an interface that can be added after the fact. Most (all?) major OOP languages only allow you to declare interfaces when you declare a class, but in Haskell, and in Coalton that takes a lot of inspiration from Haskell, you can declare "interfaces" (typeclasses) on any pre-existing type, including ones coming from a library. Here, the `Eq :a` interface means that there must be a function called == (in Lisp even the operators are defined as functions) that takes two parameters of type :a and returns a Boolean.
`(define-type Color ...)` is defining a simple enum type. (You can do a lot more with it, of course, but this example is kept simple). Then `(define-instance (Eq Color) ...)` is saying "The type called Color is an instance of the typeclass (interface) called Eq". And since Eq requires a function called `==`, inside the define-instance block you have to define that function for the Color type. The pattern-matching should be simple enough that I don't think I need to explain it.
Now, the thing that makes this more powerful than interfaces is something I already touched on. Here the Color type is declared and then its typeclass instances are defined right away, which is the normal thing to do when you're creating a new type: keep all its code together. But if that Color type had come from another library that you imported, you would still be able to say "oh, and this Color type does implement Eq: here's the definition of == as applied to Color values". You're not restricted to only the interfaces that the library author thought to apply: you can take someone else's code and add interfaces to it! There have been several times when I really wished that were possible in C#.
Finally, the constraints before the => fat arrow are like declaring your function parameters as `public T isEqual<T>(T a, T b) where T : IEquatable`. This allows Coalton to catch, at compile time, any call to `is-eql` with parameters for which the `==` function is not defined.
There's plenty more at https://coalton-lang.github.io/manual/topics/whirlwind-tour/.
I mean it must employ gradual typing, right? So that it can interface with existing code that is untyped
But there are definite advantages to having Coalton know your types, which is why they give you a `(declare foo Integer)` form. This doesn't compile to any code, it's a compiler hint that tells Coalton that it can assume `foo` is an int, not a float64/double, which allows it to pick at compile time which implementation of + gets used in `(+ foo 5)`.
The 2025 video introducing Coalton at https://www.youtube.com/watch?v=of92m4XNgrM gives an example of what Coalton can do with knowing types. Robert Smith (the presenter, and the primary creator of Coalton) gives an example of a Fast Fourier Transform function that uses generic numeric types so you can call it on any number type: float32, float64, int-modulo-a-prime, whatever. He then benchmarks it, and it takes about 1 second to run 2 million times. Then he adds the single compiler hint `(monomorphize)` above the function declaration. This tells Coalton "Hey, instead of doing a dispatch table lookup in this function and calling different + implementations based on the type of the parameters, I want you to create two different copies of this function, one that will call the specialized float32 math functions, and the other one that will call the specialized float64 math functions." (Or three copies if you also called it with your int-modulo-prime number type). This eliminates a dispatch-table lookup and allows the compiler to produce much more specialized code. It comes at the expense of larger binaries, of course: he's explicit about how this is trading speed for size, so it's an opt-in choice you make (by adding a `(monomorphize)` declaration above the function definition) rather than something that Coalton defaults to.
But I've digressed. Yes, I believe (though note my caveat about not having used Coalton yet) that it would use dynamic types for code whose types it can't infer. But I'm pretty sure it would also give you a warning. If it gives you an error, the solution is to add a `(declare [name] [type])` line in the appropriate place.
Code that is untyped—Common Lisp code—is run in (lisp ...) forms [0] which requires the user to annotate the type and adds dynamic type checks to it to ensure it meets the contract the programmer specified.