4 ms·

Shame that reporting for "normal" earthlings is unlikely to include a few sample lines of code of this new language. Draft paper: https://arxiv.org/pdf/2008.11

by jll29 5y ago

Shame that reporting for "normal" earthlings is unlikely to include a few sample lines of code of this new language. Draft paper: https://arxiv.org/pdf/2008.11256.pdf https://arxiv.org/pdf/2008.11256.pdf Sample code (looks like a DSL embedded in Python): https://github.com/gilbo/atl/blob/master/examples/catenary.py https://github.com/gilbo/atl/blob/master/examples/catenary.p...

ogogmad 5y ago
One of the innovations in the paper is they find a method for implementing reverse-mode autodiff in a stateless manner, making optimisations easier to verify. I might be wrong but they take the principle of dual numbers: a + b epsilon, and change the b component into its linear dual. Therefore, b is a function, and not a number. If b is a function instead of a number, then there's more flexibility regarding flow of control, and that flexibility allows you to express reverse-mode autodiff.
- brrrrrm 5y ago
  a pure functional language is trivially differentiated, no? View a program as a data flow graph and then append the differentiation data flow graph. How this is executed (reverse-mode vs forward-mode vs some exotic mix) is just a leaked abstraction. Ideally, it wouldn't need to be exposed to the user.
  - taeric 5y ago
    My understanding is that all trivial versions of anything are wonderful for the pedagogy, but far short of what is needed in implementation. Just consider garbage collection. Trivial reference counting is easy to explain and implement. Not going to win too many points in use, though.
balsam 5y ago
Its unfortunate that ATL is such a generic name. The actual code to which you meant to link is here: https://github.com/ChezJrk/verified-scheduling https://github.com/ChezJrk/verified-scheduling OTOH, a Coq-like DSL written in python would be exciting!
- 7thaccount 5y ago
  I think it's a reference to APL which is an old, but extremely cool and relevant language and stands for "A Programming Language". APL was all about matrices and vectors too.
  - ScottBurson 5y ago
    Yes, clearly an homage to APL.
- hedgewitch 5y ago
  Ironically, some (all?) of the same developers appear to be creating a Python DSL based on the work done on the Coq DSL. https://github.com/ChezJrk/SYS_ATL https://github.com/ChezJrk/SYS_ATL
  - balsam 5y ago
    Ah it seems that the repos mentioned in this threads are all related after all— The coq repo is covered by the paper but is a verified version of only the scheduler (a part of the parent python repo, i presume) Then the repo you linked to seems to be a rewrite/generalization of another(?) lower level part of the main ATL.

by jll29 5y ago

ogogmad 5y ago

One of the innovations in the paper is they find a method for implementing reverse-mode autodiff in a stateless manner, making optimisations easier to verify. I might be wrong but they take the principle of dual numbers: a + b epsilon, and change the b component into its linear dual. Therefore, b is a function, and not a number. If b is a function instead of a number, then there's more flexibility regarding flow of control, and that flexibility allows you to express reverse-mode autodiff.

brrrrrm 5y ago
a pure functional language is trivially differentiated, no? View a program as a data flow graph and then append the differentiation data flow graph. How this is executed (reverse-mode vs forward-mode vs some exotic mix) is just a leaked abstraction. Ideally, it wouldn't need to be exposed to the user.
- taeric 5y ago
  My understanding is that all trivial versions of anything are wonderful for the pedagogy, but far short of what is needed in implementation. Just consider garbage collection. Trivial reference counting is easy to explain and implement. Not going to win too many points in use, though.

balsam 5y ago

Its unfortunate that ATL is such a generic name. The actual code to which you meant to link is here: https://github.com/ChezJrk/verified-scheduling https://github.com/ChezJrk/verified-scheduling OTOH, a Coq-like DSL written in python would be exciting!

7thaccount 5y ago
I think it's a reference to APL which is an old, but extremely cool and relevant language and stands for "A Programming Language". APL was all about matrices and vectors too.
- ScottBurson 5y ago
  Yes, clearly an homage to APL.
hedgewitch 5y ago
Ironically, some (all?) of the same developers appear to be creating a Python DSL based on the work done on the Coq DSL. https://github.com/ChezJrk/SYS_ATL https://github.com/ChezJrk/SYS_ATL
- balsam 5y ago
  Ah it seems that the repos mentioned in this threads are all related after all— The coq repo is covered by the paper but is a verified version of only the scheduler (a part of the parent python repo, i presume) Then the repo you linked to seems to be a rewrite/generalization of another(?) lower level part of the main ATL.