无法证明单例类型在生成类型类实例时是单例类型
假设我有一个类型类，证明Shapeless coproduct中的所有类型都是单例类型： import shapeless._ trait AllSingletons[A, C <: Coproduct] { def values: List[A] } object AllSi...
Haskell中的单例类型
作为对各种依赖类型形式化技术进行调查的一部分，我遇到了一篇倡导使用单例类型（只有一个成员的类型）来支持依赖类型编程的论文。 根据这个来源，在Haskell中，运行时值和编译时类型之间存在分离，当使用单例类型时可以模糊这种分离，因为它引入了类型/值同构。 我的问题是：在这方面，单例类型与类型...
Haskell单例：SNat有什么好处
我正在尝试理解Haskell的单例模式。 在论文《使用单例的依赖类型编程》和他的博客文章《发布0.9版的单例模式！》中， Richard Eisenberg定义了数据类型Nat，它使用Peano公理定义了自然数：data Nat = Zero | Succ Nat 通过使用语言扩展，这种数据...
运行时值的精细和存在类型
假设我想要将一些字符串和整数标识符进行映射，并且我希望我的类型能够防止运行时错误，因为有人试图查找超出范围的id。以下是一个简单直接的API： trait Vocab { def getId(value: String): Option[Int] def getValue(id: I...
使用Haskell编码“小于”
我希望一些Haskell专家能够帮助澄清一些问题。 通常的方式是否可以定义Nat（通过@dorchard Haskell中的单例类型）？ data S n = Succ n data Z = Zero class Nat n instance Nat Z instance Nat...
将一个特性限制在对象中？
有没有一种方法可以限制特质只能混入对象中？例如：trait OnlyForObjects { this: ... => } object Foo extends OnlyForObjects // --> OK class Bar extends OnlyForObjec...
证明一种类型不等式给GHC
出于教育目的，我一直在尝试通过使用各种语言扩展和单例类型来重构《Idris类型驱动开发》一书中的一个示例（即RemoveElem.idr），使其在Haskell中运行。这个示例的要点是一个函数，它能够从非空向量中删除一个元素，并且给出了该元素确实在向量中的证明。下面的代码是自包含的（适用于GH...
如何使用单例库中的依赖对类型Sigma？
如何使用singletons库中的依赖对类型Sigma？ 假设存在以下类型索引列表和复制函数： data Vect :: Nat -> Type -> Type where VNil :: Vect 0 a VCons :: a -> Vect n a ->...
我能否得到已知自然数n来暗示已知自然数(n * 3)等？
我正在使用这种形状的数据类型，使用来自linear的V:type Foo n = V (n * 3) Double -> Double 将其固定在n上非常重要，因为我希望能够确保在编译时传入了正确数量的元素。这是我的程序的一部分，在这里我正在做的事情与之独立。 对于任何KnownNat...