存在和重复见证

Question

让我们想象一下我有一个存在主义类型T.

T = ?X { a :: X,  f :: X -> Int} 

其中我产生了一个价值

v :: T
v = pack {Int, { a = 0, f x =  0 } } as T

所以:

• 禁止此值的用户知道X实现中实际使用的是哪种类型.为了消耗这个值,他们的代码必须是多态的X
• 另一方面,实现者完全知道X实际上是一个Int并且可以根据自己的意愿使用基础类型的能力

我想知道是否有这种机制的变体不会破坏证据:

w, v = pack {Int, { a = 0, f x =  0 } } as T
s = unpack w v  -- recovers type information 

这里w将是型方程搭售的价值层面的证据X来int.我们的想法是在代码的另一部分中有选择地重用实现,并具有非多态代码.为了拥有通常的存在行为,我们可以忽略w返回的.

我想一个能投X到Int,放弃类型安全,但这是另一个故事:如果我知道这个秘密v,就不是很有意义,我要能够秘密告诉别人,让编译器验证这个秘密被它赋予的代码使用.

是否已经尝试/这是最错误的部分？

Answer 1

使用单身人士

-- singleton for some types we are interested in
data S a where
   Sint  :: S Int
   Sbool :: S Bool

-- existential type, with a singleton inside
data T where
   T :: S a -> a -> (a -> Int) -> T

-- producer
t :: T
t = T Sint 3 succ

-- consumer
foo :: T -> Int
foo (T Sint  n     f) = f (n + 10)
foo (T Sbool True  f) = 23
foo (T Sbool False f) = f 3

如果你需要完整的monty,请使用Typeable.

data T where
   T :: Typeable a => a -> (a -> Int) -> T

-- consumer
foo :: T -> Int
foo (T x f) = case cast x of
   Just n  -> f ((n :: Int) + 10)
   Nothing -> 12   -- more casts can be attempted here