3

使用以下 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用来关闭本地块HiddenClock内的约束。where假设我有以下两个顶级定义：

-- 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？

4

1 回答 1

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
   |

为了使这项工作，您要么需要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) => _
   |
于 2022-02-20T15:59:58.087 回答