How expressive are Iron’s refinement types?

[GunpowderGuy]

Hi, I have a few questions about what can be expressed with Iron’s refinement types.

In tools like [Liquid Haskell](https://ucsd-progsys.github.io/liquidhaskell-blog/), which implements a subset of refinement types known as liquid types, it’s possible to encode and statically verify properties like:

That a function f sorts its input.

This can be defined as: for any input xs, the output ys = f(xs) is both a permutation of xs and ordered. These two properties together state that f is a sorting function — and the type checker enforces that.

Another kind of property I’m interested in is totality: that a function terminates for all finite inputs.

Are these types of properties currently expressible with Iron?

In addition, I’ve experimented with encoding game rules using refinement types. For example, here’s a simplified version of Crazy Eights ("Ocho Locos"):

https://gist.github.com/GunpowderGuy/9b0bcdd80f5fc0f6097032861e681e70

It’s written in Idris2 using dependent types, but something very similar is possible with Liquid Haskell too. In this game, each card played must match either the number or the color of the card at the top of the stack. The rules are encoded in the types, and any match ( structure that consists of a series of moves ) that violates them is rejected at compile time.

Could something like that be represented in Iron?

Thanks in advance — I’m very interested in what’s already possible with Iron’s current type system.

[Iltotore]

Hello.

Iron is less expressive than LiquidHaskell mainly because it only relies on Scala's metaprogramming capabilities and isn't a compiler plugin, just a regular library (unlike LiquidHaskell AFAIK).

This can be defined as: for any input xs, the output ys = f(xs) is both a permutation of xs and ordered. These two properties together state that f is a sorting function — and the type checker enforces that.

It is currently not possible to do this kind of constraint because of multiple things:

• Iron does not infer constraints/evidences by itself
• Evaluating at compile-time some expressions is hard to do in Scala metaprogramming without having to re-create the compiler itself

In addition, I’ve experimented with encoding game rules using refinement types. For example, here’s a simplified version of Crazy Eights ("Ocho Locos"):

https://gist.github.com/GunpowderGuy/9b0bcdd80f5fc0f6097032861e681e70

Same for your Idris 2 example. Scala's dependent typing is far less powerful than Idris' and it is not possible to get user-defined typeclass instances (like FromExpr) in a macro in Scala sadly. However Iron will enforce explicit checking at runtime for this case.

Thanks in advance — I’m very interested in what’s already possible with Iron’s current type system.

This is probably where the confusion is: Iron is not a fully fledged type system and is just a relatively small library leveraging Scala's existing type system and metaprogramming capabilities to implement refined types. To achieve something like Idris or LH, we'd probably need at least a compiler plugin if not a fork of Scala's compiler itself.

Also, you might be interested in Stainless (Github).

[GunpowderGuy]

Thanks! That answers what i wanted to know about Iron.
Given your info , Stainless is probably the closest analogue to liquid haskell. Except it isnt nearly as used as liquid haskell. And it might be less geared towards interop with projects that dont use it? I should open a github issue asking them about that