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?

This is the cost of not using a total language. Type safety rests on evaluating proofs to canonical form. In total languages, proofs can be trusted without evaluation and thus erased at runtime. You could take the trust hit and use unsafeCoerce, once you've checked your program gets past the typechecker. — pigworker
See section 4.4.4 "Running proofs" of Richard A. Eisenberg's thesis arxiv.org/abs/1610.07978 — danidiaz
I dream of GHC integrating a termination (abstract) checker, and automatically optimize/rewrite "proofs" using zero-cost coercions. That would be really nice. — chi
@pigworker I thought partial recursiveness was necessary for Turing completeness? — denormal
@denormal Well, consider that Turing-completeness may not be that important... most programs can be written in non-Turing-complete languages. Also, according to this answer you can somehow model partial functions in languages like Idris: my guess is that this is due to the fact that such languages also have codata and productive definitions (i.e. coinduction) which is often not considered, so it seems like termination+coinduction may be Turing-complete (but don't quote me on this). — Bakuriu

chi chi · Accepted Answer · 2016-12-30T22:02:08

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.

Run-time cost of dependently-typed programming with GHC

1 Answers