Haskell: 具有幻象变量的数据的异构列表
我目前正在学习存在量化、幽灵类型和GADTs。我该如何创建一个带有幽灵变量的数据类型的异构列表？例如： {-# LANGUAGE GADTs #-} {-# LANGUAGE ExistentialQuantification #-} data Toy a where TBool ::...
不使用unsafeCoerce操纵存在量
最近我一直在研究这种类型，我理解它是自由分配函子的编码（关于这个的背景知识，请参见这个答案）： data Ev g a where Ev :: ((g x -> x) -> a) -> Ev g a deriving instance Functor (Ev g)...
对值进行存在量化
我在Scala语言规范（3.2.10 存在类型）中发现了关于值的存在量词。 x: y.Inner forSome{val y : Outer} 有没有一些关于IT技术的例子可以说明呢？ T forSome {val x: S}被定义为T forSome { type t <: S...
在 Prolog 中的全称量词和存在量词
我该如何在Prolog中实现以下规则。 我将“No spiders are mammals”这句话写成存在和全称量词：¬∃x(mammals(X) ∧ spider(X) ) //It is not the case that mammals are spider ∀X(mammals(X...
高阶函数中的存在类型
我有一个函数，其任务是根据类型为a->v的值函数计算某些最优值的类型a type OptiF a v = (a -> v) -> a 我有一个容器，想要存储这样一个函数和另一个使用这些值的函数： data Container a = forall v. (Ord v)...
模块与存在类型的区别
众所周知，OCaml模块其实就是“存在类型”。在某种程度上，它们之间存在一种平衡关系。 module X = struct type t val x : t end 并且 data 'a spec = { x : 'a } data x = X : 'a spec 这并不完全是无中...
在Haskell中是否可能拥有遗忘类型的同义词？
如果我有一个带有幽灵参数的类型，但是我只有时候关心它，就像这个例子： data Foo p a b = Bar a b 有没有什么简便的方法可以编写一个类型同义词 Baz，使得对于某些我已经忘记的p，Baz a b 是 Foo p a b？ 你不能这样做： type Baz a b ...
何时在Haskell中使用存在类型和依赖对？
当需要使用专门的存在类型或依赖对（也称为依赖和或 sigma 类型）时应该怎么做呢？ 以下是一个示例。 下面是一个长度索引列表和依赖类型的复制函数。有关如何实现 replicateVect，请参见这个问题。以下代码使用了 singletons 库： data Vect :: Type -...
存在类型表达式的斯科伦化
在Scala中，以下表达式会引发类型错误： val pair: (A => String, A) forSome { type A } = ( { a: Int => a.toString }, 19 ) pair._1(pair._2) 如SI-9899和这个答案中提到的那...
Typeably向下转换GADTs
假设我正在编写一种DSL，希望支持幻象类型和糟糕类型表达式。我的值类型可能是： {-# LANGUAGE GADTs, DataKinds #-} data Ty = Num | Bool deriving (Typeable) data Val a where VNum :: I...