Постоянная времени компиляции в Haskell

Question

Я пытаюсь встроить предварительно вычисленные данные в 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);

Answer 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 Data.Modular
import Dimension
import Language.Haskell.TH

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

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

[0,1,2]