是否可以在运行时分配 KnownNat？

Question

我正在尝试（未成功）在运行时的 haskell 中创建一个“对象”*，其类型在运行时使用依赖类型定义。

我关注this tutorial on dependent types，他们用来在运行时传递值的是一个函数，该函数将Sing 作为参数并使用Sing 的值的模式匹配来获取运行时的数字。 但我无权访问任何 Sing 进行模式匹配。

我认为下面的代码可以工作，但实际上我得到的结果非常令人失望，编译器告诉我 randomNetwork 的类型定义中的 n 与我在类型定义中捕获的 n 不同的SNat。

{-# LANGUAGE
    ScopedTypeVariables, TemplateHaskell, TypeFamilies, GADTs, KindSignatures,
    TypeOperators, FlexibleContexts, RankNTypes, UndecidableInstances,
    FlexibleInstances, InstanceSigs, DefaultSignatures, DataKinds,
    RecordWildCards, StandaloneDeriving, MultiParamTypeClasses #-}

module Main where

-- some imports to make the code below main work
import Control.Monad.Random
import GHC.TypeLits
import Data.List

--import Grenade
import Data.Singletons
import Data.Singletons.TypeLits

main = do
  let sizeHidden = toSing (20 :: Integer) :: SomeSing Nat

  net0 <- case sizeHidden of
            SomeSing (SNat :: Sing n) ->
              randomNetwork :: IO (Network '[ FullyConnected 75 n, FullyConnected n 1 ] '[ 'D1 75, 'D1 n, 'D1 1 ])
  --net0 <- randomNetwork :: IO (Network '[ FullyConnected 75 3, FullyConnected 3 1 ] '[ 'D1 75, 'D1 3, 'D1 1 ])
  print net0


-- from Grenade.Core.Network
data Network :: [*] -> [Shape] -> * where
    NNil  :: SingI i
          => Network '[] '[i]

    (:~>) :: (SingI i, SingI h, Layer x i h)
          => !x
          -> !(Network xs (h ': hs))
          -> Network (x ': xs) (i ': h ': hs)
infixr 5 :~>

instance Show (Network '[] '[i]) where
  show NNil = "NNil"
instance (Show x, Show (Network xs rs)) => Show (Network (x ': xs) (i ': rs)) where
  show (x :~> xs) = show x ++ "\n~>\n" ++ show xs

class CreatableNetwork (xs :: [*]) (ss :: [Shape]) where
  randomNetwork :: MonadRandom m => m (Network xs ss)

instance SingI i => CreatableNetwork '[] '[i] where
  randomNetwork = return NNil

instance (SingI i, SingI o, Layer x i o, CreatableNetwork xs (o ': rs)) => CreatableNetwork (x ': xs) (i ': o ': rs) where
  randomNetwork = (:~>) <$> createRandom <*> randomNetwork

-- from Grenade.Layers.FullyConnected
data FullyConnected i o = FullyConnected
                        !(FullyConnected' i o)   -- Neuron weights
                        !(FullyConnected' i o)   -- Neuron momentum

data FullyConnected' i o = FullyConnected'
                         !(R o)   -- Bias
                         !(L o i) -- Activations

instance Show (FullyConnected i o) where
  show FullyConnected {} = "FullyConnected"

instance (KnownNat i, KnownNat o) => UpdateLayer (FullyConnected i o) where
  type Gradient (FullyConnected i o) = (FullyConnected' i o)
  runUpdate = undefined
  createRandom = undefined

instance (KnownNat i, KnownNat o) => Layer (FullyConnected i o) ('D1 i) ('D1 o) where
  type Tape (FullyConnected i o) ('D1 i) ('D1 o) = S ('D1 i)
  runForwards  = undefined
  runBackwards = undefined

-- from Grenade.Core.Layer
class UpdateLayer x where
  type Gradient x :: *
  runUpdate       :: LearningParameters -> x -> Gradient x -> x
  createRandom    :: MonadRandom m => m x
  runUpdates      :: LearningParameters -> x -> [Gradient x] -> x
  runUpdates rate = foldl' (runUpdate rate)

class UpdateLayer x => Layer x (i :: Shape) (o :: Shape) where
  type Tape x i o :: *
  runForwards    :: x -> S i -> (Tape x i o, S o)
  runBackwards   :: x -> Tape x i o -> S o -> (Gradient x, S i)

-- from Grenade.Core.Shape
data Shape = D1 Nat

data S (n :: Shape) where
  S1D :: ( KnownNat len )
      => R len
      -> S ('D1 len)

deriving instance Show (S n)

instance KnownNat a => SingI ('D1 a) where
  sing = D1Sing sing

data instance Sing (n :: Shape) where
  D1Sing :: Sing a -> Sing ('D1 a)

-- from Grenade.Core.LearningParameters
data LearningParameters = LearningParameters {
    learningRate :: Double
  , learningMomentum :: Double
  , learningRegulariser :: Double
  } deriving (Eq, Show)

-- from Numeric.LinearAlgebra.Static
newtype Dim (n :: Nat) t = Dim t
  deriving (Show)
newtype R n = R (Dim n [Double])
  deriving (Show)
newtype L m n = L (Dim m (Dim n [[Double]]))

如何在运行时定义“隐藏层”的大小（无需手动构建）？如何在类型级别使用我在运行时捕获的值？

顺便说一句，这是我用上面的代码得到的编译错误：

Prelude> :r
  net0 <- case sizeHidden of
            SomeSing (SNat :: KnownNat n => Sing n) -> randomNetwork :: IO (Network '[ FullyConnected 75 3, FullyConnected 3 1 ] '[ 'D1 75, 'D1 3, 'D1 1 ])
[1 of 1] Compiling Main             ( /home/helq/Downloads/NetworkOnRuntime.hs, interpreted )

/home/helq/Downloads/NetworkOnRuntime.hs:23:15: error:
    • Couldn't match type ‘a0’
                     with ‘Network
                             '[FullyConnected 75 a, FullyConnected a 1] '['D1 75, 'D1 a, 'D1 1]’
        because type variable ‘a’ would escape its scope
      This (rigid, skolem) type variable is bound by
        a pattern with constructor:
          SomeSing :: forall k k1 (k2 :: k1) (a :: k). Sing a -> SomeSing k,
        in a case alternative
        at /home/helq/Downloads/NetworkOnRuntime.hs:22:13-37
      Expected type: IO a0
        Actual type: IO
                       (Network
                          '[FullyConnected 75 a, FullyConnected a 1] '['D1 75, 'D1 a, 'D1 1])
    • In the expression:
          randomNetwork ::
            IO (Network '[FullyConnected 75 n, FullyConnected n 1] '[D1 75,
                                                                     D1 n,
                                                                     D1 1])
      In a case alternative:
          SomeSing (SNat :: Sing n)
            -> randomNetwork ::
                 IO (Network '[FullyConnected 75 n, FullyConnected n 1] '[D1 75,
                                                                          D1 n,
                                                                          D1 1])
      In a stmt of a 'do' block:
        net0 <- case sizeHidden of {
                  SomeSing (SNat :: Sing n)
                    -> randomNetwork ::
                         IO (Network '[FullyConnected 75 n, FullyConnected n 1] '[D1 75,
                                                                                  D1 n,
                                                                                  D1 1]) }

/home/helq/Downloads/NetworkOnRuntime.hs:25:3: error:
    • Ambiguous type variable ‘a0’ arising from a use of ‘print’
      prevents the constraint ‘(Show a0)’ from being solved.
      Relevant bindings include
        net0 :: a0 (bound at /home/helq/Downloads/NetworkOnRuntime.hs:21:3)
      Probable fix: use a type annotation to specify what ‘a0’ should be.
      These potential instances exist:
        instance (Show b, Show a) => Show (Either a b)
          -- Defined in ‘Data.Either’
        instance Show SomeNat -- Defined in ‘GHC.TypeLits’
        instance Show SomeSymbol -- Defined in ‘GHC.TypeLits’
        ...plus 31 others
        ...plus 170 instances involving out-of-scope types
        (use -fprint-potential-instances to see them all)
    • In a stmt of a 'do' block: print net0
      In the expression:
        do { let sizeHidden = ...;
             net0 <- case sizeHidden of {
                       SomeSing (SNat :: Sing n)
                         -> randomNetwork ::
                              IO (Network '[FullyConnected 75 n, FullyConnected n 1] '[D1 75,
                                                                                       D1 n,
                                                                                       D1 1]) };
             print net0 }
      In an equation for ‘main’:
          main
            = do { let sizeHidden = ...;
                   net0 <- case sizeHidden of { SomeSing (SNat :: Sing n) -> ... };
                   print net0 }
Failed, modules loaded: none.

*：我知道，我们称之为价值观（我认为）

Answer 1

让我们想想这一行：

net0 <- case sizeHidden of
    SomeSing (SNat :: Sing n) ->
        randomNetwork :: IO (Network '[ FullyConnected 75 n, FullyConnected n 1 ] '[ 'D1 75, 'D1 n, 'D1 1 ])

net0 的类型是什么？好像是

Network '[ FullyConnected 75 n, FullyConnected n 1 ] '[ 'D1 75, 'D1 n, 'D1 1 ]

但是，n 是什么？它不在环境中，因为main 的类型环境为空。它也没有被普遍量化。这就是问题所在，n 不能引用任何东西。您需要在绑定n 的环境中使用net0 完成所有工作¹，如

case sizeHidden of
   SomeSing (SNat :: Sing n) -> do
       net0 <- randomNetwork :: IO (Network '[ FullyConnected 75 n, FullyConnected n 1 ] '[ 'D1 75, 'D1 n, 'D1 1 ])
       print net0

或将net0 包装在它自己的存在中：

data DogeNet = 
  forall n. KnownNat n => DogeNet (Network '[ FullyConnected 75 n, FullyConnected n 1 ]
                                           '[ 'D1 75, 'D1 n, 'D1 1 ])

instance Show DogeNet where    -- deriving can't handle existentials
    show (DogeNet n) = show n 

main = do
    ...
    net0 <- case sizeHidden of
        SomeSing (SNat :: Sing n) ->
            DogeNet <$> (randomNetwork 
                           :: IO (Network '[ FullyConnected 75 n, FullyConnected n 1 ]
                                          '[ 'D1 75, 'D1 n, 'D1 1 ]))
    print net0

randomNetwork 仍然需要类型签名，因为我们需要表明我们确实打算使用上一行绑定的n，这迫使我们编写了两次网络规范。但是可以使用新的TypeApplications 扩展来清理它：

            DogeNet @n <$> randomNetwork

---

¹ 这并没有让事情像看起来那样不可能。您仍然可以将net0 传递给在n 中普遍量化的函数。这只是意味着，如果您曾经返回一个涉及 new 类型级别编号的类型，则需要通过 CPS 执行此操作，或者使用像 DogeNet 这样的存在。