Dependant types - Network dimension

[Cypher1]

Would it be possible to build a dependence on the dimensions of the networks so that there can't be runtime errors caused by incorrectly shaped networks?

Something like this:
https://blog.jle.im/entry/practical-dependent-types-in-haskell-1.html

Thanks

[blackgnezdo]

@Cypher1 Thanks for the link, it's interesting! You are right, it would be wonderful to have shapes be the first class citizens of type world. There are some edge cases like dynamic reshape where it may not work out, but majority of shape-related bugs can be avoided. I have a somewhat uneasy feeling about gradient construction code too.

I believe the shape-typed API can be constructed on top of the raw one that we currently have (though we may want to extend the stronger types down into generated code too). So, if you have some code lying around - do show us!

[Cypher1]

Hmm. The link I posted is my only experience with dependant types except for a few attempts at learning Agda.

Possibly when I finish my degree I'll be free to help out. I'd love to work on this.

[starper]

Here are two related blog posts: post 1 and post 2

[helq]

I'm currently working on this. I took the code from Monday Morning Haskell (the linked blog posts) and have been working on making the API less verbose, this is how far have I come so far:

main3 = runSession $ do
  (a :: Placeholder "a" '[2,2] Float) <- placeholder
  (b :: Placeholder "b" '[2,2] Float) <- placeholder
  result <- render $ a `add` b
  let (inputA :: TensorData "a" [2,2] Float) = encodeTensorData . fromJust $ fromList [1,2,3,4]
      (inputB :: TensorData "b" [2,2] Float) = encodeTensorData . fromJust $ fromList [5,6,7,8]
  runWithFeeds (feed b inputB :~~ feed a inputA :~~ NilFeedList) result

(PS: this is running code, it actually works, it type checks and fails if I change the sizes of the shapes or the names of the placeholders!. This is, I think, impressive, I've been basically just refactoring for a couple of days what James Bowen (the guy from the blog posts) wrote, I love the GHC compiler)

I hope to release the code next week. I still have some problems with some type functions (eg, Union don't work too well for this problem), but I think I could have the basics nailed down for next week.

[blackgnezdo]

@helq word of caution: you need to make sure that the original author releases their code under a compatible license if you are to contribute a derived version. Superficially, there's no license statement on the blog page which forces one to assume the most restrictive interpretation...

[helq]

@blackgnezdo I don't think this is a big problem, he released the code under the BSD license, this is the repo https://github.com/jhb563/HTensor/tree/dependent-placeholders.

Now, I'm not quite sure how to re-license that code to incorporate it to this project, this project is licensed under Apache 2. I suppose, that's not a big deal, but I'm not sure how should it be done precisely, what the LICENSE file should say? and where should the original author's name and mine's be? (Actually, I don't care much about me, I remember we concede some rights to Google once we ask the code to be merged, but it would be nice to know how to add those data to the code or to some sort of list)

[blackgnezdo]

@helq the easiest would be if the original author dual-licensed his code under Apache 2 in addition to BSD. Are you open to his @jhb563? (If you go there, changing the LICENSE file to include the name instead of "Author name" would also be a good idea)

[helq]

@blackgnezdo ok. While we wait for @jhb563, I thought I could make public the code I've been working on, https://github.com/helq/tensorflow-haskell-deptyped. After we resolve how to manage the licenses I will just copy the code to this repo and make a PR.

In the mean time, I'm working on rewriting the MNIST example to use dependent types (this could take me a week more, probably. There are many details to solve before the MNIST example works with dependent types without a hassle). I hope, after the MNIST example is working and the license thing is resolved, I'll PR.

[helq]

Ok, @jhb563 has changed the license. I should ask, is the licensing alright now? What is left to do? May I just change the license of my project too?
Thanks.

[blackgnezdo]

@helq I double checked and if we decide to depend on any external library, it has to be placed into third_party directory according to this document. Alternatively, submitting the code directly to the project via CLA process is also possible but needs to be done by the original copyright holder. Same goes for your code, you can keep it separate or sign a CLA when you submit PRs.

[helq]

@blackgnezdo I have changed the license of my code to be dual licensed into Apache and BSD3.
https://github.com/helq/tensorflow-haskell-deptyped/tree/706431224c85b2164fe815331046f6258b1afa3e

I have forked this repository and I have added my code to the root of it. I have relicensed yet again the code so it says "Copyright 2017 TensorFlow authors", is that right? What should be in the header of each license on each file, all the copyright holders? (or I ain't any copyright holder, and am I missing something?)

Anyway, here is the code https://github.com/helq/haskell/tree/deptyped [commit 91fbd8a235]

Can I make a PR now? (I have already signed the CLA) or is it necessary for @jhb563 to sign the CLA?

Thanks, and sorry for so much asking.

[blackgnezdo]

@helq apologies about delayed reply, work life interfered.

We looked a bit into the diff between the commit you sent and the tensorflow/haskell tree. My understanding is it adds a new package which doesn't require any new functionality in the tensorflow/haskell packages. If this is correct, I think we can safely keep dependent types work on the side. I'm happy to include a reference to this package to make it more discoverable for people who would like to use it.

My main motivation for this is to avoid sorting our licensing as it it seems the only copyright that can be on the code served in this repository can be that of TensorFlow Authors (so CLAs are required from all contributors).

[helq]

Wow, already a month! Sorry for the very late reply (I guess we all have work/home responsibilities).

@blackgnezdo Ok, I understand, then there is no need to merge the code (unless I start to make significant changes to this repo, I suppose). In this case, I would really appreciate if you could add a little reference to the README to indicate there are side projects extending the API.

Thank you for the replies. Oh! and happy holidays!

[fkm3]

Sure, added a link in #171. If you have a cool example or something, we can add that as a code snippet as well.

[helq]

@fkm3, something like this? (from here: https://github.com/helq/tensorflow-haskell-deptyped/blob/master/executable/Main.hs#L126)

{-# LANGUAGE DataKinds, ScopedTypeVariables #-}

import           Data.Maybe (fromJust)
import           Data.Vector.Sized (Vector, fromList)
import           TensorFlow.DepTyped

test :: IO (Vector 8 Float)
test = runSession $ do
  (x :: Placeholder "x" '[4,3] Float) <- placeholder

  let elems1 = fromJust $ fromList [1,2,3,4,1,2]
      elems2 = fromJust $ fromList [5,6,7,8]
      (w :: Tensor '[3,2] '[] Build Float) = constant elems1
      (b :: Tensor '[4,1] '[] Build Float) = constant elems2
      y = (x `matMul` w) `add` b -- y shape: [4,2] (b shape is [4.1] but `add` broadcasts it to [4,2])

  let (inputX :: TensorData "x" [4,3] Float) = encodeTensorData . fromJust $ fromList [1,2,3,4,1,0,7,9,5,3,5,4]

  runWithFeeds (feed x inputX :~~ NilFeedList) y

main :: IO ()
main = test >>= print

I first thought to copy the example from the README and change it to use dependent types. Once I did it, I noticed it was too long, so I opted to put it as a reference example in my README and wrote something simpler for this repo. Is it what you were asking for?

PS: thanks for the link! :)

[fkm3]

Sorry for the slow reply. I'm adding that example in #174, thanks! Also, feel free to send PRs for this sort of thing if you like (licensing issues aren't usually an issue).

[vertexcite]

Activity at https://github.com/helq/tensorflow-haskell-deptyped seems to have stopped. It does not seem to build with any versions later than TF v1.3. No commits since 4 months ago, still depends on stackage lts-8.13. Seems like a lot would be needed before that got merged into this repo, which is quite different from the impression the statement "May be merged with this repository in the future." in https://github.com/tensorflow/haskell/blob/master/README.md gives.

[helq]

@vertexcite, well, you're right. Unfortunately, I've stopped working on it because I had a lot of things to do in school. I would love to continue, but right now I have no time or motivation to follow.

I gotta say I learned a lot in the process, anybody who wants to play with the repo is welcome. I still remember some of the things the project is missing to be usable (like variable size tensors). I also remember how I had planned to add them. So, if you wanna continue with it and want some guidance, just open an issue.

Updating the stackage dependencies shouldn't be hard (I think, all that needs to be changed are the definitions of external libraries in stack.yaml), but if tensorflow's API (this repo) has changed, some more work could need to be done.

[stites]

Quick heads up -- the data haskell group pointed me in the direction of dimensions, from @achirkin, when integrating this into hasktorch (which is "statically-typed-first"). If anyone is planning on taking this on for tensorflow, you can ping me on gitter.im (also you should join the datahaskell group) -- and I can help out with debugging/passing along references.

[helq]

@stites The dimensions library looks very interesting indeed.

Just a little question to know if it is worth the hassle, can you declare a tensor with one dynamic dimension? In tensorflow (python) one can declare a tensor with a shape like [-1, 3, 4] (alternatively [None, 3, 4]) and then, at runtime, one can pass any arbitrary tensor (eg, [10, 3, 4] or [2, 3, 4])

I only managed to to declare "static" shapes (though, they can change at runtime, like forall n. KnowNat n => Tensor '[n, 3, 4], but because a forall cannot be used in a data declaration (or I don't seem to get it working) we cannot use this trick at all), so I'm curious if you can just put a wildcard dimension using the dimensions library.

[achirkin]

Hi @helq !
Indeed. Here is a small example. If you have some dimensions unknown, you can change Nat indexing to XNat that allows you to say either you know the exact dimension (N 4), or the dimension is unknown, but at least k (eg XN 3). Then, Dim (XN 3) can be pattern-matched against Dx to restore KnownDim n => Dim (n :: Nat)

[stites]

Another point of mention is that there is a SomeDims datatype -- an existentially quantified wrapper around Dims d -- that allows you to write tensor operations statically and only fill them at run time.