Запомните результат удовлетворения ограничения

Я ищу функцию

{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ConstraintKinds #-}

memoC :: (c => a) -> (c => a)

чтобы результат a оценивался только один раз для поставленного ограничения.

Другая короткая версия

Как я могу сделать значение некоторого типа a, которое может быть проверено только при наличии доказательства некоторого ограничения c?

Мотивация

Я давно искал общее решение для запоминания значений формы:

C a => a

Где c - некоторое ограничение, а a - диапазоны по всем типам. С ограничением Typeable на a и некоторыми интеллектуальными конструкторами можно было бы безопасно memoize позвоночника trie для Typeable a => b, построив trie over TypeRep s. Этот вопрос касается более сложной части, что положить в листья такой тройки.

Если мы можем каким-то образом получить a в листья, у листьев trie сначала должно быть значение C a => a для определенного типа a, так как словари для классов не могут быть просмотрены с тип. Для поиска значений из trie потребуется словарь для C a. Это, по-видимому, означает изменение значения, хранящегося на листе trie на основе переданного в словаре.

Если мы не можем каким-то образом получить a в листья, у листьев будет еще более страшный тип C a => b для одного b, а при предоставлении словаря нам нужно будет доказать, что тип a (и, следовательно, словарь) можно определить тем, что удерживается в b, которое не будет более мощным, чем TypeRep.

Зла

Заманчиво добраться до мешка зла, чтобы построить конструктора, чтобы держаться у листьев три. Изменение значения, хранящегося на листе trie на основе переданного в словаре, не является злым, если для каждого ограничения существует только один словарь.

Любое "решение" этого может быть крайне злым. Я предполагаю, что существует только один словарь для любого ограничения. Reflection give нам другое зло, которое может построить более одного словаря для ограничения.

Откажитесь от этого зла.

Пример

Следующее не должно (и не делает) memoize результат предоставления ограничения TracedC String.

{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE FlexibleInstances #-}

import Debug.Trace (trace)

class TracedC a where
    tracedC :: () -> a  -- The () argument keeps a from being memoized in the dictionary for `TracedC a`

instance TracedC [Char] where
    tracedC _ = trace "tracedC :: String" "Yes"

newtype Memoized c a = Memoized { getMemoized :: c => a }

example :: Memoized (TracedC a) a
example = Memoized (tracedC ())

main = do
    let memo = example :: Memoized (TracedC [Char]) String
    putStrLn $ getMemoized memo
    putStrLn $ getMemoized memo

Выходной сигнал

tracedC :: String
Yes
tracedC :: String
Yes

Решение допускает аналогичный пример, но только оценивает tracedC () :: TracedC [Char] -> String после вывода только

tracedC :: String
Yes
Yes

Связанные попытки

Карта из типов в значения f a, которые могут быть использованы в монадической записке с явной стороны эффекты.

Ответы

Ответ 1

Pure Evil

Мы создаем строгий конструктор вокруг значения, которое не имеет ограничений и MVar.

{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ConstraintKinds #-}

import System.IO.Unsafe (unsafePerformIO)
import Control.Concurrent.MVar

data UpToSingle c a = UpToSingle (c => a) !(MVar a)

Он будет использоваться только интеллектуальными конструкторами и деконструкторами. В модуле мы не будем экспортировать конструктор UpToSingle.

Мы предоставляем для него интеллектуальный конструктор; построение конструктора эквивалентно распределению MVar.

upToSingle :: (c => a) -> UpToSingle c a
upToSingle a = UpToSingle a $ unsafePerformIO newEmptyMVar

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

fillMVar :: MVar a -> a -> IO a
fillMVar mvar a = do
    tryPutMVar mvar a
    readMVar mvar

withSingle :: c => UpToSingle c a -> a
withSingle (UpToSingle a mvar) = unsafePerformIO $ fillMVar mvar a

Пример зла

Используя тот же пример, что и в вопросе.

{-# LANGUAGE FlexibleInstances #-}

import Debug.Trace (trace)

class TracedC a where
    tracedC :: () -> a  -- The () argument keeps a from being memoized in the dictionary for `TracedC a`

instance TracedC [Char] where
    tracedC _ = trace "tracedC :: String" "Yes"

И UpToSingle вместо Memoized, UpToSingle вместо конструктора Memoized и withSingle вместо getMemoized

example :: UpToSingle (TracedC a) a
example = upToSingle (tracedC ())

main = do
    let memo = example :: UpToSingle (TracedC [Char]) String
    putStrLn $ withSingle memo
    putStrLn $ withSingle memo

Получаем желаемый результат

tracedC :: String
Yes
Yes

Doubly Evil

В сочетании с reflection раскрывается зло либо UpToSingle, либо Given. Обе последние две строки должны печатать одно и то же. Подстановкой они оба give 9 (withSingle (upToSingle given)).

main = do
    let g1 = upToSingle given :: UpToSingle (Given Integer) Integer
    let g2 = upToSingle given :: UpToSingle (Given Integer) Integer
    print $ give 7 (withSingle g1)
    print $ give 9 (withSingle g2)
    print $ give 9 (withSingle g1)

На самом деле они печатают следующее:

7
9
7

give 7, оцененный до give 9, передал другой Given Integer словарь на g1, чем give 9, и имел побочный эффект изменения результата give 9 (withSingle (upToSingle given)). Либо UpToSingle является злом, потому что словари уникальны или give является злом для создания новых неисторических словарей.

От TypeRep до Typeable

Мы можем использовать тот же трюк задержки, когда обнаружено ограничение для создания листов memo trie для Typeable a => f a. Понятно, что листы trie являются следующими из следующих GDynamic s.

{-# LANGUAGE GADTs #-}
{-# LANGUAGE ScopedTypeVariables #-}

import Data.Typeable
import Control.Monad (liftM)

data GDynamic f where
    GDynamic :: Typeable a => f a -> GDynamic f

unGDynamic :: Typeable a => GDynamic f -> Maybe (f a)
unGDynamic (GDynamic f) = gcast f

При построении trie у нас нет экземпляров Typeable a, необходимых для построения GDynamic s. Мы имеем только TypeRep. Вместо этого мы будем красть экземпляр Typeable a, предоставляемый при достижении значения. Значение GDynamic до экземпляра Typeable a - это TypeRep, определение значения forall a. и MVar для хранения фактического GDynamic.

data UpToTypeable f = UpToTypeable TypeRep (forall a. Typeable a => f a) !(MVar (GDynamic f))

Мы не экспортируем конструктор UpToTypeable, а экспортируем только интеллектуальный конструктор и деконструктор. Когда UpToTypeable построен, мы выделяем MVar.

upToTypeable :: TypeRep -> (forall a. Typeable a => f a) -> UpToTypeable f
upToTypeable r f = UpToTypeable r f $ unsafePerformIO newEmptyMVar

Когда он деконструируется, пользователь предоставляет экземпляр Typeable a. Если он имеет тот же TypeRep, который хранится в UpToTypeable, мы принимаем это как доказательство того, что типы равны, и используйте предоставленный экземпляр Typeable a для заполнения значения GDynamic.

withTypeable :: forall f a. Typeable a => UpToTypeable f -> Maybe (f a)
withTypeable (UpToTypeable r f mvar) = unsafePerformIO $ do
    if typeRep (Proxy :: Proxy a) == r
    then liftM unGDynamic $ fillMVar mvar (GDynamic (f :: f a))
    else return Nothing

Это должно быть безопасным, поскольку будущие версии GHC запретят использование экземпляров пользователя для Typeable.