Memoize the result of satisfying a constraint

Question

I am searching for a function

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

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

such that the resulting as is only evaluated once for the supplied constraint.

Another short version

How can I make a value of some type a that can only be inspected in the presence of a proof of some constraint c?

Motivation

I have long sought after a general solution to memoizing values of the form:

C a => a

Where C is some constraint and a ranges over all types. With a Typeable constraint on a and some smart constructors it would be possible to safely memoize the spine of a trie for Typeable a => b by building a trie over TypeReps. This question is about the harder part, what to put at the leaves of such a trie.

If we can somehow get a into the leaves, the leaves of the trie would need to initially have a value C a => a for some concrete type a, since dictionaries for classes can't be looked up from the type. Looking up values from the trie would require the dictionary for C a. This would seem to amount to modifying the value held at the leaf of the trie based on the passed in dictionary.

If we can't somehow get a into the leaves, the leaves would have an even scarier type C a => b for a single b, and, in providing the dictionary we'd need to prove that the type a (and thus the dictionary) can be determined by what is held in b, which won't be any more powerful than a TypeRep.

Evil

It's tempting to reach into the bag of evil to build a constructor to hold at the leaves of a trie. Modifying the value held at the leaf of the trie based on the passed in dictionary isn't evil if there's only ever a single dictionary possible for each constraint.

Any "solution" to this could be extremely evil. I am assuming that there's only ever a single dictionary for any constraint. Reflection gives us another evil that can construct more than one dictionary for a constraint.

Disuade me from this evil.

Example

The following should not (and doesn't) memoize the result of providing the constraint 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

The output is

tracedC :: String
Yes
tracedC :: String
Yes

A solution would admit a similar example but only evaluate tracedC () :: TracedC [Char] -> String once outputting only

tracedC :: String
Yes
Yes

Related attempts

A map from types to values f a which could be used in monadic memoization with explicit side effects.

Answer 1

Pure Evil

We make a strict constructor around a value that's missing a constraint and an MVar.

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

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

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

It will only be used by smart constructors and deconstructors. In a module we wouldn't export the UpToSingle constructor.

We provide a smart constructor for it; constructing the constructor is equivalent to allocating the MVar.

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

We also provide a smart deconstructor. It uses whatever value's there or computes one with the provided dictionary. It relies on there being a single possible dictionary for 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

Evil Exemplified

Using the same example traced code as in the question.

{-# 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"

And UpToSingle in place of Memoized, upToSingle in place of the Memoized constructor, and withSingle in place of getMemoized

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

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

We get the desired output

tracedC :: String
Yes
Yes

Doubly Evil

Combined with reflection the evil of either UpToSingle or Given is revealed. Both of the last two lines should print the same thing. By substitution they are both 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)

They actually print the following:

7
9
7

The give 7 evaluated before the give 9 passed a different Given Integer dictionary to g1 than the give 9 would and had the side effect of changing the result of give 9 (withSingle (upToSingle given)). Either UpToSingle is evil for assuming dictionaries are unique or give is evil for constructing new non-unique dictionaries.

From TypeRep to Typeable

We can use the same trick of delaying when a constraint is discovered to build the leaves of a memo trie for Typeable a => f a. Conceptually the leaves of the trie are each one of the following 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

When constructing the trie, we don't have the Typeable a instances needed to construct the GDynamics. We only have a TypeRep. Instead we will steal the Typeable a instance provided when the value is accessed. A GDynamic value up to a Typeable a instance is the TypeRep, the definition of the value forall a. and an MVar to hold the actual GDynamic.

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

We don't export the UpToTypeable constructor, instead exporting only a smart constructor and deconstructor. When UpToTypeable is constructed we allocate the MVar.

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

When it is deconstructed the user provides a Typeable a instance. If it has the same TypeRep as that stored in the UpToTypeable we accept that as proof that the types are equal and use the provided Typeable a instance to fill in the value of the 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

This should be safe since future GHC versions will forbid user provided instances for Typeable.