在GADT中识别datakind
我不确定这是否是我希望我的设计看起来真实的样子，但是有什么方法可以让我的GADT看到mt参数必须有善良的MarketType，因为它是MarketIndex的类型参数
我认为当前的类型检查正在进行mt :: *，所以MarketIndex mt失败了，而不是我们需要在某个时候购买一个MarketIndex mt，因此必须限制mt :: MarketType。
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
module Market.TypesDK where
data MarketType = WinDrawWin
| AsianHandicap
deriving (Show)
type family MarketIndex (mt :: MarketType) :: *
type instance MarketIndex WinDrawWin = ()
type instance MarketIndex AsianHandicap = Double
data Market :: MarketType -> * where
Instance :: mt -> MarketIndex mt -> Market mt我得到的错误是：
[1 of 1] Compiling Market.TypesDK ( TypesDK.hs, interpreted )
TypesDK.hs:32:33:
The first argument of ‘MarketIndex’ should have kind ‘MarketType’,
but ‘mt’ has kind ‘*’
In the type ‘MarketIndex mt’
In the definition of data constructor ‘Instance’
In the data declaration for ‘Market’
Failed, modules loaded: none.也许我的语法弄错了，或者我要求太多了？
回答 2
Stack Overflow用户
发布于 2014-10-17 12:52:58
GADT语法很好，但是只有类型的*才能有值，而且由于mt被用作字段，所以它不得不通过类型推断对*进行分类。解决方法是创建一个所谓的单例类型，它将自定义类型的类型映射到值级别。
data SMarketType mt where
SWinDrawWin :: SMarketType WinDrawWin
SAsianHandicap :: SMarketType AsianHandicap
data Market :: MarketType -> * where
Instance :: SMarketType mt -> MarketIndex mt -> Market mtStack Overflow用户
发布于 2014-10-17 20:16:25
尚已经回答了。我只想补充一点，我发现在调试此类问题时提供显式类型/类注释是有用的。例如，用下面的种类注释代码
data Market :: MarketType -> * where
Instance :: forall (mt :: MarketType) . mt -> MarketIndex mt -> Market mt产生(可以说是)更清晰的信息：
期望一种类型，但在“Market”的数据声明中，“mt”在数据构造器“实例”的定义中的类型“mt”中有“MarketType”类
在您的错误中，mt被推断为后来与MarketIndex mt冲突的类型(:: *)。通过强制这样做，现在编写MarketIndex mt是可以的，但是现在错误声明mt应该是:: *，这会让人印象深刻。
IMHO，我希望错误沿着
类型构造函数( -> )有样* -> * -> *，但应用于‘mt->.’中的类‘MarketType’参数。
https://stackoverflow.com/questions/26423987
复制相似问题
腾讯云开发者
Copyright © 2013 - 2026 Tencent Cloud. All Rights Reserved. 腾讯云 版权所有
深圳市腾讯计算机系统有限公司 ICP备案/许可证号：粤B2-20090059 
粤公网安备44030502008569号
腾讯云计算（北京）有限责任公司 京ICP证150476号 | 京ICP备11018762号