Datra is a language for data transformations. The preprint, primer, and Lean formalization live in this repository. Details on the WIP Haskell implementation can be found here.
Excuse the AI slop, it is temporary until the surface language has a chance to stablize, which will allow me to write its documentation in my own words.
let factorial := {n? : Int} -> Int do
yield if n = 0 then 1 else n * factorial (n - 1)
assert factorial 5 = 120
Variadic arguments need no special handling in Datra. Args is a first-class
type defined entirely in the standard library:
Args := &T? do
slots := (^_i :: Nat) do yield "arg%(_i)"? : T
yield ((^n? :: Nat) do yield slots[0..n])
For example, this is a Datra program that utilizes Args directly:
ArgsIntMap := {Args Int,}
ListInt := List Int
display := ArgsIntMap -> "%ListInt" do
toList := ArgsIntMap -> {ListInt,} do yield it
yield "%(toList it)"
assert display() = "()"
assert display(1) = "1"
assert display(1, 2, 3) = "(1; 2; 3)"
assert display(arg1 := 10, 4) = "(4; 10)"
assert ((arg2 := 10, 4) of ArgsIntMap) = false # missing argument: `arg1`
See the Haskell implementation README for Docker installation and invocation.
Licensed under the Apache License 2.0. Datra is authored by qualiascript; distributions and derivative works must preserve the attribution in NOTICE.