differentiable programming on idris,why? (WIP!)
Due to the extreme flexibility of pytorch,I am going to bind to pytorch cpp instead of tensorflow
Learn & Research dependent types with deep learning
Elaborator reflection,maybe the most advanced macro system ,will make our great statically typed functional code terse and beautiful
Utilize existing efforts on optimizations for deep learning,rather than a whole new framework
depGraph2 : FreeGraphD $ (TensorD ,TensorD ) depGraph2 = do in1<-liftF $ PlaceholderD  out1<-liftF $ PlaceholderD  out2<-PlaceholderD  -- using implicits pure (in1,out1) compGraphD : FreeGraphD $ TensorD  compGraphD = do (in1,out1)<-depGraph2 pure in1
1.verify tf c lib is installed
ls /usr/lib | grep tensor should give sth like: libtensorflow_framework.so libtensorflow.so
2.install idris-free package with freer
https://github.com/idris-industry/idris-free (not merged yet)
then idris-emacs mode will load fine (you can take a look at .ipkg file)
warning! idris-free is also under active development,please check dependencies are the newest!
idris Ffi.idr -o idr ./idr
which should output your installed tf version
Construct idris computation graph with free monad approach,transform it and send to tf c api
c_api.h is the tf low level api,we can get
op , for exmaple,matmul,placeholders,variables,etc,with TF_newOperation . Unfortunately,there is not a type-safe list for such operations.
At high level, User defined computation graph would be optimised and then transformed to tf graph.
Elabs.idr : macros UserApi : user level graph construction and ops ,with freer monad Ffi : tf ffi bindings , link to /usr/include/tensorflow/c/c_api.h Midlevel : anything else between userapi and FFi
Free monad: https://github.com/idris-hackers/idris-free
haskell and scala example:
bind to c struct ! : https://github.com/idris-lang/Idris-dev/tree/master/libs/contrib/CFFI
idris elab refl:
tf c api usage:
TensorFlow has many ops, and the list is not static, so we recommend generating the functions for adding ops to a graph instead of writing them by individually by hand (though writing a few by hand is a good way to figure out what the generator should generate)
An Operation is a node in a TensorFlow Graph that takes zero or more Tensor objects as input, and produces zero or more Tensor objects as output. Objects of type Operation are created by calling a Python op constructor (such as tf.matmul) or tf.Graph.create_op.
1.get idris tf ffi to work (ok)
2.implement tf ops api with free monad
3.write your own computational graph
4.train and predict
Looking forward for your to join!
more about idris ffi
tf c api usage
a free/freer/algebraic effects computation graph api