我可以使用DataKinds编写一个函数来返回由参数编码的类型的值吗？

Question

假设我有一种货币类型:

data Currency = USD | EUR | YEN

和存储int的Money类型,并由给定的Currency参数化(Currency被提升为具有DataKinds扩展名的类型).

data Money :: Currency -> * where
    Money :: Int -> Money c

是否可以编写一个函数,该函数moneyOf以其参数为货币值,并返回一个Money值,该值由相应的Currency值类型参数化？比如moneyOf :: Currency -> Money c,但我们得到的编译时保证c是从Currency值生成的类型？

Answer 1

不,但有解决方法.正如你所看到的,你需要写的类型是一样的东西moneyOf :: (c :: Currency) -> Int -> Money c,在这里c无论是在类型绑定,并在功能实现本身(moneyOf _ amt = Money amt).这不是我们在Haskell中可以做的事情.那么我们可以做些什么呢？有两种选择,取决于你真正想要多少.

选项1:代理. 定义多重类型

data Proxy (t :: k) = Proxy

这种类型背后的想法是,您可以使用Proxy :: Proxy t作为传递类型t的具体术语级表示的方式.因此,例如,我们可以定义:

moneyOf :: Proxy c -> Int -> Money c
moneyOf _ = Money

然后,我们可以称之为moneyOf (Proxy :: Proxy USD) 10获得Money 10 :: Money USD.你可以使用的一个技巧是改为给函数类型proxy k -> Int -> Money c(注意小写proxy!),这样就proxy可以与任意函数类型统一.¹这很适合将参数传递给函数以修复它们的返回类型,但它不是真的让你做任何事情.

正如您所描述的那样,我认为代理可能是最适合解决它的问题. (假设普通类型的签名,例如Money 10 :: Money USD,不起作用,那就是 - 当你可以使用它们时更简单!)

选项2:单身人士类型. 但是,如果您发现需要更多的通用性(或者您只是好奇),那么另一种方法是创建一个单例类型,如下所示:

data SingCurrency (c :: Currency) where
  SUSD :: SingCurrency USD
  SEUR :: SingCurrency EUR
  SYEN :: SingCurrency YEN

这被称为"单一类型",因为每个SingCurrency c只有一个成员(例如,SUSD类型的唯一值SingCurrency USD).现在,你可以写

moneyOf :: SingCurrency c -> Int -> Money c
moneyOf _ = Money

在这里,moneyOf SUSD 10评估为Money 10 :: Money USD.但仅凭这一点并没有给你带来任何超越使用的东西(除了少一点打字).当你想要制作它们时,单身人士会变得特别有趣:

class SingCurrencyI (c :: Currency) where
  sing :: SingCurrency c

instance SingCurrencyI USD where scur = SUSD
instance SingCurrencyI EUR where scur = SEUR
instance SingCurrencyI YEN where scur = SYEN

现在,如果您有SingCurrencyI c约束,则可以自动生成相应的SingCurrency c值sing,从而允许您从类型级别移动到术语级别.(请注意,虽然所有Currencys都是实例,但是SingCurrencyI如果你需要它,你需要明确指定约束.)我想不出任何好的例子,使用它在我的头顶; 我认为我的建议是只有当你发现自己处于一种你无法完成所需要的情况时才会使用单身人士,并意识到单身人士的额外类型 - 价值同步会对你有所帮助(而且你不能在哪里重新设计自己的情况).

如果你确实发现自己使用单件,那么机器就是在singletons包装中为你设置的,更一般的是:有一个数据系列Sing :: k -> *取代了SingCurrency; 并且有一个SingI :: k -> Constraint取代的类型类SingCurrencyI,它有单个成员sing :: SingI a => Sing a.还有一个功能withSingI :: Sing n -> (SingI n => r) -> r,允许您自由转换Sing n为SingI n(另一个方向是sing).(这些都是提供的Data.Singletons.)还有一些模板Haskell Data.Singletons.TH允许你写

singletons [d|data Currency = USD | EUR | YEN|]

在你的程序中,以定义顶层Currency与适当的一起类型Sing和SingI实例.(您需要启用以下语言扩展,得:KindSignatures,DataKinds,TypeFamilies,GADTs或ExistentialQuantification,ScopedTypeVariables和TemplateHaskell).

这真的很强大 - 它几乎像依赖类型,如果你眯眼 - 但它可能是一个巨大的痛苦使用.事实上,如果你想了解更多信息,那么就有一篇论文正是在谈论:"同性恋:依赖类型的Haskell编程的乐趣和痛苦",由Sam Lindley和Conor McBride撰写.对于那些已经考虑过这些想法的人来说,这绝对是可读的,尽管这些材料本身就很棘手; 但请注意,他们的符号略有不同.不幸的是,我不知道任何好的博客文章或教程式的介绍.

¹虽然我不确定类型系列的类型统一规则的状态.

²否则,包含的运行时字典sing将不会被传入,因此该值在运行时将不可用.