我在 ReasonML 上玩了更多，发现type t以下示例中的模式匹配无法处理错误
错误：此模式匹配 t(float) 类型的值，但预期模式匹配 t(int) 类型的值 类型 float 与类型 int 不兼容
type t('a) =
| One: t(int)
| Two: t(float);
let x =
fun
| One => None
| Two => None;
现在在某种程度上，如果这是关于函数的返回类型，这对我来说是有意义的。
我找到了一个等价问题的答案（我认为）。对于第二部分，答案似乎是忽略构造函数的绑定类型。在 ReasonML 中是否可能相同？
Ps：请在术语上迂腐地纠正我，我还在学习什么是什么。
Pps：我知道我可以通过显式键入来解决原始问题，x但我真的很喜欢fun它的语法，因为它很有趣。
假设我有一个如下所示的 GADT：
data Tag = A | B | C
data Payload (tag :: Tag) where
PA :: Int -> Payload A
PB :: Double -> Payload B
PC :: Bool -> Payload C
我想要Payload自己没有运行时表示——即我想要Coercible Int (Payload A)，我想要零成本模式匹配，并且通常我希望它表现得好像我有以下三个 newtype 定义：
newtype PayloadA = PA Int
newtype PayloadB = PB Double
newtype PayloadC = PC Bool
有没有办法说服 GHC 给我那个？
Scala 3 现在有一种改进的方式来定义 ADT。一种语法糖，消除了用通常的方式做这些事情的所有麻烦sealed trait。
所以我会用一个例子来解释我的问题
enum Adt[+A]{
case Option1
case Option2
}
在本例中Option1和Option2的类型为Adt[Nothing]，因为类型参数A是协变的。
如果枚举是逆变的，那么它们的类型就是Adt[Any]。
但如果它是不变的呢？
我想编写一个函数，用 GADT 样式定义的数据结构将正则 lambda 表达式转换为 DeBrujin 样式。
{-# Language GADTs, StandaloneDeriving,ScopedTypeVariables #-}
module DeBrujin where
import Debug.Trace
import Data.List as L
data Apply
data Abstract
data Variable
data LambdaTerm a where
Var :: String -> LambdaTerm Variable
Abs :: String -> LambdaTerm a -> LambdaTerm Abstract
App :: LambdaTerm Abstract -> LambdaTerm a -> LambdaTerm Apply
instance Show (LambdaTerm a) where
show (Var v) = v
show (Abs s t) = "?" ++ s ++ "." ++ show t
show …type (_, _) eq = Equal: ('a, 'a) eq（来源）有什么用？我已经refl在 Coq 中使用过，但还不需要像 OCaml 中那样的东西。
该类型已在即将发布的 OCaml Stdlib 版本中定义Base，并且.
我如何知道何时使用此类型，以及使用此类型的代码是什么样的？
基地文档说：
Type_equal 的目的是表示类型检查器不知道的类型相等性，否则可能是因为类型相等性取决于动态数据，或者可能是因为类型系统不够强大。
所以听起来我正在寻找类型相等性依赖于动态数据或类型系统不够强大的示例，而类型equal是有帮助的。
我发现使用了
equal具有相同定义的类型，Stdlib.camlinternalFormat但不理解它
更新上面的基本文档中的引用可能不是具体eq的，并且可能与Base.Type_equal.Idiuc 更相关。
如何从Haskell中的(G)ADT参数获取构造函数作为函数？可以这样做吗？
data Ex1 = C1 Int | C2 Int -- | .....
| C3
fun :: Ex1 -> Ex1
fun C3 = C3
fun (c i) = c $ i^2
这对我来说不合适.
fun (C1 i) = C1 $ i^2
fun (C2 i) = C2 $ i^2