All geek questions in one place

Offline programming time with GHC

I am programming a labeled library in Haskell. Using profiling for 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 commutativity property of addition for level integers. This is defined:

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 it is used in my library with gcastWithto prove the equivalence of various types.

So ... 29% of my runtime is wasted on something completely useless, because type checking happens at compile time.

I naively assumed that this would not happen.

Is there anything I can do to optimize these useless challenges?

+4
1

, , -

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

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

, , . Refl a :~: b. , , . emptor!

( !)

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

, , .

, GHC , .

+1

Source: https://habr.com/ru/post/1665370/

More articles:


All Articles