values (instead of functions) inside rec

[xekoukou]

https://github.com/stedolan/malfunction/blob/c4d24c57f692c3646e908b9f77e9afd632b286c1/src/malfunction_parser.ml#L110

There exist recursive values in agda , functions that have zero arguments. For example , this code does not compile with malfunction. :

open import Common.IO
open import Common.Unit
open import Common.String
open import Common.Nat

record Stream (A : Set) : Set where
  coinductive
  field
    head : A
    tail : Stream A
open Stream public

repeat : Stream String
head repeat = "hello"
tail repeat = repeat

lookup : ∀ {A} → Stream A → Nat → A
lookup xs zero = xs .head
lookup xs (suc n) = lookup (xs .tail) n

main : IO Unit
main = putStr (lookup repeat 1000000)

I could introduce a dummy variable , but I was wondering if you could do something from your side.

[stedolan]

OCaml and malfunction are strict (eagerly evaluated), so non-functional recursive values don't really make much sense. (OCaml supports recursive values, but they're a bit useless: you can write a list which is its own tail, but you can't write an infinite increasing stream of numbers).

So, malfunction's never going to support arbitrary recursive binders. The best bet might be to compile Agda coinductive records as functions taking a field index as a parameter.

Alternatively, I think it would be possible to extend recursive binders to allow a mix of lazy values and functions. Even with this feature, you'd still need to compile some values differently: lazy values must be forced before they can be used.

[xekoukou]

Yes , I already have support for coinduction, (though it might be buggy).

This code which is almost identical to the above works, because repeat has two arguments instead of zero arguments.

Your last proposal will probably work , having recursive lazy values.

open import Common.IO
open import Common.Unit
open import Common.String
open import Common.Nat

record Stream (A : Set) : Set where
  coinductive
  field
    head : A
    tail : Stream A
open Stream public

repeat : ∀ {A} → A → Stream A
head (repeat x) = x
tail (repeat x) = repeat x

lookup : ∀ {A} → Stream A → Nat → A
lookup xs zero = xs .head
lookup xs (suc n) = lookup (xs .tail) n

main : IO Unit
main = putStr (lookup (repeat "hello") 1000000)

( module
  ( $agdaIdent14.952a3c475e16a2d6.Common.IO.putStr
    (global $ForeignCode $Common $IO $printString)
  )
  ( rec
    ( $agdaIdent12.f4381f0c0de3e784.Coinduction.repeat
      ( lambda ($v0 $v1)
        (lazy ( block (tag 0)
                $v1
                ( apply $agdaIdent12.f4381f0c0de3e784.Coinduction.repeat 0 $v1 )
              ))
      )
    )
  )
  ( $agdaIdente.f4381f0c0de3e784.Coinduction.Stream.tail
    ( lambda ($v0)
      ( let
        ( $letId0 (force $v0) )
        ( switch $letId0
          ( (tag 0) (field 1 $letId0) )
          ( _ (tag _)
            ( apply (global $Stdlib $failwith) "__UNREACHABLE__" )
          )
        )
      )
    )
  )
  ( $agdaIdentc.f4381f0c0de3e784.Coinduction.Stream.head
    ( lambda ($v0)
      ( let
        ( $letId0 (force $v0) )
        ( switch $letId0
          ( (tag 0) (field 0 $letId0) )
          ( _ (tag _)
            ( apply (global $Stdlib $failwith) "__UNREACHABLE__" )
          )
        )
      )
    )
  )
  ( rec
    ( $agdaIdent1a.f4381f0c0de3e784.Coinduction.lookup
      ( lambda ($v0 $v1 $v2)
        ( switch $v2
          ( _ (tag _)
            ( switch ( ==.ibig $v2 0.ibig )
              ( 1
                ( apply $agdaIdentc.f4381f0c0de3e784.Coinduction.Stream.head $v1 )
              )
              ( _ (tag _)
                ( apply $agdaIdent1a.f4381f0c0de3e784.Coinduction.lookup
                  0
                  ( apply $agdaIdente.f4381f0c0de3e784.Coinduction.Stream.tail $v1 )
                  ( -.ibig $v2 1.ibig )
                )
              )
            )
          )
        )
      )
    )
  )
  ( $main
    ( apply (global $ForeignCode $main_run)
      ( apply ( lambda ($world)
                ( apply ( apply $agdaIdent14.952a3c475e16a2d6.Common.IO.putStr
                          ( apply $agdaIdent1a.f4381f0c0de3e784.Coinduction.lookup
                            0
                            ( apply $agdaIdent12.f4381f0c0de3e784.Coinduction.repeat
                              0
                              "hello"
                            )
                            1000000.ibig
                          )
                        )
                  $world
                )
              )
        0
      )
    )
  )
  ( export )
)

[stedolan]

Support for recursive lazy values was easier than I thought it would be!

[xekoukou]

I tested it and it works. Thanks.