Scala类型级编程-表示层次结构
我正在学习Scala中的类型级编程，并且很好奇是否可以使用类型级编程来表示树或层次结构。 简单情况下，可以表示一个多级树。A_ | B_ |C |D | E 如何表示这样的结构？
在GHC.TypeLits中，someNatVal有什么作用（我们不能用natVal实现）？
我正在尝试理解GHC.TypeLits，特别是someNatVal。我理解了这篇博客中的使用方式，但是如同博客中提到的，相同的示例也可以使用natVal来实现：isLength :: forall len a. KnownNat len => Integer -> List len...
Scala类型约束以检查参数值
我正在尝试用Scala实现康威的超现实数。 超现实数定义为递归对——一对超现实数集合，称为左和右，使得右集合中的任何元素都不小于或等于左集合中的任何元素。 超现实数之间的“小于或等于”关系也是递归定义的：如果不存在左集合中的元素a使得y≤a，并且不存在右集合中的元素b满足b≤x，则我们说x ≤...
更改函数类型（->）的固定性？
在进行一些类型级计算时，我遇到了这样的问题：我想更改->的固定性，因为它不能与固定性为0的左结合类型运算符混合使用。我知道使用TypeOperators扩展和infixr 1 ->无法直接解决这个问题，因为它只会返回错误parse error on input ‘->’。 ...
我该如何提取这个多态递归函数？
我正在使用 GHC 7.8 进行一些有趣的事情，但遇到了一点问题。我有以下代码：mkResultF :: Eq k => Query kvs ('KV k v) -> k -> ResultF (Reverse kvs) (Maybe v) mkResultF Here ke...
如何证明类型级布尔值的双重否定？
我有以下模块： {-# LANGUAGE DataKinds, KindSignatures, TypeFamilies, RoleAnnotations #-} module Main where import Data.Coerce (coerce) -- logical negat...
在生产中使用索引Monad的经验报告？
在之前的问题中，我发现了 Conor McBride 的《厄运的 Kleisli 箭头》，当时我正在寻找一种将Idris示例编码为Haskell的方法。我的努力去理解 McBride 的代码并使其在 Haskell 中编译成功导致了这个 gist：https://gist.github.com...
具有类型约束的Haskell类型族实例
我正在尝试使用类型族表示表达式，但我似乎无法想出我想要写的约束条件，而且我开始觉得这似乎不可能。以下是我的代码： class Evaluable c where type Return c :: * evaluate :: c -> Return c data Neg...
何时在Haskell中使用存在类型和依赖对？
当需要使用专门的存在类型或依赖对（也称为依赖和或 sigma 类型）时应该怎么做呢？ 以下是一个示例。 下面是一个长度索引列表和依赖类型的复制函数。有关如何实现 replicateVect，请参见这个问题。以下代码使用了 singletons 库： data Vect :: Type -...
当我扩展定义时，为什么我的函数依赖冲突消失了？
我尝试在Haskell中实现整数类型。首先，我使用以下方法实现了自然数： data Zero data Succ a 我随后将其扩展到整数上，方法是 data NegSucc a 我决定创建一个Increment类来增加整数。这是我做的方式： {-# Language Funct...