记住满足约束的结果

Question

我正在寻找一个函数

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

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

这样得到的as 只针对提供的约束计算一次。

另一个简短的版本

我怎样才能使某种类型的值 a 只能在存在某些约束证明 c 的情况下检查？

动机

长期以来，我一直在寻找记忆表单值的通用解决方案：

C a => a

C 是一些约束，a 涵盖所有类型。使用Typeable 约束a 和一些智能构造函数，可以通过在TypeReps 上构建trie 来安全地记忆Typeable a => b 的trie 的脊椎。这个问题是关于更难的部分，在这种树的叶子上放什么。

如果我们能够以某种方式将a 放入叶子中，那么对于某些具体类型a，trie 的叶子最初需要有一个值C a => a，因为无法从类型。从树中查找值需要C a 的字典。这似乎相当于根据传入的字典修改树的叶子中保存的值。

如果我们不能以某种方式将a 放入叶子中，那么对于单个b，叶子将会有一个更可怕的类型C a => b，并且，在提供字典时，我们需要证明该类型a（以及字典）可以由 b 中的内容来确定，它不会比 TypeRep 更强大。

邪恶

很想进入bag of evil 来构建一个构造函数来保存在树的叶子上。如果每个约束可能只有一个字典，那么根据传入的字典修改树的叶子中保存的值并不是坏事。

对此的任何“解决方案”都可能非常邪恶。我假设任何约束都只有一个字典。反射gives us another evil 可以为一个约束构造多个字典。

劝我远离这个邪恶。

示例

以下内容不应（也不会）记住提供约束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

相关尝试

A map from types to values f a 可以在 monadic memoization 中使用，具有显式副作用。

Answer 1

纯恶

我们围绕缺少约束和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

双重邪恶

结合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

当发现约束时，我们可以使用相同的延迟技巧来构建Typeable a => f a 的备忘录树的叶子。从概念上讲，树的叶子是以下GDynamics 之一。

{-# 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 时，我们没有构造 GDynamics 所需的 Typeable a 实例。我们只有一个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 实例。如果它与存储在UpToTypeable 中的TypeRep 相同，我们接受它作为类型相等的证明，并使用提供的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 提供实例。