返回类型，作为术语或值计算的结果 [英] Return Type as a result of Term or Value calculation

问题描述

我试图很好地掌握Kinds，Types和amp;术语（或值，不确定哪个是正确的）以及用于操纵它们的GHC扩展。我明白我们可以使用TypeFamilies来使用Types编写函数，现在我们还可以在一定程度上使用DataKinds，PolyKinds等操作Kinds。我已经阅读过这篇关于Singleton Types的论文，尽管我还没有完全理解它，但它似乎很有趣。这一切都让我产生疑惑，是否有办法创建一个函数来计算基于期限或价值水平计算的回报类型？这是什么依赖类型实现？

这是我在想什么的例子

  data Type1 
 data Type2 
 
f :: Type1  - > Type2  - > （Type1或Type2） - 不使用Either或某些包装器ADT 
  

- 更新 - ------

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

  data Curve = Point！ Vec3 
 | Line！Vec3！UVec3 
 | Circle！Vec3！UVec3！Double 
 | Ellipse！Vec3！UVec3！UVec3！Double！Double 
 |抛物线！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 
 derived（Show，Eq）
  

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

下一个选项是让每个曲面和曲线类型保持独立。像这样，

  data Point = Point！Vec3派生（Show，Eq）
 data Line = Line！Vec3！ （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）
 
 
数据Plane = Plane！Vec3！UVec3派生（Show，Eq）
数据Sphere = Sphere！Vec3！Double派生（Show，Eq）
数据Cylinder = Cylinder！ Vec3！UVec3！Double deriving（Show，Eq）
 data Cone = Cone！Vec3！UVec3！Double deriving（Show，Eq）
  

从长远来看，这似乎更为灵活这很好，很精细，但需要一个包装器ADT来处理相交函数中的多个返回类型，或者建立一个通用的曲线或曲面列表，因为它们之间没有关系。我可以使用Type Classes和Existentials将它们分组，但是然后我失去了原来的类型，我不喜欢它。

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

  ------------------------------------------------- -------------- 
  - 曲线类型
 ------------------------ --------------------------------------- 
 type Pnte =曲线PNT 
 type Line =曲线LIN 
类型Circ =曲线CIR 
类型Elli =曲线ELL 
类型Para =曲线PAR 
类型Hype =曲线HYP 
 --- -------------------------------------------- 
 data CrvIdx = PNT 
 | LIN 
 | CIR 
 | ELL 
 | PAR 
 | HYP 
 --------------------------------------------- -  
 data Curve :: CrvIdx→*其中
 Pnte ::！Vec3→曲线PNT 
线::！Vec3→！UVec3→曲线LIN 
 Circ ::！Vec3 →！UVec3→！双→曲线CIR 
 Elli ::！Vec3→！UVec3→！UVec3→！双→！双→曲线ELL 
 Para ::！Vec3→！UVec3→！UVec3→！ Double→Curve PAR 
 Hype ::！Vec3→！UVec3→！UVec3→！Double→！Double→Curve HYP 
 
 -------------- ------------------------------------------------- 
  - 表面类型
 --------------------------------------- ------------------------ 
类型Plne =表面PLN 
类型Sphe =表面SPH 
类型Cyln =表面CYL 
类型Cone =表面CNE 
 ------------------------------------ ----------- 
 data SrfIdx = PLN 
 | SPH 
 | CYL 
 | CNE 
 --------------------------------------------- -  
 data Surface :: SrfIdx→*其中
 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中选择返回类型，现在认识到这不会发生。所以现在问题是什么将是一种高效而灵活的方式来表示这些类型及其之间的相互作用？谢谢。

解决方案

简短回答：不。您需要使用包装ADT， Data.Dynamic 或 type-family / associated
type 。

类型系列可能是您想要的最接近的东西，但再次，
类型需要能够在编译时决定。例如：

  { - ＃LANGUAGE TypeFamilies＃ - } 
 
 data Red 
 data绿色
数据蓝色
 
数据黄色
数据青色
数据紫色
 
类型系列MixedColor ab 
类型实例MixedColor红色红色=红色
类型实例混合颜色红色绿色=黄色
类型实例混合颜色红色蓝色=紫色
类型实例混合颜色绿色红色=黄色
类型实例混合颜色绿色绿色=绿色
类型实例MixedColor绿色蓝色=青色
  - 等等.. 
 
 mixColors :: c1  - > c2  - > MixedColor c1 c2 
 mixColors = undefined 
  

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

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

最近推出的类型级自然数可以是有用的，如果你需要在你的类型编码
数值计算。

编辑：另外，我不知道为什么你不愿意使用ADT （也许你需要描述你的使用c是否更详细？），因为编码例如函数可以返回 Type1 或 Type2 的事实恰恰是 类型的信息ADT编码非常自然，并被惯用于。

I'm trying to get a good grasp on Kinds, Types & Terms(or Values, not sure which is correct) and the GHC extensions for manipulating them. I understand that we can use TypeFamilies to write functions with Types and now we can also manipulate Kinds to some extent using DataKinds, PolyKinds etc. I have read this paper on Singleton Types which seems interesting although I don't fully understand it yet. This has all led me to wonder, is there a way to create a function that calculates the return Type based on calculation at the Term or Value level? Is this what Dependent Types achieve?

Here's an example of what I'm thinking

data Type1
data Type2

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

--Update--------

Based on alot of research and help here, it's become clear to me now that no matter how many extensions I enable, the return type of a function can never be calculated based on expresions at the value level in Haskell. So I'm posting more of my actual code in hopes that someone will help me decide on the best way to move forward. I'm writing a small library with conic curves and quadric surfaces as the basic types. The operations on these types involves calculating the intersections between them. The intersection of 2 surfaces is one of the types of conic curves, including degenerates like a point(there actually needs to be another type of curve besides the conics, but that besides the point). The exact curve return type can only be determined by the values of the intersecting surfaces at run time. A Cylinder - Plane intersection can result in Nothing, Line, Circle or Ellipse. My first plan was to structure the curves and surfaces using ADT's like this...

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)

...which is the most straight forward and has the advantage of being a nice closed algebraic type, which I like. In this representation the return type of the intersection is easy, it's just Curve. The downside of this representation is that every function of these types has to pattern match for each type and handle all the permutations which seems cumbersome to me. The Surface-Surface intersection function would have 16 patterns to match on.

The next option is to keep each Surface and Curve type individual. Like so,

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)

This seems like it might be more flexible in the long run and is nice and granular but would require a wrapper ADT to be able to handle the multiple return types from the intersection function or to build a list of general "Curves" or "Surfaces" because there is no relationship between them. I could use Type Classes and existentials to group them, but then I lose the original type, which I don't like.

The compromises in these designs led me to try this..

---------------------------------------------------------------
-- 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

...which at first I thought was going to give me some magical, best of both worlds scenario where I could refer to any curve type by "Curve" (like in a list or the intersection return type) and also have the full type available (Curve CrvIdx) to write functions in the granular style using multiparameter type classes, etc.. I soon discovered that this does not work quite as nicely as I hoped as is shown in this question. I have stubbornly continued to bang my head against the wall trying to find a way to write a function that can choose a return type from my GADT based on the geometric properties of the arguments at runtime and now realize this is not going to happen. So now the question is what would be an efficient and flexible way to represent these types and the interactions between them? Thanks.

解决方案

Short answer: no. You need to use a wrapper ADT, Data.Dynamic or a type-family/associated type.

Type families are probably the closest thing to what you want, but again, the type needs to be able to be decided at compile time. For example:

{-# 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

Here, the mixColors function can essentially return values of any type, but the return type needs to be an instance of the type family MixedColor so that the compiler can infer the actual return type based on the argument types.

You can use type families and type-classes to build relatively complex type-functions, getting you closer and closer to the functionality of dependent types, but that means your data needs to be decorated with enough type-level information to make the required type-calculations.

The recently introduced type-level natural numbers can be useful if you need to encode numerical calculations in your types.

EDIT: Also, I'm not sure why you are reluctant to use ADTs (maybe you need to describe your use-case in more detail?), because encoding e.g. the fact that a function can return either Type1 or Type2 is exactly the kind of information that ADTs encode very naturally and are idiomatically used for.

这篇关于返回类型，作为术语或值计算的结果的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！