notebook.community

Edit and run

Table of Contents

Practical Dependent Types in Haskell: Existential Neural Networks and Types at Runtime (Part 2) - Exercises

This IHaskell Jupyter notebook contains my attempts at the exercises posed at the end of Practical Dependent Types in Haskell: Existential Neural Networks and Types at Runtime (Part 2) by Justin Le.

Original author: David Banas capn.freako@gmail.com
Original date: January 14, 2018

Copyright © 2018 David Banas; all rights reserved World wide.

Language Pragmas, Imports, and Base Type Definitions





In [1]:



    


{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE ExplicitForAll #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}

import Control.Monad.Random
import Data.Binary
import Data.Singletons.Prelude
import Data.Singletons.TypeLits
import GHC.Generics (Generic)
import GHC.TypeLits
import Numeric.LinearAlgebra.Static
import qualified Numeric.LinearAlgebra.Static as LAS

data Weights i o = W { wBiases :: !(LAS.R o)
                     , wNodes  :: !(LAS.L o i)
                     }                      -- an "o x i" layer
  deriving (Show, Generic)

instance (KnownNat i, KnownNat o) => Binary (Weights i o)

data Network :: Nat -> [Nat] -> Nat -> * where
    O     :: !(Weights i o)
          -> Network i '[] o
    (:&~) :: KnownNat h
          => !(Weights i h)
          -> !(Network h hs o)
          -> Network i (h ': hs) o
infixr 5 :&~

putNet :: (KnownNat i, KnownNat o)
       => Network i hs o
       -> Put
putNet = \case
    O w     -> put w
    w :&~ n -> put w *> putNet n

getNet :: forall i hs o. (KnownNat i, KnownNat o)
       => Sing hs
       -> Get (Network i hs o)
getNet = \case
    SNil            ->     O <$> get
    SNat `SCons` ss -> (:&~) <$> get <*> getNet ss

instance (KnownNat i, SingI hs, KnownNat o) => Binary (Network i hs o) where
    put = putNet
    get = getNet sing

hiddenStruct :: Network i hs o -> [Integer]
hiddenStruct = \case
    O _    -> []
    _ :&~ (n' :: Network h hs' o)
           -> natVal (Proxy @h)
            : hiddenStruct n'

data OpaqueNet :: Nat -> Nat -> * where
    ONet :: Network i hs o -> OpaqueNet i o

type OpaqueNet' i o r = (forall hs. Network i hs o -> r) -> r

randomWeights :: (MonadRandom m, KnownNat i, KnownNat o)
              => m (Weights i o)
randomWeights = do
    s1 :: Int <- getRandom
    s2 :: Int <- getRandom
    let wB = randomVector  s1 Uniform * 2 - 1
        wN = uniformSample s2 (-1) 1
    return $ W wB wN

randomNet' :: forall m i hs o. (MonadRandom m, KnownNat i, KnownNat o)
           => Sing hs -> m (Network i hs o)
randomNet' = \case
    SNil            ->     O <$> randomWeights
    SNat `SCons` ss -> (:&~) <$> randomWeights <*> randomNet' ss

randomNet :: forall m i hs o. (MonadRandom m, KnownNat i, SingI hs, KnownNat o)
          => m (Network i hs o)
randomNet = randomNet' sing

Ex 1: Using continuation style existentials.

Implement putONet' and getONet' using the continuation-style existentials, instead.

The constructor style implementations are:

putONet :: (KnownNat i, KnownNat o)
        => OpaqueNet i o
        -> Put
putONet (ONet net) = do
    put (hiddenStruct net)
    putNet net

getONet :: (KnownNat i, KnownNat o)
        => Get (OpaqueNet i o)
getONet = do
    hs <- get
    withSomeSing hs \$ \ss ->
      ONet <$> getNet ss





In [2]:



    


putONet' :: (KnownNat i, KnownNat o)
         => OpaqueNet' i o Put
         -> Put
putONet' f = f $ \net -> do
  put (hiddenStruct net)
  putNet net
  
getONet' :: (KnownNat i, KnownNat o)
         => (forall hs. Network i hs o -> Get r)
         -> Get r
getONet' f = do
  hs  <- get
  withSomeSing hs $ \ss -> do
    net <- getNet ss
    f net

I struggled for a long time with the getONet' definition, above, before realizing that I needed nested monads. I was, instead, attempting different variations on this basic theme:





In [3]:



    


getONet'' :: (KnownNat i, KnownNat o)
         => (forall hs. Network i hs o -> Get r)
         -> Get r
getONet'' f = do
  hs  <- get
  net <- withSomeSing hs $ \ss -> getNet ss
  f net



    


















    






<interactive>:6:35: error:
    • Couldn't match type ‘hs0’ with ‘a’
        because type variable ‘a’ would escape its scope
      This (rigid, skolem) type variable is bound by
        a type expected by the context:
          Sing a -> Get (Network i hs0 o)
        at <interactive>:6:10-43
      Expected type: Get (Network i hs0 o)
        Actual type: Get (Network i a o)
    • In the expression: getNet ss
      In the second argument of ‘(&dollar)’, namely ‘\ ss -> getNet ss’
      In a stmt of a 'do' block: net <- withSomeSing hs &dollar \ ss -> getNet ss
    • Relevant bindings include ss :: Sing a (bound at <interactive>:6:29)

And not quite understanding what to do about that error. Of course, with the correct code available to stare at, now, the solution seems obvous. D'oh! :(

I think I'd like to discuss w/ Conal the deeper type-level interactions and significances present in this example.

Ex 2: Existentializing the entire network structure.

Work with an existential wrapper over the entire network structure (inputs and outputs, too):





In [4]:



    


data SomeNet where
  SNet :: (KnownNat i, KnownNat o)
    => Network i hs o
    -> SomeNet

(We need the KnownNat constraints because of type erasure, to recover the original input/output dimensions back once we pattern match)

And write:

  • A function to convert SomeNets to OpaqueNets. Return the OpaqueNet with existentially quantified i and o in continuation-style. (You can write a data type to return it in constructor-style, too, for funsies.)

  • randomSNet, returning m SomeNet.

  • While you’re at it, write it to return a random continuation-style SomeNet, too! (See the type of withRandomONet' for reference on how to write the type)

  • The Binary instance for SomeNet.

    Hint: Remember natVal :: KnownNat n => Proxy n -> Integer!

Hint: Remember that toSomeSing also works for Integers, to get Sings for Nats, too!

Conversion from SomeNet to OpaqueNet





In [5]:



    


sNetToONet :: (forall i o. OpaqueNet i o -> r) -> SomeNet -> r
sNetToONet f (SNet net) = f $ ONet net

Implementation of randomSNet, using constructor style





In [6]:



    


randomSNet :: forall m. (MonadRandom m)
           => Integer    -- # inputs
           -> [Integer]  -- hidden layer widths
           -> Integer    -- # outputs
           -> m SomeNet
randomSNet i hs o =
  withSomeSing i  $ \(SNat :: Sing (i  :: Nat)) ->
  withSomeSing o  $ \(SNat :: Sing (o  :: Nat)) ->
  withSomeSing hs $ \(ss   :: Sing (hs :: [Nat])) ->
    SNet <$> (randomNet' ss :: m (Network i hs o))

Original code, resultant error, and my commentary:

randomSNet i hs o =
  withSomeSing i \$ \case
    (SNat :: Sing i) -> withSomeSing o \$ \case
      (SNat :: Sing o) -> withSomeSing hs \$ \ss -> do
        SNet <$> (randomNet' ss :: m (Network i hs o))

:12:47: error:
• Expected kind ‘Nat’, but ‘a’ has kind ‘k20’
• In the first argument of ‘Network’, namely ‘i’
In the first argument of ‘m’, namely ‘Network i hs o’
In an expression type signature: m (Network i hs o)

:12:52: error:
• Expected kind ‘Nat’, but ‘a’ has kind ‘k1’
• In the third argument of ‘Network’, namely ‘o’
In the first argument of ‘m’, namely ‘Network i hs o’
In an expression type signature: m (Network i hs o)

Hmmm, I'm not sure why I'm getting the error, above. If I understand this excerpt from Justin's post:

main :: IO ()
main = do
    putStrLn "How many cats do you own?"
    c <- readLn :: IO Integer
    case toSing c of
      SomeSing (SNat :: Sing n) -> -- ...

Now, inside the case statement branch (the ...), we have type n :: Nat in scope! And by pattern matching on the SNat constructor, we also have a KnownNat n instance (As discussed in previous part).

correctly, then I should have what I need in i and o. That is, they should both have kind Nat.

I have suggested to Justin that he add an explanatory note, re: the necessity of typing n.

Implementation of randomSNet, using continuation style





In [7]:



    


withRandomSNet :: forall m r. (MonadRandom m)
           => Integer    -- # inputs
           -> [Integer]  -- hidden layer widths
           -> Integer    -- # outputs
           -> (forall i hs o. (KnownNat i, KnownNat o) => Network i hs o -> m r)
           -> m r
withRandomSNet i hs o f =
  withSomeSing i  $ \(SNat :: Sing (i  :: Nat)) ->
  withSomeSing o  $ \(SNat :: Sing (o  :: Nat)) ->
  withSomeSing hs $ \(ss   :: Sing (hs :: [Nat])) -> do
    n <- randomNet' ss :: m (Network i hs o)
    f n

Binary instance for SomeNet





In [8]:



    


instance Binary SomeNet where
  put (SNet (net :: Network i hs o)) = do
    put $ natVal (Proxy @i)
    put $ hiddenStruct net
    put $ natVal (Proxy @o)
    putNet net

  get = do
    i  <- get :: Get Integer
    hs <- get :: Get [Integer]
    o  <- get :: Get Integer
    withSomeSing i    $ \(SNat :: Sing (i  :: Nat  )) ->
      withSomeSing hs $ \(ss   :: Sing (hs :: [Nat])) ->
      withSomeSing o  $ \(SNat :: Sing (o  :: Nat  )) -> do
        n <- getNet ss :: Get (Network i hs o)
        return (SNet n)



    











In [12]:



    


:i R



    


















    



















In [ ]:

Content source: capn-freako/Haskell_Misc

Similar notebooks:

notebook.community | gallery | about