记住满足约束的结果

Question

我正在寻找一个功能

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

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

这样得到的as仅针对所提供的约束进行一次评估.

另一个简短版本

如何创建某种类型的值,a只有在存在某些约束的证明时才能检查c？

动机

我一直在追求一种通用的解决方案来记住表格的价值:

C a => a

所有类型的C约束和a范围都在哪里.通过Typeable约束a和一些智能构造器,可以Typeable a => b通过在TypeReps上构建trie 来安全地记住trie的脊柱.这个问题是关于更难的部分,在这样一个特里的叶子上放什么.

如果我们可以以某种方式a进入叶子,则trie的叶子最初需要具有C a => a某种具体类型的值a,因为类的字典无法从类型中查找.查找trie中的值将需要字典C a.这似乎等于根据传入的字典修改trie叶子上保存的值.

如果我们不能以某种方式a进入叶子,叶子将会有一个更加可怕C a => b的单一类型b,并且,在提供字典时,我们需要证明类型a(因此字典)可以由什么是举行b,这将不会比一个更强大TypeRep.

邪恶

它很容易进入邪恶的袋子,建立一个构造者来抓住特里的叶子.如果每个约束只有一个字典可用,那么根据传入的字典修改trie叶子上保存的值并不是邪恶的.

任何"解决方案"都可能是非常邪恶的.我假设任何约束都只有一个字典.反思give是另一个可以为约束构造多个字典的邪恶.

劝我脱离这种邪恶.

例

以下内容不应该(也不会)记住提供约束的结果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可用于具有明显副作用的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

双重邪恶

结合反思任何一个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.从概念上讲,trie的叶子都是以下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时,我们没有Typeable a构造GDynamics 所需的实例.我们只有一个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.