Run-time cost of dependently-typed programming with GHC

Question

I am programming a dependently-typed library in Haskell. Using profiling on my test executable I see something like:

commutativity' Math 1189 4022787186 29.1 27.2 29.1 27.2

commutativity' is basically (recursive) proof of the integer addition commutativity property for type-level integers. It is defined this:

commutativity' :: SNat n -> SNat m -> Plus (S n) m :~: Plus n (S m)
commutativity' SZ m = Refl
commutativity' (SS n) m = gcastWith (commutativity' n m) Refl

And then used in my library with gcastWith to prove the equivalence of various types.

So... 29% of my runtime is spent on something completely useless, since type-checking happens at compile-time.

I had naively assumed that this wouldn't happen.

Is there something I can do to optimize away these useless calls?

Answer 1

If you are very sure the proof term terminates you can use something like

unsafeProof :: proof -> proof
unsafeProof _ = unsafeCoerce ()

someFunction :: forall n m.  ...
someFunction = case unsafeProof myProof :: Plus (S n) m :~: Plus n (S m) of
   Refl -> ...

This must be used only on types having a single no parameters constructor, e.g. Refl for a :~: b. Otherwise, your program will likely crash or behave weirdly. Caveat emptor!

A safer (but still unsafe!) variant could be

unsafeProof :: a :~: b -> a :~: b
unsafeProof _ = unsafeCoerce ()

Note that you can still crash the program with that, if you pass bottom to it.

I hope one day GHC will perform this optimization safely and automatically, ensuring termination through static analysis.