函数返回GADT的任何构造函数的结果 [英] Function returning result of any constructor of a GADT

问题描述

当我尝试创建一个返回 Thing a （其中 Thing ）的函数时，我正在与typechecker发生争斗。 c>是GADT）。最简单的例子：



  { - ＃LANGUAGE GADTs，EmptyDataDecls＃ - } 
 module Main其中
 
  - 定义一个人为的GADT 
数据TFoo 
数据TBar 
数据Thing a where 
 Foo :: Int  - > Thing TFoo 
 Bar :: String  - > TBar 
 
 combine :: [Thing a] 
 combine = [Foo 1，Barabc] 
 
 main :: IO（）
 main = undefined 
  

类型检查者不满意 a 不符合 TBar 。大概这是因为它已经推断出 a 是 TFoo 。但是，这是令人惊讶的，因为使用常规的总和类型可以做到：

pre $ data Thing = Foo Int | Bar String

combine :: [Thing]
combine = [Foo 1，Barabc]


是否有返回GADT参数的类型参数？

除了人为的例子，我需要GADTs所以我可以输入特定的函数来仅使用 Foo ，但在此之前，我还需要返回 Thing s。

解决方案

您已将您的量词混在一起。 $ b

  combine :: [事物a] 
  

意味着（语法中隐含 forall ）

  combine：全部[事物a] 
  

基本上，合并需要无论 a 是什么，因为 a [Thing a] c $ c>由调用 combine 的代码选择。或者，换句话说，

   -  psuedo-Haskell 
 combine ::（a :: *） - > ; [事物a] 
  

combine 是一个函数它将一个类型作为参数并承诺构造该类型的 Things 的列表。 结合与这个类型签名的唯一可能的定义是 combine = [] ，再加上一堆愚蠢的定义，比如 [未定义] 等 combine = [Foo 1] 也不起作用，因为 a 没有被推断，因为它不是 combine 来设置 a ;这是用户。

你想要的

   -  psuedo-Haskell 
 combine :: [exists a。事情a] 
  

这意味着 combine 是一个事物的列表，每个事物都是一个未知类型的 Thing （并且每一个 Thing 都可以是不同类型）。 存在量词是 forall 的反面。这意味着 combine 的定义可以设置它想要的任何类型，用户将不得不处理它。 Haskell不支持 exists 开箱即用，所以您需要定义一个中间数据类型：

  data SomeThing = forall a。 SomeThing（Thing a）
  

使用通用量词创建存在性量化的语法略微落后，但想法是，你得到

  SomeThing :: forall a。事情a  - > SomeThing 
  

基本上消除了 a 是的。

然后您可以

  combine :: [ SomeThing] 
 combine = [SomeThing $ Foo 1，SomeThing $ Barabc] 
  

I'm currently having a fight with the typechecker when I try to create a function returning Thing a (where Thing is a GADT). A minimal contrived example:

{-#LANGUAGE GADTs, EmptyDataDecls #-}
module Main where

-- Define a contrived GADT
data TFoo
data TBar
data Thing a where
  Foo :: Int -> Thing TFoo
  Bar :: String -> Thing TBar

combine :: [Thing a]
combine = [Foo 1, Bar "abc"]

main :: IO ()
main = undefined

The typechecker gets unhappy that a doesn't match TBar. Presumably this is because it has already inferred that a is TFoo. But, this is surprising, because with regular sum types you can do:

data Thing = Foo Int | Bar String

combine :: [Thing]
combine = [Foo 1, Bar "abc"]

Is there anyway to return a type parametric over the GADT parameter?

Outside of the context of the contrived examples, I need GADTs so I can type certain functions to only take a Foo, but before that I need to also be able to just return a list of Things.

解决方案

You've got your quantifiers mixed up.

combine :: [Thing a]

means (the forall is implicit in the syntax)

combine :: forall a. [Thing a]

Essentially, combine needs to be a [Thing a] no matter what a is, because a is chosen by the code that calls combine. Or, in another sense,

-- psuedo-Haskell
combine :: (a :: *) -> [Thing a]

combine is a function that takes a type as argument and promises to construct a list of Things of that type. The only possible definition of combine with this type signature is combine = [], plus a bunch of dumb ones like [undefined], etc. E.g. combine = [Foo 1] would not work either, because a is not being inferred, because it's not combine that sets a; it's the user.

You want

-- psuedo-Haskell
combine :: [exists a. Thing a]

which means "combine is a list of things, and each thing is a Thing of some unknown type" (and every Thing can be of a different type). The exists quantifier is the flipside of forall. It means the definition of combine can set whatever type it wants and the user will have to deal with it. Haskell doesn't support exists out-of-the-box, so you need to define an intermediate data type:

data SomeThing = forall a. SomeThing (Thing a)

The syntax is a bit backwards for using the universal quantifier to create existential quantification, but the idea is that you get

SomeThing :: forall a. Thing a -> SomeThing

which essentially erases the knowledge of what a is.

You can then have

combine :: [SomeThing]
combine = [SomeThing $ Foo 1, SomeThing $ Bar "abc"]

这篇关于函数返回GADT的任何构造函数的结果的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！