在GADT中识别出datakind

Question

我不确定这是我希望我的设计看起来如何,但是有没有办法让我的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.

也许我的语法错了,或者我的要求太多了？

Answer 1

你的GADT语法很好,但只有类型的类型*可以有值,因为mt它被用作一个字段,它被强制*通过类型推断来实现.您尝试执行的操作的解决方法是创建一个所谓的单例类型,将自定义类型的类型映射到值级别.

data SMarketType mt where
    SWinDrawWin :: SMarketType WinDrawWin
    SAsianHandicap :: SMarketType AsianHandicap

data Market :: MarketType -> * where
    Instance :: SMarketType mt -> MarketIndex mt -> Market mt