haskell - 是否有可能推断出一种类似反射的闭包类型？

Question

用下面的Clash“玩具模型”:

{-# 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 block 内的 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 约束:

    • 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 board 的绑定(bind)没有类型签名的类型检查？

Answer 1

我不认为你真的可以推断出这一点，我也不完全确定你为什么需要这样做。 在 Clash 中，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
   |      

为了完成这项工作，您需要在 baz 的定义中包含 withX(明确传递 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) => _
   |