haskell - 使用 DataKinds 扩展的更简洁的写作方式(Proxy::Proxy 42)

Question

我一直在使用 DataKinds 扩展以类型安全的方式将类型级别 Nats 传递给函数，我只是想知道是否有更好的编写方式:

(Proxy :: Proxy 42)

例如，如果类型系统看到参数需要，是否有任何扩展会自动将文字 42 提升为 (Proxy::Proxy 42)？

我以为我在某个地方读到过，但现在找不到了。让用户写 (Proxy::Proxy 42) 我觉得有点难看。

Answer 1

首先，如果您启用 PartialTypeSignatures , 你可以省略 Proxy:

{-# LANGUAGE PartialTypeSignatures #-}

(Proxy :: _ 42)

第二，TypeApplications在 GHC 8 中是一个更整洁的解决方案。它让我们可以使用 @ 前缀显式地提供 forall 绑定(bind)的参数:

{-# LANGUAGE TypeApplications, RankNTypes, DataKinds, TypeFamilies #-}

import Data.Proxy
import GHC.TypeLits

foo :: forall (n :: Nat) a. a -> a
foo x = x

bar :: ()
bar = foo @10 () -- apply the type nat literal explicitly