Ship is an experimental implementation of dependent type theory, equipped with a computationally effective notion of type isomorphism. As befits Red Clydeside, closed terms evaluate to canonical forms.
Or at least, something of the sort might happen, eventually.