Rudimentary but working Agda -> Ruby compilation & use examples (see test file at bottom) http://github.com/larrytheliquid/agda-rb

Maths.agda

module Maths where

data Nat : Set where
  zero : Nat
  suc : Nat → Nat

plus : Nat → Nat → Nat
plus zero n = n
plus (suc m) n = suc (plus m n)

data NatList : Set where
  nil : NatList
  cons : Nat → NatList → NatList

nappend : NatList → NatList → NatList
nappend nil ys = ys
nappend (cons x xs) ys = cons x (nappend xs ys)

nfoldr : {B : Set} → (Nat → B → B) → B → NatList → B
nfoldr f z nil       = z
nfoldr f z (cons x xs) = f x (nfoldr f z xs)

nsum : NatList → Nat
nsum = nfoldr plus zero

data List (A : Set) : Set where
  nil : List A
  cons : A → List A → List A

lappend : ∀ {A} → List A → List A → List A
lappend nil ys = ys
lappend (cons x xs) ys = cons x (lappend xs ys)

lfoldr : {A B : Set} → (A → B → B) → B → List A → B
lfoldr f z nil = z
lfoldr f z (cons x xs) = f x (lfoldr f z xs)

lsum : List Nat → Nat
lsum = lfoldr plus zero

data Vec (A : Set) : Nat → Set where
  nil : Vec A zero
  cons : ∀ {n} → A → Vec A n → Vec A (suc n)

vappend : ∀ {A m n} → Vec A m → Vec A n → Vec A (plus m n)
vappend nil ys = ys
vappend (cons x xs) ys = cons x (vappend xs ys)

vfoldr : ∀ {A B : Set} {n} →
  (A → B → B) → B → Vec A n → B
vfoldr f z nil = z
vfoldr f z (cons x xs) = f x (vfoldr f z xs)

vsum : ∀ {n} → Vec Nat n → Nat
vsum = vfoldr plus zero

Maths.rb

module Ragda module Maths

def self.[](k) CONTEXT[k] end

CONTEXT = {
  "List" => {
    "cons" => lambda do |x0| 
      lambda do |x1| 
        lambda do |x2| 
          x2["cons"][x0, x1]
         end
       end
     end,
    "nil" => lambda do |x0| 
      x0["nil"][]
     end
  },
  "Nat" => {
    "suc" => lambda do |x0| 
      lambda do |x1| 
        x1["suc"][x0]
       end
     end,
    "zero" => lambda do |x0| 
      x0["zero"][]
     end
  },
  "NatList" => {
    "cons" => lambda do |x0| 
      lambda do |x1| 
        lambda do |x2| 
          x2["cons"][x0, x1]
         end
       end
     end,
    "nil" => lambda do |x0| 
      x0["nil"][]
     end
  },
  "Vec" => {
    "cons" => lambda do |x0| 
      lambda do |x1| 
        lambda do |x2| 
          lambda do |x3| 
            x3["cons"][x0, x1, x2]
           end
         end
       end
     end,
    "nil" => lambda do |x0| 
      x0["nil"][]
     end
  },
  "lappend" => lambda do |x0| 
    lambda do |x1| 
      x1[{
        "cons" => lambda do |x2, x3| 
          lambda do |x4| 
            CONTEXT["List"]["cons"][x2][CONTEXT["lappend"][x0][x3][x4]]
           end
         end,
        "nil" => lambda do || 
          lambda do |x2| 
            x2
           end
         end
      }]
     end
   end,
  "lfoldr" => lambda do |x0| 
    lambda do |x1| 
      lambda do |x2| 
        lambda do |x3| 
          lambda do |x4| 
            x4[{
              "cons" => lambda do |x5, x6| 
                x2[x5][CONTEXT["lfoldr"][x0][x1][x2][x3][x6]]
               end,
              "nil" => lambda do || 
                x3
               end
            }]
           end
         end
       end
     end
   end,
  "lsum" => lambda do |x0| 
    x0[{
      "cons" => lambda do |x1, x2| 
        CONTEXT["plus"][x1][CONTEXT["lfoldr"]["*"]["*"][CONTEXT["plus"]][CONTEXT["Nat"]["zero"]][x2]]
       end,
      "nil" => lambda do || 
        CONTEXT["Nat"]["zero"]
       end
    }]
   end,
  "nappend" => lambda do |x0| 
    x0[{
      "cons" => lambda do |x1, x2| 
        lambda do |x3| 
          CONTEXT["NatList"]["cons"][x1][CONTEXT["nappend"][x2][x3]]
         end
       end,
      "nil" => lambda do || 
        lambda do |x1| 
          x1
         end
       end
    }]
   end,
  "nfoldr" => lambda do |x0| 
    lambda do |x1| 
      lambda do |x2| 
        lambda do |x3| 
          x3[{
            "cons" => lambda do |x4, x5| 
              x1[x4][CONTEXT["nfoldr"][x0][x1][x2][x5]]
             end,
            "nil" => lambda do || 
              x2
             end
          }]
         end
       end
     end
   end,
  "nsum" => lambda do |x0| 
    x0[{
      "cons" => lambda do |x1, x2| 
        CONTEXT["plus"][x1][CONTEXT["nfoldr"]["*"][CONTEXT["plus"]][CONTEXT["Nat"]["zero"]][x2]]
       end,
      "nil" => lambda do || 
        CONTEXT["Nat"]["zero"]
       end
    }]
   end,
  "plus" => lambda do |x0| 
    x0[{
      "suc" => lambda do |x1| 
        lambda do |x2| 
          CONTEXT["Nat"]["suc"][CONTEXT["plus"][x1][x2]]
         end
       end,
      "zero" => lambda do || 
        lambda do |x1| 
          x1
         end
       end
    }]
   end,
  "vappend" => lambda do |x0| 
    lambda do |x1| 
      lambda do |x2| 
        lambda do |x3| 
          x3[{
            "cons" => lambda do |x4, x5, x6| 
              lambda do |x7| 
                CONTEXT["Vec"]["cons"][CONTEXT["plus"][x4][x2]][x5][CONTEXT["vappend"][x0][x4][x2][x6][x7]]
               end
             end,
            "nil" => lambda do || 
              lambda do |x4| 
                x4
               end
             end
          }]
         end
       end
     end
   end,
  "vfoldr" => lambda do |x0| 
    lambda do |x1| 
      lambda do |x2| 
        lambda do |x3| 
          lambda do |x4| 
            lambda do |x5| 
              x5[{
                "cons" => lambda do |x6, x7, x8| 
                  x3[x7][CONTEXT["vfoldr"][x0][x1][x6][x3][x4][x8]]
                 end,
                "nil" => lambda do || 
                  x4
                 end
              }]
             end
           end
         end
       end
     end
   end,
  "vsum" => lambda do |x0| 
    CONTEXT["vfoldr"]["*"]["*"][x0][CONTEXT["plus"]][CONTEXT["Nat"]["zero"]]
   end
}

end end 

maths_test.rb

require File.dirname(__FILE__) + "/Maths"
require 'test/unit'

class MathsTest < Test::Unit::TestCase
  Maths = Ragda::Maths

  NAT = {
    'zero' => lambda{ 0 },
    'suc'  => lambda{|n| n[NAT].succ }
  }

  def test_nat
    zero  = Maths['Nat']['zero']
    one   = Maths['Nat']['suc'][zero]
    two   = Maths['Nat']['suc'][one]
    three = Maths['Nat']['suc'][two]

    assert_equal 0, zero[NAT]
    assert_equal 1, one[NAT]
    assert_equal 2, two[NAT]
    assert_equal 3, three[NAT]

    assert_equal 0, Maths['plus'][zero][zero][NAT]
    assert_equal 2, Maths['plus'][zero][two][NAT]
    assert_equal 2, Maths['plus'][two][zero][NAT]
    assert_equal 3, Maths['plus'][two][one][NAT]
    assert_equal 3, Maths['plus'][one][two][NAT]
  end

  NAT_LIST = {
    'nil' => lambda{ [] },
    'cons'  => lambda{|x, xs| [x] + xs[NAT_LIST] }
  }

  def test_nat_list
    zero  = Maths['Nat']['zero']
    one   = Maths['Nat']['suc'][zero]
    two   = Maths['Nat']['suc'][one]
    three = Maths['Nat']['suc'][two]

    empty = Maths['NatList']['nil']
    a = Maths['NatList']['cons'][one][empty]
    b = Maths['NatList']['cons'][two][empty]
    c = Maths['NatList']['cons'][three][empty]
    bc = Maths['NatList']['cons'][two][c]
    abc = Maths['NatList']['cons'][one][bc]

    plus = Maths['plus']
    nfoldr = Maths['nfoldr']['*']

    assert_equal [], empty[NAT_LIST]
    assert_equal [one], a[NAT_LIST]
    assert_equal [two], b[NAT_LIST]
    assert_equal [three], c[NAT_LIST]
    assert_equal [two, three], bc[NAT_LIST]
    assert_equal [one, two, three], abc[NAT_LIST]

    assert_equal [], Maths['nappend'][empty][empty][NAT_LIST]
    assert_equal [two, three], Maths['nappend'][empty][bc][NAT_LIST]
    assert_equal [two, three], Maths['nappend'][bc][empty][NAT_LIST]
    assert_equal [two, three], Maths['nappend'][b][c][NAT_LIST]
    assert_equal [three, two], Maths['nappend'][c][b][NAT_LIST]
    assert_equal [one, two, three], Maths['nappend'][a][bc][NAT_LIST]
    assert_equal [two, three, one], Maths['nappend'][bc][a][NAT_LIST]

    assert_equal 0, Maths['nsum'][empty][NAT]
    assert_equal 0, nfoldr[plus][zero][empty][NAT]
    assert_equal 1, Maths['nsum'][a][NAT]
    assert_equal 1, nfoldr[plus][zero][a][NAT]
    assert_equal 6, Maths['nsum'][abc][NAT]
    assert_equal 6, nfoldr[plus][zero][abc][NAT]
  end

  LIST = NAT_LIST

  def test_list
    zero  = Maths['Nat']['zero']
    one   = Maths['Nat']['suc'][zero]
    two   = Maths['Nat']['suc'][one]
    three = Maths['Nat']['suc'][two]

    empty = Maths['List']['nil']
    a = Maths['List']['cons'][one][empty]
    b = Maths['List']['cons'][two][empty]
    c = Maths['List']['cons'][three][empty]
    bc = Maths['List']['cons'][two][c]
    abc = Maths['List']['cons'][one][bc]

    plus = Maths['plus']
    lfoldr = Maths['lfoldr']['*']['*']

    assert_equal [], empty[LIST]
    assert_equal [one], a[LIST]
    assert_equal [two], b[LIST]
    assert_equal [three], c[LIST]
    assert_equal [two, three], bc[LIST]
    assert_equal [one, two, three], abc[LIST]

    assert_equal [], Maths['lappend']['*'][empty][empty][LIST]
    assert_equal [two, three], Maths['lappend']['*'][empty][bc][LIST]
    assert_equal [two, three], Maths['lappend']['*'][bc][empty][LIST]
    assert_equal [two, three], Maths['lappend']['*'][b][c][LIST]
    assert_equal [three, two], Maths['lappend']['*'][c][b][LIST]
    assert_equal [one, two, three], Maths['lappend']['*'][a][bc][LIST]
    assert_equal [two, three, one], Maths['lappend']['*'][bc][a][LIST]

    assert_equal 0, Maths['lsum'][empty][NAT]
    assert_equal 0, lfoldr[plus][zero][empty][NAT]
    assert_equal 1, Maths['lsum'][a][NAT]
    assert_equal 1, lfoldr[plus][zero][a][NAT]
    assert_equal 6, Maths['lsum'][abc][NAT]
    assert_equal 6, lfoldr[plus][zero][abc][NAT]
  end

  VEC = {
    'nil' => lambda{ [] },
    'cons'  => lambda{|n, x, xs| [x] + xs[VEC] }
  }

  def test_vec
    zero  = Maths['Nat']['zero']
    one   = Maths['Nat']['suc'][zero]
    two   = Maths['Nat']['suc'][one]
    three = Maths['Nat']['suc'][two]

    n  = Maths['Nat']['zero']
    empty = Maths['Vec']['nil']
    a = Maths['Vec']['cons'][n][one][empty]
    b = Maths['Vec']['cons'][n][two][empty]
    c = Maths['Vec']['cons'][n][three][empty]
    bc = Maths['Vec']['cons'][n][two][c]
    abc = Maths['Vec']['cons'][n][one][bc]

    plus = Maths['plus']
    vfoldr = Maths['vfoldr']['*']['*'][zero]

    assert_equal [], empty[VEC]
    assert_equal [one], a[VEC]
    assert_equal [two], b[VEC]
    assert_equal [three], c[VEC]
    assert_equal [two, three], bc[VEC]
    assert_equal [one, two, three], abc[VEC]

    assert_equal [], Maths['vappend']['*'][n][n][empty][empty][VEC]
    assert_equal [two, three], Maths['vappend']['*'][n][n][empty][bc][VEC]
    assert_equal [two, three], Maths['vappend']['*'][n][n][bc][empty][VEC]
    assert_equal [two, three], Maths['vappend']['*'][n][n][b][c][VEC]
    assert_equal [three, two], Maths['vappend']['*'][n][n][c][b][VEC]
    assert_equal [one, two, three], Maths['vappend']['*'][n][n][a][bc][VEC]
    assert_equal [two, three, one], Maths['vappend']['*'][n][n][bc][a][VEC]

    assert_equal 0, Maths['vsum'][n][empty][NAT]
    assert_equal 0, vfoldr[plus][zero][empty][NAT]
    assert_equal 1, Maths['vsum'][n][a][NAT]
    assert_equal 1, vfoldr[plus][zero][a][NAT]
    assert_equal 6, Maths['vsum'][n][abc][NAT]
    assert_equal 6, vfoldr[plus][zero][abc][NAT]
  end
end