2

我试图很好地掌握种类、类型和术语（或值，不确定哪个是正确的）以及用于操作它们的 GHC 扩展。我知道我们可以使用 TypeFamilies 来编写带有 Types 的函数，现在我们还可以在某种程度上使用 DataKinds、PolyKinds 等来操作 Kinds。我读过这篇关于Singleton Types 的论文，虽然我还没有完全理解它，但它看起来很有趣。这一切都让我想知道，有没有办法创建一个基于 Term 或 Value 级别的计算来计算返回类型的函数？这是依赖类型实现的吗？

这是我在想的一个例子

data Type1
data Type2

f :: Type1 -> Type2 -> (Type1 or Type2)--not using Either or some "wrapper" ADT

- 更新 - - - -

基于这里的大量研究和帮助，我现在很清楚，无论我启用多少扩展，函数的返回类型永远不能基于 Haskell 中值级别的表达式来计算。所以我发布了更多我的实际代码，希望有人能帮助我决定前进的最佳方式。我正在编写一个以圆锥曲线和二次曲面为基本类型的小型库。对这些类型的操作涉及计算它们之间的交集。2个曲面的交点是圆锥曲线的一种类型，包括像点一样的退化（实际上除了圆锥之外还需要另一种类型的曲线，但除了点之外）。确切的曲线返回类型只能由运行时相交曲面的值确定。圆柱体 - 平面相交可以产生无、直线、圆或椭圆。我的第一个计划是像这样使用 ADT 来构造曲线和曲面......

data Curve = Point     !Vec3
           | Line      !Vec3 !UVec3
           | Circle    !Vec3 !UVec3 !Double
           | Ellipse   !Vec3 !UVec3 !UVec3 !Double !Double
           | Parabola  !Vec3 !UVec3 !UVec3 !Double
           | Hyperbola !Vec3 !UVec3 !UVec3 !Double !Double
           deriving(Show,Eq)

data Surface = Plane    !Vec3 !UVec3
             | Sphere   !Vec3 !Double
             | Cylinder !Vec3 !UVec3 !Double
             | Cone     !Vec3 !UVec3 !Double
             deriving(Show,Eq)

...这是最直接的，并且具有作为一个很好的封闭代数类型的优点，我喜欢。在这种表示中，交集的返回类型很简单，它只是曲线。这种表示的缺点是这些类型的每个函数都必须为每种类型进行模式匹配并处理所有排列，这对我来说似乎很麻烦。Surface-Surface 相交函数将有 16 个图案进行匹配。

下一个选项是保持每个 Surface 和 Curve 类型独立。像这样，

data Point     = Point     !Vec3                               deriving(Show,Eq)
data Line      = Line      !Vec3 !UVec3                        deriving(Show,Eq)
data Circle    = Circle    !Vec3 !UVec3 !Double                deriving(Show,Eq)
data Ellipse   = Ellipse   !Vec3 !UVec3 !UVec3 !Double !Double deriving(Show,Eq)
data Parabola  = Parabola  !Vec3 !UVec3 !UVec3 !Double         deriving(Show,Eq)
data Hyperbola = Hyperbola !Vec3 !UVec3 !UVec3 !Double !Double deriving(Show,Eq)


data Plane    = Plane    !Vec3 !UVec3                          deriving(Show,Eq)
data Sphere   = Sphere   !Vec3 !Double                         deriving(Show,Eq)
data Cylinder = Cylinder !Vec3 !UVec3 !Double                  deriving(Show,Eq)
data Cone     = Cone     !Vec3 !UVec3 !Double                  deriving(Show,Eq)

从长远来看，这似乎更灵活，而且很好且细化，但需要包装器 ADT 才能处理来自交集函数的多种返回类型或构建一般“曲线”或“表面”的列表因为他们之间没有任何关系。我可以使用类型类和存在来对它们进行分组，但是我失去了我不喜欢的原始类型。

这些设计中的妥协让我尝试了这个。

---------------------------------------------------------------
-- Curve Types
---------------------------------------------------------------
type Pnte = Curve PNT
type Line = Curve LIN
type Circ = Curve CIR
type Elli = Curve ELL
type Para = Curve PAR
type Hype = Curve HYP
-----------------------------------------------
data CrvIdx = PNT
            | LIN
            | CIR
            | ELL
            | PAR
            | HYP
-----------------------------------------------
data Curve :: CrvIdx → * where 
  Pnte :: !Vec3                                       → Curve PNT
  Line :: !Vec3 → !UVec3                              → Curve LIN
  Circ :: !Vec3 → !UVec3 → !Double                    → Curve CIR
  Elli :: !Vec3 → !UVec3 → !UVec3 → !Double → !Double → Curve ELL
  Para :: !Vec3 → !UVec3 → !UVec3 → !Double           → Curve PAR
  Hype :: !Vec3 → !UVec3 → !UVec3 → !Double → !Double → Curve HYP

---------------------------------------------------------------
-- Surface Types
---------------------------------------------------------------
type Plne = Surface PLN
type Sphe = Surface SPH
type Cyln = Surface CYL
type Cone = Surface CNE
-----------------------------------------------
data SrfIdx = PLN
            | SPH
            | CYL
            | CNE 
-----------------------------------------------
data Surface :: SrfIdx → * where
  Plne :: !Vec3 → !UVec3           → Surface PLN
  Sphe :: !Vec3 → !Double          → Surface SPH
  Cyln :: !Vec3 → !UVec3 → !Double → Surface CYL
  Cone :: !Vec3 → !UVec3 → !Double → Surface CNE

...起初我认为这会给我一些神奇的，两全其美的场景，我可以通过“曲线”引用任何曲线类型（如在列表或交集返回类型中）并且还具有完整类型可用（Curve CrvIdx）使用多参数类型类等以粒度样式编写函数。我很快发现这并不像我希望的那样工作得很好，正如这个问题所示。我一直顽固地继续用头撞墙，试图找到一种方法来编写一个函数，该函数可以根据运行时参数的几何属性从我的 GADT 中选择返回类型，现在意识到这不会发生。所以现在的问题是什么是表示这些类型以及它们之间的交互的有效和灵活的方式？谢谢。

4

1 回答 1

2

简短的回答：没有。您需要使用包装器 ADTData.Dynamic或类型族/关联类型。

类型族可能是最接近您想要的东西，但同样，类型需要能够在编译时确定。例如：

{-# LANGUAGE TypeFamilies #-}

data Red
data Green
data Blue

data Yellow
data Cyan
data Violet

type family MixedColor a b
type instance MixedColor Red Red      = Red
type instance MixedColor Red Green    = Yellow
type instance MixedColor Red Blue     = Violet
type instance MixedColor Green Red    = Yellow
type instance MixedColor Green Green  = Green
type instance MixedColor Green Blue   = Cyan
-- etc ..

mixColors :: c1 -> c2 -> MixedColor c1 c2
mixColors = undefined

在这里，mixColors函数本质上可以返回任何类型的值，但返回类型需要是类型族的实例，MixedColor 以便编译器可以根据参数类型推断实际的返回类型。

您可以使用类型族和类型类来构建相对复杂的类型函数，让您越来越接近依赖类型的功能，但这意味着您的数据需要使用足够的类型级别信息进行修饰，以生成所需的类型-计算。

如果您需要在类型中对数值计算进行编码，则最近引入的类型级自然数会很有用。

编辑：另外，我不确定你为什么不愿意使用 ADT（也许你需要更详细地描述你的用例？），因为编码例如一个函数可以返回或者正是Type1这种Type2信息的事实ADT 非常自然地编码并且习惯性地用于。

于 2013-02-19T07:38:50.880 回答