时间戳

首页 > 解决方案 > 使用 `Proxy s` 绑定类型与使用 forall 绑定类型

haskell - 使用 `Proxy s` 绑定类型与使用 forall 绑定类型

问题描述

在以下示例中，我不清楚为什么toto会失败，而tata会起作用。

对此有什么解释吗？

{-# LANGUAGE AllowAmbiguousTypes  #-}
{-# LANGUAGE  TypeFamilies, KindSignatures, FlexibleContexts #-}
{-# LANGUAGE TypeApplications, FunctionalDependencies, MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables , GADTs, MultiParamTypeClasses, RankNTypes                #-}
{-# LANGUAGE TypeOperators, UnicodeSyntax, DataKinds              #-}

import Data.Proxy

data KNat where
class ReflectNum (s :: KNat) where

toto ∷ (∀ (s :: KNat). ReflectNum s ⇒ Int) → Int
toto k = toto k

tata ∷ (∀ (s :: KNat). ReflectNum s ⇒ Proxy s -> Int) → Int
tata k = tata (\(p :: Proxy s) -> k p)

错误是

SO.hs:14:15: error:
    • Could not deduce (ReflectNum s0) arising from a use of ‘k’
      from the context: ReflectNum s
        bound by a type expected by the context:
                   forall (s :: KNat). ReflectNum s => Int
        at SO.hs:14:10-15
      The type variable ‘s0’ is ambiguous
    • In the first argument of ‘toto’, namely ‘k’
      In the expression: toto k
      In an equation for ‘toto’: toto k = toto k
   |
14 | toto k = toto k
   |               ^

标签： haskelltype-level-computation

解决方案

这是 GHC 实现可见类型应用程序的一个已知限制。具体来说，Proxy有时仍然需要允许更高级别函数（例如您的toto函数）的参数访问类型变量。

有一个 GHC 提议以lambda-expressions 中的类型变量绑定的形式为这个问题添加一个解决方案。使用提案中的语法，您的toto函数可以写成

toto k = toto (\@s -> k @s)

本地绑定s变量。遗憾的是，该提议尚未实施。

同时，对于像这样的高级功能，我认为你只需要使用Proxy. 对不起。

推荐阅读