可以推断出一种类似反射的闭包类型吗？

Question

与以下“玩具模型”的冲突：

{-# LANGUAGE RankNTypes, KindSignatures, DataKinds, FlexibleContexts #-}

-- Simplified model of platform definitions
data Domain = DomSys | Dom25

data Signal (dom :: Domain)
data Clock (dom :: Domain)

class HiddenClock (dom :: Domain)

withClock :: Clock dom -> (HiddenClock dom => r) -> r
withClock _ _ = undefined

我想使用withClock关闭本地where块中的HiddenClock约束。假设我有以下两个层次的定义：

-- Simplified model of external standalone definitions
mainBoard :: (HiddenClock dom) => Signal dom -> Signal dom -> Signal dom -> (Signal dom, Signal dom)
mainBoard = undefined

peripherals :: (HiddenClock dom) => Signal dom -> Signal dom
peripherals = undefined

video
    :: Clock domVid
    -> Clock domSys
    -> Signal domSys
    -> Signal domSys
    -> (Signal domVid, Signal domSys, Signal domSys)
video = undefined

然后，我想写如下的东西：

topEntity :: Clock Dom25 -> Clock DomSys -> Signal DomSys -> Signal Dom25
topEntity clkVid clkSys input = vga
  where
    (vga, vidRead, line) = video clkVid clkSys vidAddr vidWrite
    (vidAddr, vidWrite) = withClock clkSys board

    board = mainBoard vidRead line p
      where
        p = peripherals input

不幸的是，GHC (至少在8.10.7时)无法推断出board的正确类型，这会导致withClock clkSys board与HiddenClock DomSys constriant的关系不太接近：

    • No instance for (HiddenClock 'DomSys)
        arising from a use of ‘mainBoard’
    • In the expression: mainBoard vidRead line p
      In an equation for ‘board’:
          board
            = mainBoard vidRead line p
            where
                p = peripherals input
      In an equation for ‘topEntity’:
          topEntity clkVid clkSys input
            = vga
            where
                (vga, vidRead, line) = video clkVid clkSys vidAddr vidWrite
                (vidAddr, vidWrite) = withClock clkSys board
                board
                  = mainBoard vidRead line p
                  where
                      p = peripherals input
   |
38 |     board = mainBoard vidRead line p
   |             ^^^^^^^^^^^^^^^^^^^^^^^^

    • No instance for (HiddenClock 'DomSys)
        arising from a use of ‘peripherals’
    • In the expression: peripherals input
      In an equation for ‘p’: p = peripherals input
      In an equation for ‘board’:
          board
            = mainBoard vidRead line p
            where
                p = peripherals input
   |
40 |         p = peripherals input
   |             ^^^^^^^^^^^^^^^^^

可以通过向board添加类型签名来解决这一问题。

    board :: (HiddenClock DomSys) => (Signal DomSys, Signal DomSys)

我的问题是:是否可以稍微修改这段代码，或者篡改withClock topEntity 等的确切类型，以使topEntity的定义没有在 board**?**绑定上的类型签名？

Answer 1

我不认为你真的能推断出这一点，我也不完全确定你为什么要这么做。在冲突中，HiddenClock在引擎盖下使用ImplicitParams。目前，您的board无法知道时钟来自何处。

您需要通过值clkSys传递时钟，或者显式地写入需要在类型级别上使用HiddenClock约束的时钟。

ImplicitParams实际上并不像普通类型的类约束那样工作。这个HiddenClock不是对dom的约束。您可以看到，尽管HiddenClock 'DomSys没有自由变量，但它仍然需要作为约束。

下面是一个使用平原Haskell (与ImplicitParams一起)解决问题的示例：

{-# LANGUAGE ImplicitParams #-}
{-# LANGUAGE RankNTypes #-}

module Temp where

withX :: Int -> ((?x :: Int) => r) -> r
withX x r =
  let ?x = x
  in r

somethingThanNeedsX :: (?x :: Int) => Int
somethingThanNeedsX = ?x + 2

foo :: Int
foo = bar
  where
    bar = withX 42 baz

    baz = somethingThanNeedsX

GHC告诉我：

Orig.hs:19:11: error:
    • Unbound implicit parameter (?x::Int)
        arising from a use of ‘somethingThanNeedsX’
    • In the expression: somethingThanNeedsX
      In an equation for ‘baz’: baz = somethingThanNeedsX
      In an equation for ‘foo’:
          foo
            = bar
            where
                bar = withX 42 baz
                baz = somethingThanNeedsX
   |
19 |     baz = somethingThanNeedsX
   |      

为了使这种工作正常进行，您要么需要在withX的定义中使用baz (显式地传递x/时钟)，要么需要显式地说明ImplicitParams依赖项。如果不需要完整类型的签名，只需使用ImplicitParams约束(使用PartialTypeSignatures)：

{-# LANGUAGE ImplicitParams #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE PartialTypeSignatures #-}

module Temp where

withX :: Int -> ((?x :: Int) => r) -> r
withX x r =
  let ?x = x
  in r

somethingThanNeedsX :: (?x :: Int) => Int
somethingThanNeedsX = ?x + 2

foo :: Int
foo = bar
  where
    bar = withX 42 baz

    baz :: (?x :: Int) => _
    baz = somethingThanNeedsX

这现在编译得很好(如果您真的需要的话，可以使用{-# OPTIONS_GHC -fno-warn-partial-type-signatures #-}禁用警告)：

Temp.hs:20:27: warning: [-Wpartial-type-signatures]
    • Found type wildcard ‘_’ standing for ‘Int’
    • In the type signature: baz :: (?x :: Int) => _
      In an equation for ‘foo’:
          foo
            = bar
            where
                bar = withX 42 baz
                baz :: (?x :: Int) => _
                baz = somethingThanNeedsX
    • Relevant bindings include foo :: Int (bound at Temp.hs:16:1)
   |
20 |     baz :: (?x :: Int) => _
   |