幻影类型的动机是什么？
唐·斯图尔特（Don Stewart）在他的《大规模Haskell》演讲中提到了虚类型：data Ratio n = Ratio Double 1.234 :: Ratio D3 data Ask ccy = Ask Double Ask 1.5123 :: Ask GBP 我阅读了他关于它...
按类型索引与在 Idris 中包含类型的区别
我是一名有用的助手，可以为您翻译文本。 我目前正在学习使用Idris进行类型驱动开发这本书。 我有两个问题与第6章中示例数据存储的设计有关。该数据存储是一个命令行应用程序，允许用户设置存储在其中的数据类型，然后添加新数据。 以下是相关代码的部分内容（稍作简化）。 您可以在Github上查...
现代的GHC版本是否具有任何形式的证明擦除？
假设我有一个参数，仅为了类型系统的好处而存在，例如在这个小程序中：{-# LANGUAGE GADTs #-} module Main where import Data.Proxy import Data.List data MyPoly where MyConstr :: Proxy...
Haskell的“Const”函子是否类似于范畴论中的常函子？
我知道Haskell中很多名称都受范畴论术语启发，我正在尝试确切地理解类比的起点和终点。 类别Hask 我已经知道Hask不一定是一个范畴，因为严格/惰性和seq的一些技术细节，但现在我们先将其放在一边。 为了清晰起见， Hask的对象是具体类型，即kind为*的类型。 这包括函数类型...
Rust中的PhantomData如何工作？
在Rust中，我发现PhantomData的概念非常令人困惑。我广泛地使用它来约束我的基于FFI的代码中的对象生命周期，但我仍然不确定我是否正确地使用了它。 这是一个编造的示例，展示我通常如何使用它。例如，我不希望MyStruct的实例超过Context的实例存在：// FFI declar...
Haskell: 具有幻象变量的数据的异构列表
我目前正在学习存在量化、幽灵类型和GADTs。我该如何创建一个带有幽灵变量的数据类型的异构列表？例如： {-# LANGUAGE GADTs #-} {-# LANGUAGE ExistentialQuantification #-} data Toy a where TBool ::...
我该如何在线程之间共享包含虚指针的结构体？
我有一个结构需要针对类型进行通用性设计，但是该类型实际上并未包含在该结构中：它只是在该结构的方法中使用，而不是在该结构本身中。因此，该结构包括一个PhantomData成员： pub struct Map<T> { filename: String, phanto...
Scala：使用类型参数或抽象类型作为类型边界
假设我有以下内容： class Bounded[A] { type apply[C <: A] = C } 这段代码可以编译: implicitly[Bounded[Any]#apply[String] =:= String] 这个失败了： type Str = Bou...
定义幽灵类型 - 无法编译示例
我正在尝试了解幻影类型。我正在阅读Ralf Hinze的《有趣的幻影类型》。他使用了一个我从未见过且无法编译的关键字with。当我尝试时，会出现=的解析错误。 data Type t = RInt with t = Int | R...