Totality checking

[bbarker]

Just curious, does this support totality checking?

Background story: I was having issues with some MATLAB code not terminating written in a rather nonconventional way (for MATLAB, that is, i.e. functional). It occurred to me that if I could use generated C++ interfaces for my code in MATLAB, then I could handle the higher level logic from something like your Idris or PureScript compiler forks for C++. However, not really sure which of these would be better to use, though I don't think PureScript supports totality checking in any capacity (maybe I'm wrong). Also, Idris might provide a more compelling story for modeling matrices in MATLAB via dependent types, though that isn't really required for my current problem.

[andyarvanitis]

Interesting question. For purescript, there is some support (namely that functions need to be marked when partial). You can find some docs here and probably elsewhere with a bit of googling (sorry I don't know where offhand). You might want to check with the purescript guys on what it does exactly and how good it is. My C++ and Golang backends don't have anything special going on at the type level vs js purescript. Note that my backends are now just utilities on the mainline corefn output, not forks (though the C++ one was in the past).

As for Idris, I'm afraid I haven't been paying attention (in a long time), but it certainly had interesting things going on w.r.t. a totality checker. I stopped doing any alternative backends for it a long time ago, though.