在 Haskell 中编译时间常数答案

【问题标题】：Compile time constant in Haskell在 Haskell 中编译时间常数
【发布时间】：2023-03-04 12:26:01
【问题描述】：

我正在尝试在 Haskell 中嵌入预先计算的数据。那是

catToMap li = Map.fromList $ zip [0..] li

cat1 = catToMap ["aa", "bb", "cc"]

dim = Map.size cat1

我想在类型定义中静态使用dim：

type Network = Grenade.Network
    '[Grenade.FullyConnected dim 20, Grenade.FullyConnected 20 1, Grenade.Logit]
    '[Grenade.D1 dim, Grenade.D1 20, Grenade.D1 1, Grenade.D1 1]

（从grenade库导入）

但是，上面给出了dim不在范围内的错误。

我也在尝试创建函数

import qualified Numeric.LinearAlgebra.Static as SA

-- | ith standard basis in Rn
stdbasis :: forall n . KnownNat n => Int -> SA.R n
stdbasis i = SA.vector [builder x| x <- [0..n-1]]
where
    builder j = if i == j then 1 else 0

但这给了我n不在范围内的错误。

我尝试解决第一个问题是使用模板 Haskell：

catToMap = $(\li -> Map.fromList $ zip [0..] li)

cat1 = $(catToMap ["aa", "bb", "cc"])

dim = $(Map.size cat1)

但它给了我错误

• Couldn't match expected type ‘Q Exp’
              with actual type ‘[a0] -> Map.Map Integer a0’
• The lambda expression ‘\ li -> (Map.fromList $ zip ... li)’
  has one argument,
  but its type ‘Language.Haskell.TH.Lib.ExpQ’ has none
  In the expression: \ li -> (Map.fromList $ zip [0 .. ] li)
  In the untyped splice: $(\ li -> (Map.fromList $ zip [0 .. ] li))

我想要实现的类似于 C++ 模板：

template <int size> Vector<n>
stdbasis(int i);

【问题讨论】：

第二个错误，n 确实不在范围内，你应该使用[0..i-1]。无论如何，我认为这没有多大好处，因为由于惰性编程，常量通常会计算一次。
@WillemVanOnsem 如果我每次都手动输入dim 的值，则容易出错且难以更改（例如，如果添加了新类别）。但是在编译时需要该值来构造Network

标签： haskell template-haskell

【解决方案1】：

模板 Haskell 是正确的方法，但您需要在正确的位置使用它并使用合适的 TH 构造函数。该点是您要使用依赖于值级计算的类型级数量的地方。 dim 仍然是值级别，但 Grenade.FullyConnected 的参数是类型级别，所以这就是你需要拼接的地方。

这是一个完整的（简化的）示例：

module Dimension where  -- No TH here, we just need a separate module
                        -- to put the value-level code whose results
                        -- are to be spliced into the type level
import Data.Map as Map

dim :: Integer
dim = fromIntegral $ Map.size cat1
 where catToMap li = Map.fromList $ zip [0..] li
       cat1 = catToMap ["aa", "bb", "cc"]

{-# LANGUAGE TemplateHaskell, TypeOperators, DataKinds #-}

module Main where    

import @987654321@
import Dimension
import @987654322@

type F = ℤ / $(pure . @987654323@ $ @987654324@ dim) -- this is where you'd define your Network type

main :: IO ()
main = print [0::F ..]

[0,1,2]

【讨论】：