使用DataKinds扩展更整洁地书写(Proxy :: Proxy 42)的方法

Question

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

(Proxy :: Proxy 42)

例如，有没有一个扩展程序，如果类型系统看到参数需要，它就会自动将文字42提升为(Proxy :: Proxy 42)？

我记得在某个地方看到过这样的扩展程序，但现在找不到了。让用户编写 (Proxy :: Proxy 42) 有点丑陋。

- Clinton

Answer 1

首先，如果你启用了PartialTypeSignatures，你可以省略一个Proxy：

{-# LANGUAGE PartialTypeSignatures #-}

(Proxy :: _ 42)

其次，GHC 8 中的 TypeApplications 是一种更为简洁的解决方案。它允许我们使用 @ 前缀显式地提供 forall 绑定的参数：

{-# 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

- András Kovács