Затраты времени на программирование с автоматическим программированием с GHC

Question

Я программирую библиотеку с зависимой типией в Haskell. Использование профилирования на моем тестовом исполняемом я вижу что-то вроде:

commutativity' Math 1189 4022787186 29.1 27.2 29.1 27.2 

commutativity' является в основном (рекурсивным) доказательством коммутативности собственности целое сложения для чисел типа уровня. Она определяется следующим образом:

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 

А затем используется в моей библиотеке с gcastWith, чтобы доказать эквивалентность различных типов.

Итак ... 29% моего времени выполнения потрачено на что-то совершенно бесполезное, так как проверка типов происходит во время компиляции.

Я наивно предположил, что этого не произойдет.

Есть ли что-то, что я могу сделать, чтобы оптимизировать эти бесполезные звонки?

Answer 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. В противном случае ваша программа, скорее всего, приведет к краху или ведет себя странно. Пусть покупатель будет бдителен!

Безопаснее (но по-прежнему небезопасно!) Вариант может быть

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

Обратите внимание, что вы можете разбить программу с тем, если вы передаете дно к нему.

Надеюсь, что однажды GHC выполнит эту оптимизацию безопасно и автоматически, обеспечивая окончание посредством статического анализа.