Introducing Iron: type-level assertions for Scala

Announce
1

Hello everyone!

This is an introduction to Iron, a type constraint system for Scala. It allows you to create either-based assertions at type level.

Here is a small example using iron-numeric:

def log(x: Double ==> Greater[0d]): Refined[Double] = x.map(Math.log)

val x = -1d
val y = 1d
log(x) //Left(IllegalValueError(0d, "value should be greater than the specified value"))
log(y) //Right(1d)

Iron can also optimize and evaluate constraints at compile-time in some cases:

log(-1d) //Compile-time error
log(1d) //Replaced at compile time by `Right(1d)`

Iron also has modules for other kind of data (string, numeric, iterable…) and for some projects (cats, circe…)

More information on the project repository: GitHub - Iltotore/iron: Hardened type constraints for Scala

A small example of a REST API using Iron & Cats is available here.

I already wrote a post about my project in r/scala when 0.1.0 was released and I had many good reviews. Now, Iron v1.1 is out and I’m open for any suggestion here and in the Issues section. :slightly_smiling_face:

7 Likes
2

@Iltotore Looks nice!
If possible, it would be enlightening if you could compare differences/similarities between Iron and Type level’s GitHub - fthomas/refined: Refinement types for Scala ?

(Tried to find references from either to the other but couldn’t find any comparative info…)

1 Like
3

Sorry for the delay!

Iron and Refined share similarities:

  • They both provide type refinements
  • They both support compile-time and runtime checking
  • Their usages are similar: IronType[Type, Constraint] vs Refined[Type, Constraint]

But they have major differencies:

  • Refined supports Scala and has AFAIK partial support for Scala 3 while Iron is Scala 3 only
  • Refined relies on Shapeless while Iron (core) does not depend on any lib and uses Scala 3’s new metaprogramming features
  • The previous point makes Iron’s ability to check constraints at compile-time predictable: if the value to test and the condition to evaluate are fully inlined, it works at compile-time. If they aren’t then the condition has to be checked at runtime. I couldn’t find such rules in Refined.
  • Iron does not bring any overhead at runtime (thanks to Scala 3’s opaque types and inline keyword). For example val x: Int :| Positive = 5 is compiled to val x: Int = 5. Moreover, val x: Either[String, Int :| Positive] = value.refineEither desugars to val x: Either[String, Int] = Either.cond(value > 0, value, "Should be strictly positive")
3 Likes
4

Many thanks for a very informative and easy to understand explanation of differences! It would be great if you included this info in the README-page and/or microsite.

Iron seems like a very cool library and it seems easy to use even for those without any meta-programming knowledge or even knows about inline and opaque types to just use the basics.

1 Like