Working on a small standard-library overlay focused on total functions and I made integer division total. Is this too crazy?

Learning
21

I was intrigued by how this issue might be approached with dependent types, so I installed Idris2, read docs for an hour or two and came up with something a little different that what I was imagining, but somewhat interesting nonetheless.

I didn’t find out if I could write a function like forall (n m: pos) where n > m -> (sub n m : pos)

But I did manage to do was this: (I defined positive integers as a unary type because I don’t know anything about type aliases in Idris yet)

subType : Pos -> Pos -> Type
subType One One = Nat
subType _ One = Pos
subType One _ = Integer
subType (S n) (S m) = subtractable n m

subPos : (n : Pos) -> (m : Pos) -> subType n m
subPos One One = 0
subPos One (S x) = -(natToInteger (natOfPos x))
subPos (S x) One = x
subPos (S x) (S y) = subPos x y

Basically what you can do is create functions which return types, like subType above, and then use them in type signatures for other functions (as in subPos)

So here, subPos may return an Integer, a Nat or a Pos based on the value of the inputs. Kind of an interesting approach. Idris can confirm that this is correct because the case matching between the two functions is basically identical, so it doesn’t need to actually execute the code for subType at runtime to determine the type because it can statically deduce that it is correct.

What I don’t yet know is what you can do with the output of this function in a case where the values of the inputs are unknown. I assume you have to handle every case, but I don’t know what that looks like yet.

22

It’ll be completely fine for some uses (e.g., you need to do a single division by a number passed as a command-line argument: great, you’ve pushed validation at the very entrance of your program, you don’t need much beyond this) and really painful for others (e.g., you are doing a bunch of arithmetic operation in a row with intermediate results passed around: you’ll need to stop here and there to validate intermediate results, all validation failures will probably lead to the same handler).

If you want to be friendlier to the latter use-case, you can try sdomething closer to

module SafeArith : sig
  type integer
  val of_int : int -> integer
  val to_int : integer -> (int, [`Division_by_zero | `Mod_by_zero | `Overflow]) result
  val ( / ) : integer -> integer -> integer
  (* other arithmetic infix ops, but on integer rather than int *)
end

You can then have arbitrarily nested arithmetic expressions with a local open.

1 Like