Haskell - 我如何从值转换为类型？
假设我有以下数据类型和类型类（使用适当的语言扩展）: data Zero=Zero data Succ n = Succ n class Countable t where count :: t -> Int instance Countable Zero where ...
Vinyl: 编写记录类型别名
在 Vinyl 中，我可以定义一个类型别名来方便地将记录导出到其他模块中： import Data.Vinyl name = Field :: "name" ::: String age = Field :: "age" ::: Int type Person = ["name" ::: ...
数字类型签名
是否可以创建一个带有数值参数的类型？ 例如，如果我想要创建一个具有固定位宽的整数类型： newtype FixedWidth w = FixedWidth Integer addFixedWidth :: FixedWidth w -> FixedWidth w -> Fix...
Shapeless HList类型检查
我正在使用Shapeless，以下是我用来计算两个HList之间差异的方法： def diff[H <: HList](lst1: H, lst2:H):List[String] = (lst1, lst2) match { case (HNil, HNil) ...
如何在约束违规时创建自定义类型错误
我有一个类实例，它有一些相对不直观的限制。如果这个约束被违反，将会导致无法阅读的错误信息。我想要做的是提供一个自定义类型错误，以人类可读的方式解释约束。我已经看过这里，它似乎接近我想要的。然而，我想生成的TypeError基于约束违规，而不是实例声明。 以下是我想要实现的示例代码： dat...
创建完全依赖的连接操作
一个关于连接的有趣事实是，如果我知道等式中的任意两个变量： a ++ b = c 然后我知道了第三个。 我想在自己的concat中捕捉这个想法，所以我使用了一个函数依赖。 {-# Language DataKinds, GADTs, FlexibleContexts, Flexibl...
“a :~: b” 和 “(a :== b) :~: True” 之间有任何关联吗？
请问命题和推广的等式之间有任何联系吗？ 假设我有 prf :: x :~: y 一些 Symbol 的作用域内；通过模式匹配，将其转换为Refl，我可以将其转化为 prf' :: (x :== y) :~: True like this: fromProp :: (KnownS...
如何在Haskell中触发类型族模式匹配错误？
Haskell是否能指示类型系列匹配错误？例如，使用闭合类型系列： type family Testf a where Testf Char = IO () Testf String = IO () Testf Int的类型仅为Testf Int，编译器不会生成任何错误。如果...
在Scala中，是否有可能对def的类型参数进行“柯里化”？
假设我有一个带有多个类型参数的def： def foo[A, B, C](b: B, c: C)(implicit ev: Writer[A]) 然而，预期的用法是类型参数B和C应该根据传入的参数进行推断。 调用者只需要明确指定A（例如，让编译器选择适当的隐式对象）。不幸的是，Scala只...
为什么这段代码不违反类型族的“饱和要求”？
我有一个最小化的工作示例（从singletons库中提取），用于在类型级别列表上映射类型族： {-# language PolyKinds #-} {-# language DataKinds #-} {-# language TypeFamilies #-} {-# language Ty...