测试一个断言，该断言指出某个内容不应该被编译。
问题 当我使用支持类型级编程的库时，我经常会写出像下面这样的注释（来自Paul Snively在2012年Strange Loop上的一个示例）： // But these invalid sequences don't compile: // isValid(_3 :: _1 :: _5...
为什么在类型级计算中需要Aux技术？
我相信我错过了一些东西，因为我对Shapeless还很陌生并且在学习中，但是何时实际上需要使用Aux技术呢？我看到它被用来通过将其提升到另一个“伴随”type定义的签名中来公开一个type语句。 trait F[A] { type R; def value: R } object F { t...
使用“Prolog in Scala”查找可用的类型类实例
考虑到https://speakerdeck.com/folone/theres-a-prolog-in-your-scala，我想要“滥用”Scala类型系统，以找到所有符合给定条件的CanBuildFrom实例。按照Prolog风格，我会评估以下伪代码： can_build_from(S...
类型级编程的一些例子是什么？
我不明白“类型级编程”是什么意思，也无法通过谷歌找到合适的解释。 请问有人能提供一个演示类型级编程的例子吗？对该范 Paradigm 的解释和/或定义也会很有用。
Haskell和Idris的区别：运行时/编译时在类型宇宙中的反映
因此，在Idris中编写以下内容是完全有效的。item : (b : Bool) -> if b then Nat else List Nat item True = 42 item False = [1,2,3] // cf. https://www.youtube.com/watc...
在GHC 7.6中匹配类型级别的Nat
我的问题最好通过一个例子来解释：type family Take (n :: Nat) (xs :: [k]) :: [k] type instance Take 0 xs = '[] type instance Take (n+1) (x ': xs) = x ':...
Haskell单例：SNat有什么好处
我正在尝试理解Haskell的单例模式。 在论文《使用单例的依赖类型编程》和他的博客文章《发布0.9版的单例模式！》中， Richard Eisenberg定义了数据类型Nat，它使用Peano公理定义了自然数：data Nat = Zero | Succ Nat 通过使用语言扩展，这种数据...
创建一个折叠函数，允许在每次重复函数调用后更改类型，以便在不使用递归的情况下调用函数n次。
我正在尝试使用一个定义在这里的dfold dfold :: KnownNat k => Proxy (p :: TyFun Nat * -> *) -> (forall l. SNat l -> a -> (p @@ l...
Haskell 类型级别相等性
Haskell的语法对于定义类型族有限制:(1) type family Length (xs :: [*]) where (2) Length '[] = 0 (3) Length (x ': xs) = 1 + Length xs 在等号（=）左侧的第（2）和第（3）行...
有“类型级组合子”吗？它们将来会存在吗？
在我看来，Haskell真正好用的部分是组合子（如(.)、flip、$和<*>等）。当需要时，我几乎可以创建新的语法。 以前有一段时间，我在做某件事情，如果能够"翻转"一个类型构造函数，那将非常方便。假设我有一个类型构造函数：m :: * -> * -> * 我...