It reminds me of Idris, where the types can actually run programs (at compile time) as long as they can be proved to terminate, which is more often than I though.