более эффективные вычисления на уровне типа с использованием семейств типов?

Question

На основании статьи в Монада Reader, выпуск № 8, я закодированы до решения типа уровня к «Instant Insanity» головоломки, используя как функциональные зависимости и типа семьи:

• fundeps решение: http://lpaste.net/113108
• тип решения семейства: http://lpaste.net/113113

В fundeps растворы занимает около 200 секунд. тогда как версия семейств типов завершается примерно через 800 секунд.

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

Answer 1

Я добавил следующие определения main ваших двух фрагментов, так что решение показано в сообщении об ошибке типа жалуясь о пропавшем Show Например:

-- fundeps.hs 
{-# OPTIONS_GHC -fcontext-stack=400 #-} 
main = print $ solutions (undefined :: Cubes) 

-- families-open.hs 
{-# OPTIONS_GHC -ftype-function-depth=400 #-} 
data Proxy a = Proxy 
main = print (Proxy :: Proxy (Solutions Cubes)) 

и составил как с GHC 7.8. 3, чтобы получить некоторые базовые тайминги:

• fundeps.hs: 23s
• families-open.hs: 46s

Я обнаружил, что только преобразование типа семьи версии использовать закрытые семейства типа (код here) ускоряет его достаточно, чтобы разделить разницу:

• families-closed.hs: 36s

I подумал, что я могу ускорить его, добавив строгие виды семействам типов, используя DataKinds (код here), но, что удивительно, это вернуло меня к квадрату:

• families-closed-datakinds.hs: 44s

Однако, по крайней мере, он производит наиболее читаемый вывод всех четырех версиях:

No instance for (Show 
        (Proxy 
         '['['Cube 'G 'B 'W 'R 'B 'G, 'Cube 'W 'G 'B 'W 'R 'R, 
          'Cube 'R 'W 'R 'B 'G 'R, 'Cube 'B 'R 'G 'G 'W 'W], 
         '['Cube 'G 'B 'R 'W 'B 'G, 'Cube 'R 'R 'W 'B 'G 'W, 
          'Cube 'R 'G 'B 'R 'W 'R, 'Cube 'W 'W 'G 'G 'R 'B], 
         '['Cube 'G 'W 'R 'B 'B 'G, 'Cube 'W 'B 'W 'R 'G 'R, 
          'Cube 'R 'R 'B 'G 'W 'R, 'Cube 'B 'G 'G 'W 'R 'W], 
         '['Cube 'G 'R 'W 'B 'B 'G, 'Cube 'R 'W 'B 'G 'R 'W, 
          'Cube 'R 'B 'R 'W 'G 'R, 'Cube 'W 'G 'G 'R 'W 'B], 
         '['Cube 'G 'R 'B 'B 'W 'G, 'Cube 'W 'W 'R 'G 'B 'R, 
          'Cube 'R 'B 'G 'W 'R 'R, 'Cube 'B 'G 'W 'R 'G 'W], 
         '['Cube 'G 'W 'B 'B 'R 'G, 'Cube 'R 'B 'G 'R 'W 'W, 
          'Cube 'R 'R 'W 'G 'B 'R, 'Cube 'W 'G 'R 'W 'G 'B], 
         '['Cube 'G 'B 'B 'W 'R 'G, 'Cube 'W 'R 'G 'B 'W 'R, 
          'Cube 'R 'G 'W 'R 'B 'R, 'Cube 'B 'W 'R 'G 'G 'W], 
         '['Cube 'G 'B 'B 'R 'W 'G, 'Cube 'R 'G 'R 'W 'B 'W, 
          'Cube 'R 'W 'G 'B 'R 'R, 'Cube 'W 'R 'W 'G 'G 'B]])) 

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

Update на показателях производительности по состоянию на декабрь 2014

Как я уже отметил ранее, я опробовал эту же программу по линии развития GHC 7.9, а также, и нашел некоторые серьезные регрессии производительности. Это привело к a GHC bug ticket, который теперь разрешен к впечатляющим результатам: все три решения, включающие семейства типов, будут значительно быстрее проверять тип на предстоящей версии GHC 7.10!

Новые данные синхронизации (по состоянию на GHC a225c70) заключаются в следующем:

• families-open.hs: 7s
• families-closed.hs: 6.5s
• families-closed-datakinds.hs: 7.5s

Учитывая, что я при выполнении этих тестов без какой-либо строгости, вышеупомянутые три тайминга следует считать равными, что означает, что я wo uld определенно идут с закрытыми типами семейств + datakinds подход как наиболее типичный и тот, который производит самый приятный результат.