Counting 3,834 Big Data & Machine Learning Frameworks, Toolsets, and Examples...
Suggestion? Feedback? Tweet @stkim1

Last Commit
May. 23, 2019
Jul. 5, 2018

Join the chat at

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

syntax,api :

depGraph2 : FreeGraphD $ (TensorD [1],TensorD [2])
depGraph2 = do
  in1<-liftF $ PlaceholderD [1]
  out1<-liftF $ PlaceholderD [2]
  out2<-PlaceholderD [2] -- using implicits
  pure (in1,out1)

compGraphD : FreeGraphD $ TensorD [1]
compGraphD = do
  pure in1


1.verify tf c lib is installed

ls /usr/lib | grep tensor

should give sth like:

2.install idris-free package with freer (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

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 operations or 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.

project files:

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:

haskell and scala example:

idris ffi:

bind to c struct ! :

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.

Road map

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

tf architecture

elaborator reflection

any ideas!