问题标签 [phantom-types]

For questions regarding programming in ECMAScript (JavaScript/JS) and its various dialects/implementations (excluding ActionScript). Note JavaScript is NOT the same as Java! Please include all relevant tags on your question; e.g., [node.js], [jquery], [json], [reactjs], [angular], [ember.js], [vue.js], [typescript], [svelte], etc.

0 投票
1 回答
98 浏览

haskell - 使用幻像参数强制类型类实例

我有

其中IFix是索引类型构造函数的类型级固定点,i是索引(幻像参数),IFunctor是实际上是函子的此类索引类型构造函数的类,f只是一个随机函数,g, hi尝试fIFix包装下传播。附注:这是一个简化的示例,实际上我经常在其他设置中遇到类似的问题,手动重新包装变得有点乏味(对于一个我想避免将 unwrap-rewrap 函数映射到列表或其他结构)。

老实说,我并不感到惊讶,但是由于我看不到强制的底层,我想知道,有没有办法修改我的定义,以便coerce可以应用?我试过RoleAnnotations但是

  1. type role IFix nominal phantom是无效的
  2. 我不知道如何为类型类要求类型角色(我担心没有办法,因为文档提到类型类假定参数是名义上的)

所以我的问题是,有没有办法让强制在这种情况下工作,如果没有,是否有任何深层原因为什么不这样做,或者这只是当前角色推理实现的限制。我的幼稚观点使我相信类型类可以对参数的角色施加约束,而实例必须满足约束。是否有一些有用的强制技巧的好来源?

0 投票
1 回答
93 浏览

haskell - 算术和幻象类型

我很想了解 arithmoi 包中幻象类型的使用(https://hackage.haskell.org/package/arithmoi-0.8.0.0)。它有助于检查我是否正在使用正确的残基类 ( Z/nZ)。

有问题的幻像类型是data Mod (n :: Nat) = Mod Natural,据我所知,构造函数没有导出。但是 的构造函数SomeMod是导出的,所以我想我必须用它来构造::Mod n变量。此外,可以阅读文档,但我不能使用它。

所以我尝试了:

我收到一个关于变量 m, m1 的错误,它正在逃逸其范围。我有点疑惑。

0 投票
1 回答
141 浏览

haskell - 类型声明中的类型限制

有一个类型级自然数的著名例子:

当我们应用类型构造函数时,我有一个关于理想限制的问题Succ。例如,如果我们想在函数定义中做这样的限制,我们可以使用类和上下文,就像下面的代码:

用不了toInt (undefined :: Succ Int),没关系。

但是如何实现对类型级别构造的类似限制(可能使用一些高级类型扩展)?

例如,我想允许类型构造函数Succ仅与类型Zero和某些东西一起使用,例如:Succ (Succ Zero)Succ (Succ (Succ Zero))等等。如何在编译时避免这样的坏例子:

(目前,没有编译错误)

PS:对我来说更有趣的是如何对最后一个样本的类型声明进行限制

0 投票
1 回答
128 浏览

haskell - 具有新数据的限制类型集,例如“树 a”

在 Haskell 中探索和研究类型系统我发现了一些问题。

1)让我们将多态类型视为二叉树:

而且,例如,我只想用 和 来限制我Tree IntTree Bool考虑Tree Char。当然,我可以制作一个这样的新类型:

但是是否有可能以更优雅(并且没有像T1, T2,之类的新标签T3)的方式(可能使用一些高级类型扩展)来制作新的受限类型(对于同质树)?

2)第二个问题是关于具有异质值的树。我可以用通常的 Haskell 来做,即我可以做新的帮助类型,包含标记的异构值:

然后用这种类型的值制作树:

但是是否有可能以更优雅(并且没有像H1, H2,之类的新标签H3)的方式(也许使用一些高级类型扩展)来制作新类型(用于异构树)?我知道异构列表,也许是同一个问题?

0 投票
2 回答
781 浏览

rust - PhantomData 类型在 rust 中的使用

我正在浏览一些 rust 源代码,我发现了一个名为PhantomData. 我正在浏览 rust 文档并在互联网上进行了很多搜索。但是,我无法理解这种数据类型与 rust 的实际用途。如果可能的话,有人可以用简单的方式解释一下吗?

0 投票
1 回答
84 浏览

scala - 无形。修改标记类型

例如,我有两种标记类型:

此类型用于处理模型。第一个用于通用模型,第二个用于db实体。

我的资源中有一个转换器:

此转换不会编译,导致e.created.toLocalDateTime返回LocalDateTime,但Entity需要LocalDateTime由 标记Created

所以我必须改变我的转换来tag[Created](e.created.toLocalDateTime)使这段代码编译。它有效,但是,恕我直言,它看起来有点难看。

Timestamp被 标记Created,并且一个新的LocalDateTime也必须被相同的标记Created

有什么方法可以修改标记类型而无需重新标记新的修改值?

0 投票
1 回答
72 浏览

haskell - ST类封装

我正在尝试使用类型系统来确保永远不会从 monad M 中取出 X。我希望它的工作方式类似于runST,在这种情况下,不可能混合来自不同线程的环境。

但是,以下代码不会导致类型错误:

为什么 ST monad 中的类似代码会抛出错误而我的不会?据我了解,sinM s a应该被绑定,使sinX s成为自由类型变量,从而导致类型检查器出错。

0 投票
1 回答
161 浏览

rust - 是否有一种安全、符合人体工程学的方法来更改复杂结构中的幻像类型?

假设我们定义了一个具有许多字段的通用结构,表示使用幻像类型的类型安全状态机:

然后我们可以编写一个类型安全的状态转换:

但是我们需要笨拙地解开每个字段并以不同的结构重新打包。

我们也可以使用mem::transmute,尽管我的理解是同一结构的不同单态化不能保证具有相同的内存布局。

我希望这Foo { state: PhantomData, ..self }会奏效;唉,它无法编译。

有什么规范的、符合人体工程学的、安全的方法来写这个吗?

0 投票
2 回答
1277 浏览

haskell - 现代 GHC 版本是否有任何类型的证明擦除?

假设我有一个仅为类型系统的利益而存在的参数,例如在这个小程序中:

结构中的 Proxy 参数和成员只需要在编译时存在,以帮助进行类型检查,同时维护多态 MyPoly(在这种情况下,程序将在没有它的情况下编译,但这个人为的示例是一个更普遍的问题,其中存在仅在编译时需要的证明或代理)- Proxy 只有一个构造函数,并且类型参数是幻像类型。

用 ghc with 编译-ddump-stg表明,至少在 STG 阶段,没有擦除构造函数的 Proxy 参数或构造函数的第三个参数。

有没有办法将这些标记为仅编译时,或者以其他方式帮助 ghc 进行证明擦除并排除它们?

0 投票
1 回答
3864 浏览

rust - PhantomData 在 Rust 中究竟是如何工作的?

我发现PhantomDataRust 中的概念相当混乱。我在基于 FFI 的代码中广泛使用它来限制对象的生命周期,但我仍然不确定我是否正确地执行了此操作。

这是我经常最终使用它的人为示例。例如,我不希望 的实例MyStruct比 的实例寿命长Context

我不太明白以下内容:

  1. marker: PhantomData从语法上讲,这到底是什么东西?我的意思是,它看起来不像构造函数,我希望它类似于PhantomData{}or PhantomData()

  2. 出于生命周期跟踪的目的,是否PhantomData甚至关心声明中的实际类型marker?我尝试将其更改为PhantomData<&'a usize>,它仍然有效。

  3. 在我的MyStruct::new()方法的声明中,如果我忘记显式指定参数的'a生命周期context,那么 的魔力PhantomData就会消失,并且可以丢弃Contextbefore MyStruct。这是相当阴险的;编译器甚至没有给出警告。那么它分配给什么生命周期marker,为什么?

  4. 与上一个问题相关;如果有多个输入引用参数可能具有不同的生命周期,如何PhantomData确定使用哪个生命周期?