Is there any difference in expressiveness between an extern praxi and an extern castfn?

Question

Consider:

#include "share/atspre_staload.hats"

fun only_zero(n: int(0)): void =
        println!("This is definitely zero: ", n)

fun less_than{n,m:int | n < m}(n: int(n), m: int(m)): void =
        println!(n, " is less than ", m)

implement main0() = (
        only_zero(zeroify(n));
        only_zero(m);
        less_than(b, a);
        less_than(f, e) where { val (f, e) = make_less_than((d, c)) };
) where {
        val n = 5
        val m = ~5
        val (a, b, c, d) = (1, 2, 3, 4)
        extern castfn zeroify{n:int}(n: int(n)): int(0)
        extern praxi lemma_this_is_zero{n:int}(n: int(n)): [n == 0] void
        extern castfn make_less_than{n,m:int}(t: (int(n), int(m))): [o,p:int | o < p] (int(o), int(p))
        extern praxi lemma_less_than{n,m:int}(n: int(n), m: int(m)): [n < m] void
        prval _ = lemma_this_is_zero(m)
}

which has this output:

This is definitely zero: 5
This is definitely zero: -5
2 is less than 1
4 is less than 3

Are there cases that demand one of these over the other?

Answer 1

If you use 'castfn', you need to make sure that there is a corresponding implicit cast function in the target language. For instance, int2double is a castfn if C is the target language.

On the other hand, praxi/prfun is completely erased, having no trace in the generated code.

I would say that praxi/prfun is more general, but int2double is definitely not a praxi/prfun.