I am trying (unsuccessfully) to create an "object" * in haskell at runtime with its type defined at runtime using dependent types.
I followed this tutorial on dependent types , and what they use to pass values at runtime is a function that takes Sing as a parameter and uses pattern matching on the value of Sing to get the number at runtime. But I do not have access to match the Sing to the template.
I thought the code below might work, but what I get is actually quite disappointing, the compiler tells me that the n from the type definition for randomNetwork is not the same n that I captured in the type definition of 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 xih) => !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 xio, CreatableNetwork xs (o ': rs)) => CreatableNetwork (x ': xs) (i ': o ': rs) where randomNetwork = (:~>) <$> createRandom <*> randomNetwork -- from Grenade.Layers.FullyConnected data FullyConnected io = FullyConnected !(FullyConnected' io) -- Neuron weights !(FullyConnected' io) -- Neuron momentum data FullyConnected' io = FullyConnected' !(R o) -- Bias !(L oi) -- Activations instance Show (FullyConnected io) where show FullyConnected {} = "FullyConnected" instance (KnownNat i, KnownNat o) => UpdateLayer (FullyConnected io) where type Gradient (FullyConnected io) = (FullyConnected' io) runUpdate = undefined createRandom = undefined instance (KnownNat i, KnownNat o) => Layer (FullyConnected io) ('D1 i) ('D1 o) where type Tape (FullyConnected io) ('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 => mx runUpdates :: LearningParameters -> x -> [Gradient x] -> x runUpdates rate = foldl' (runUpdate rate) class UpdateLayer x => Layer x (i :: Shape) (o :: Shape) where type Tape xio :: * runForwards :: x -> S i -> (Tape xio, S o) runBackwards :: x -> Tape xio -> 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 mn = L (Dim m (Dim n [[Double]]))
How can I determine the size of the “hidden layer” at runtime (without manually creating it)? How can I use the value that I captured at runtime at the level level?
Btw, this is a compilation error that I get using the code above:
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 ab) -- 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.
*: I know, we call them meanings (I think)