Recursive-function-definition syntax error leads to unhelpful compiler behavior

[Erhannis]

I think maybe the documentation (and possibly the implementation) changed regarding recursive functions - I had some test functions defined so:

!mul2*N : !{case n : Nat} -> Nat
| succ => succ(succ(mul2(n)))
| zero => zero
* zero

This worked a week or two ago, but I believe that the initial ! should now be a #. This is fine. However, the compiler does not tell me that's the problem. What it tells me is that that function and all functions after are undefined:

> fm hello/natmain
Definition not found: hello/natmain

The compiler should probably, instead, tell me that the definition of mul2 is incorrect.

[Erhannis]

Something else weird; maybe indicative of a broader problem: consider the following test code:

import Base@0 open

lambdatest
  let add = {x : Word, y : Word} : Word
    x + y
  let addOne = add(1)
  let map = {f : {x : Word} -> Word, l : [Word, Word]} : [Word, Word]
    [f(fst(l)), f(snd(l))]
  map(addOne, [3,4])

main
  True

and the following shell stuff:

C:\Users\mewer\Documents\formality\hello>fm test/lambdatest
0

C:\Users\mewer\Documents\formality\hello>fm test/main
Definition not found: test/main

...Actually, it only now occurs to me that the output of lambdatest wrong. Of the wrong type, even, despite that

C:\Users\mewer\Documents\formality\hello>fm -t test/lambdatest
Word

completes, incorrectly typing the expected output as Word. Actually, looking again, l is used twice in map, and that should cause a type error, yeah?

I dunno, something weird is going on. I did npm install -g formality-lang to update my runtime, and deleted fm_modules to keep versions together (it should probably warn you on run if they aren't - I was getting syntax errors from the definition of Bool), so those ought to be synced, now. Any ideas?

[LoPoHa]

import Base@0 open

lambdatest
  let add = {x : Word, y : Word} : Word
    x + y
  let addOne = add(1)
  let map = {f : {x : Word} -> Word, l : [Word, Word]} : [Word, Word]
    [f(fst(l)), f(snd(l))]
  map(addOne, [3,4])

main
  True

If i insert this into the provit.fm, i get the following output:

import Base@0 open

lambdatest
  let add = {x : Word, y : Word} 

Saying lambdatest is a Word.

(See provit.fm)

Also you are using f and l in the map function twice. If you make a top level function out of it, you get an error there because of the linearity:

map : {f : Word -> Word} -> {l : [:Word, Word]} -> [:Word, Word]
  [f(fst(l)), f(snd(l))]

[Erhannis]

I'm not sure what you're saying. Do you mean that you think lambdatest ACTUALLY DOES evaluate to a Word? If so, what am I misunderstanding about Formality syntax? The definition I gave above for lambdatest looks to me like it does the following, in order:

1. Defines a lambda add which takes two Words and outputs a Word: the sum of the two inputs.
2. Defines a second lambda addOne which I think curries 1 onto add, or however you say that, resulting in a function that accepts one Word and outputs the Word that is 1 greater.
3. Defines a third lambda map, which takes a function from Word to Word, and a pair of Words, and outputs a pair of Words (by applying the first argument to both elements of the second argument).
4. It then calls map with addOne and [3,4] as arguments, which should (if you're ignoring the copying problem) return [4,5]. (It HAS done so, in previous builds, and I think the type-checker returned a type error. I can't remember, though.)

If the code is syntactically correct, the type of lambdatest should be [Word, Word]. (Or maybe [:Word, Word]?) If the code is NOT syntactically correct, the type-checker should reject it. There are therefore no circumstances I see under which lambdatest is of type Word. Noting that I am using f and l twice each in map (which I did not at the time understand to be disallowed), I believe the code to be incorrect, and the type-checker should yield an error rather than return a type. As the type-checker returns Word, a result previously shown to be impossible, it follows that the type-checker (or something related) has a bug.

Am I missing something?

[LoPoHa]

imo it should throw an error. and i don't know why it would evaluate to a word. but looking at the provit output, it seems like it somehow stops compiling after the add function. this would explain why there is no main function in the output. does the typechecker throws an error if you explicitly specify the type of lambdatest?

i didn't had the time to look at the code to search for the problem and I'm not part of the moonad team. so maybe it would be best to wait for @MaiaVictor or another team member.

[Erhannis]

Oh, I see; you were just adding information, rather than providing an explanation. Ok, sorry/thanks. ... It looks like there's something weird about how I'm defining the lambdas; in particular, the return type of the lambda. If I remove it, so

let add = {x : Word, y : Word}
    x + y

instead of

let add = {x : Word, y : Word} **: Word**
    x + y

(and do similarly with the other lambdas) then it behaves as expected. I'm looking over the docs again, and I thought there had been something showing the let lamda = DEFINITION somewhere, but I'm not seeing it. I do, however, see:

An inline function (lambda expression):

main : Word
  ({x : Word, y : Word} x + y)(40, 2)

and also

You can annotate the full type rather than the type of each variable:

main : Word
  (({x, y} x + y) :: Word -> Word -> Word)(40, 2)

but maybe there's something particular about the way I've combined the two? Experimentation is required. (Regardless, it seems clear the type-checker should be yielding an error on the original lambdatest.) Oh, also, it's not clear to me how :: differs from : differs from ->.

[Erhannis]

I dunno, as I mess with stuff, it just seems like the compiler errors have suddenly and drastically decreased in helpfulness, in the past week. No stack traces anymore, for instance. Edit: or, they seem less frequent, rather.

[VictorTaelin]

The type-checker will not be very good giving error messages about things it do not understand right now, but we can surely improve it. Let me see your examples one by one.

!mul2*N : !{case n : Nat} -> Nat
| succ => succ(succ(mul2(n)))
| zero => zero
* zero

Here, we should have # instead of !, and halt: instead of *, because the old syntax changed. The compiler says:

Definition not found: _8/mul2

Very unhelpful. What happens here is that the compiler parses an "empty definition" and stops parsing before it even reaches mul2. I'll now raise an error when that happens. This program now generates the following message:

[PARSE-ERROR]
Expected a definition.

I noticed the problem on line 3, col 0:
   1| import Base
   2|
   3| !mul2*N : !{case n : Nat} -> Nat
   4| | succ => succ(succ(mul2(n)))
   5| | zero => zero
   6| * zero
   7|
   8| main mul2
   9|
But it could have happened a little earlier.

Much better.

Now this:

lambdatest
  let add = {x : Word, y : Word} : Word
    x + y
  let addOne = add(1)
  let map = {f : {x : Word} -> Word, l : [Word, Word]} : [Word, Word]
    [f(fst(l)), f(snd(l))]
  map(addOne, [3,4])

Here, what happens is that lambdas aren't annotated that way, so, the parser stops at the : Word part of the first line. The problem, though, is that instead of raising an error, it was parsing an empty string, which ended up being interpreted as the number 0. That's why you got Word types many times. Awful! Now the compiler won't parse empty strings as numbers anymore, showing the following error:

[PARSE-ERROR]
Unexpected symbol.

I noticed the problem on line 4, col 33:
   1| import Base
   2|
   3| lambdatest
   4|   let add = {x : Word, y : Word} : Word
   5|     x + y
   6|   let addOne = add(1)
   7|   let map = {f : {x : Word} -> Word, l : [Word, Word]} : [Word, Word]
   8|     [f(fst(l)), f(snd(l))]
   9|   map(addOne, [3,4])
  10|
But it could have happened a little earlier.

---

Now, to fix your actual program, we could do this:

lambdatest

  let add = {x : Word, y : Word}
    (x + y) :: Word

  let add_one = add(1)

  let map = {f : !{x : Word} -> Word, l : ![:Word, Word]}
    dup f = f
    dup l = l
    # [f(fst(l)), f(snd(l))] :: [:Word, Word]

  map(#add_one, #[3,4])

Some notes though:

1. Annotated anonymous lambdas ({x : Word, y : Word} x + y) don't require you to annotate the return type. If you want to, though, you must use :: on the body.

2. You can't use f twice on map without boxing it (except if you disable the stratification check, but then you don't get termination/consistency).

3. You can avoid copying a pair by using get [a, b] = pair instead of fst(pair) and snd(pair) separately.

This is how you'd do it the most idiomatic way, exploiting boxed definitions, etc.:

add : {x : Word, y : Word} -> Word
  x + y

#map : {f : !{x : Word} -> Word} -> !{pair : [:Word, Word]} -> [:Word, Word]
  get [a, b] = pair
  [f(a), f(b)]

#main : ![:Word, Word]
  let add_one = add(1)
  <map(#add_one)>([3,4])

Thank you so much for sharing your frustrating experience, keep those posts coming, that's very important to help me improve our tools.

[Erhannis]

Thanks! As I updated the code, the errors pointed to (near) the next erroneous thing, as desired.

(I find it a little weird that you can't include the return type of a lambda with the other part of its type. I'd have expected to write their types the same as for an ordinary function. Was there a particular reason for the difference?)

The code you provide runs and type-checks. One thing I'm unclear on - why can you use f twice in map?

[johnchandlerburnham]

@Erhannis

• This is a lambda: {x : Word} x, which is a term
• This is a forall: {x : Word} -> Word, which is a type

These are all the same:

word_id : Word -> Word
 {x} x

word_id : Word -> Word
  {x : Word} x :: Word

word_id : {x : Word} -> Word
  x

It's a little like -XScopedTypeVariables in Haskell:

Prelude> :set -XScopedTypeVariables 
Prelude> (\(x :: Int) -> 3 :: Int) 4
3

or

{-# LANGUAGE ScopedTypeVariables #-}

int_id (x :: Int) =
  3 :: Int

[Erhannis]

I kiiiindof get it, I think, except it seems like it boils down to "that's how we define lambdas", which isn't really a reason. It's just, the first half of the lambda sure LOOKS to me like a type, but an incomplete one. It defines the inputs of the lambda, but apparently can't define the outputs as well? That seems strange. It's not fundamentally problematic; it just seems to me more intuitive to allow lambdas to be typed in the same way that you type normal functions. Is there a reason their syntax is made different?

(Also, still, how come you can use f twice in map?)

[VictorTaelin]

@Erhannis it is the reason though. The syntax for anonymous lambdas is just {a : A, b : B, ...} return_body, which includes annotations only for argument types. That's because this is always enough, so there is no reason to force the user to annotate the return type. Top-level definitions are different, you must annotate the full type of them, which, in the case of functions, is a forall {a : A, b : B, ...} -> ReturnType. This is not a difference between lambdas and functions, it is a difference between expressions and top-level definitions. But I can see your point and will keep that in mind.

You can use f twice in map because it is boxed! Notice its type:

#map*n : {~A : Type, ~B : Type, f : !A -> B} -> ! {case list : List(A)} -> List(B)

Here, f comes before the function's !, which means it is a boxed level-0 argument instead of an unboxed level-1 argument. That means that it can be used as many times as you want inside the body of map, but, in exchange, it can't vary dynamically (i.e., f can't read information from terms on level-1, so it is essentially "static").

[Erhannis]

Hmm. Ok, thanks.