Possible error in JS typechecker

[johnchandlerburnham]

If we take the Bool type and switch the argument order in the self-type:

Boole : Type
  boole_value<P: Boole -> Type> ->
  P(ff) -> 
  P(tt) -> 
  P(boole_value)

ff: Boole
  <P> (t) (f) f

tt: Boole
  <P> (t) (f) t

FormalityCore.js (from c65b846) errors with

Type-checking endo2.fmc:
Boole : Type
ff    : error
tt    : error

Found 2 type error(s):

Inside ff:
Found type... P(tt)
Instead of... P((t) => (f) => f)
With context:
- P : Boole -> Type
- t : P(ff)
- f : P(tt)
On line 4:
     5|   P(boole_value)
     6| 
     7| ff: Boole
     8|   <P> (t) (f) f
     9| 
    10| tt: Boole
    11|   <P> (t) (f) t
    12| 

Inside tt:
Found type... P(ff)
Instead of... P((t) => (f) => t)
With context:
- P : Boole -> Type
- t : P(ff)
- f : P(tt)
On line 7:
     8|   <P> (t) (f) f
     9| 
    10| tt: Boole
    11|   <P> (t) (f) t
    12| 

Seems like an issue with the JS typechecker, my FormalityCore.hs on c1add22 passes this fine (but the .hs could very well have bugs too)

@gabriel-barrett suggested that this could be related to an issue where

apply: <A: Type> -> <B: Type> -> A -> (A -> B) -> B
  <A> <B> (a) (f) f(a)

test: Nat -> (Nat -> Nat) -> Nat
  (n)(f)
  let Test = Nat
  apply<Nat><Test>(n)(f)

Nat: Type //prim//
  nat_value<P: Nat -> Type> ->
  (zero: P(zero)) ->
  (succ: (pred: Nat) -> P(succ(pred))) ->
  P(nat_value)

zero: Nat
  <> (z) (s) z

succ: Nat -> Nat
  (n)
  <> (z) (s) s(n)

errors with

apply: <A: Type> -> <B: Type> -> A -> (A -> B) -> B
  <A> <B> (a) (f) f(a)

test: Nat -> (Nat -> Nat) -> Nat
  (n)(f)
  let Test = Nat
  apply<Nat><Test>(n)(f)

Nat: Type //prim//
  nat_value<P: Nat -> Type> ->
  (zero: P(zero)) ->
  (succ: (pred: Nat) -> P(succ(pred))) ->
  P(nat_value)

zero: Nat
  <> (z) (s) z

succ: Nat -> Nat
  (n)
  <> (z) (s) s(n)

This also passes FormalityCore.hs without issue.

Furthermore, by generalizing Bool to 3 values instead of 2, I've found that the JS typechecker exhibits unusual behavior. For example

 Trit : Type
  trit_value<P: Trit -> Type> ->
  P(ttt) -> 
  P(fff) -> 
  P(unk) -> 
  P(trit_value)

ttt : Trit
  <P> (x0) (x1) (x2) x0

fff : Trit
  <P> (x0) (x1) (x2) x1

unk : Trit
  <P> (x0) (x1) (x2) x2

Works fine, but if we instead change the type to

Trit : Type
  trit_value<P: Trit -> Type> ->
  P(ttt) -> 
  P(unk) ->
  P(fff) ->  
  P(trit_value)

We error. However, doing

Trit : Type
  trit_value<P: Trit -> Type> ->
  P(ttt) -> 
  P(fff) -> 
  P(unk) -> 
  P(trit_value)

ttt : Trit
  <P> (x0) (x1) (x2) x0

fff : Trit
  <P> (x0) (x1) (x2) x0

unk : Trit
  <P> (x0) (x1) (x2) x2

works fine.

To further generalize, every mapping from a finite set to itself has a corresponding Self-Type encoding. For example, there are 4 functions from the 2 set to the 2 set:

0. {0,1} -> {0,0}
1. {0,1} -> {0,1} 
2. {0,1} -> {1,0}
3. {0,1} -> {1,1}

Bool encodes {0,1} -> {0,1} and Boole (defined above) encodes {0,1} -> {1,0}. A self-mapping in a finite set of n elements can be assigned a number by ordering the domain elements in ascending order and then interpreting their image as digits in base n. So we could call Bool function 2.1 (the function numbered 1 on a set of 2) and Boole, 2.2. The various Trit encodings would be 3.5, 3.7 and 3.2 respectively.

I have written a program to generate all possible self-type encodings of these finite self-mappings (or endomorphisms, if we want to be categorical): https://gist.github.com/johnchandlerburnham/fe53c5702bca6f0925f344905e82c0b0

Using this program, FormalityCore.hs passes typechecking for all encodings (up to n == 5), but JS does the following:

• 2.0, 2.1, 2.2 check, 2.3 fails
• 3.2, 3.3, 3.4.3.5,3.8,3.13,3.14, 3.23 check, the rest fail
• similar pattern for 4 and 5

It appears that functions that map to a single value all work, some of the ones that map to two values work, and all (or nearly all, there may be exceptions) that map to 3 or more fail.

To replicate these results, cal writeEndo 4 "endo4.fmc" or similar from the above file and then do

$ ./javascript/fmc.js endo3 | grep 'error' | less

to see the function numbers that error.

[johnchandlerburnham]

Update:

With various printfs enabled we can see the behavior of both FormalityCore.hs and FormalityCore.js on function 3.1:

N3.1 : Type
  N3.1_value<P: N3.1 -> Type> ->
  P(n3.1.v0) -> 
  P(n3.1.v1) -> 
  P(n3.1.v2) -> 
  P(N3.1_value)
n3.1.v0 : N3.1
  <P> (x0) (x1) (x2) x0
n3.1.v1 : N3.1
  <P> (x0) (x1) (x2) x0
n3.1.v2 : N3.1
  <P> (x0) (x1) (x2) x1

Or, more legibly:

Trit1 : Type
  Trit1_value<P: Trit1 -> Type> ->
  P(a) -> 
  P(b) -> 
  P(c) -> 
  P(Trit1_value)

a : Trit1
  <P> (x) (y) (z) x

b : Trit1
  <P> (x) (y) (z) x

c : Trit1
  <P> (x) (y) (z) y

When checking b JS logs:

b     : Trit1
check: <P> => (x) => (y) => (z) => y
typed: Trit1
ctx: []
======
check: (x) => (y) => (z) => y
typed: P(a) -> P(b) -> P(c) -> P(<P> => (x) => (y) => (z) => y)
ctx: [P : Trit1 -> Type]
======
check: (y) => (z) => y
typed: P(b) -> P(c) -> P((x) => (y) => (z) => y)
ctx: [P : Trit1 -> Type,x : P(a)]
======
check: (z) => y
typed: P(c) -> P((x) => (y) => (z) => y)
ctx: [P : Trit1 -> Type,x : P(a),y : P(b)]
======
check: y
typed: P((x) => (y) => (z) => y)
ctx: [P : Trit1 -> Type,x : P(a),y : P(b),z : P(c)]
======
infer: y
ctx: [P : Trit1 -> Type,x : P(a),y : P(b),z : P(c)]
solve: y :  P(b)
-----
infr: P(b)

Whereas the Haskell logs

CHECKING: b
check: <P> (x) (y) (z) x
typed: Trit1
ctx: []
=====
check: (x) (y) (z) x
typed: (P(a)) -> (P(b)) -> (P(c)) -> P(<P> (x) (y) (z) x)
ctx: [P : (Trit1) -> Type]
=====
check: (y) (z) x
typed: (P(b)) -> (P(c)) -> P((x) (y) (z) x)
ctx: [P : (Trit1) -> Type, x : P(a)]
=====
check: (z) x
typed: (P(c)) -> P((x) (y) (z) x)
ctx: [P : (Trit1) -> Type, x : P(a), y : P(b)]
=====
check: x
typed: P((x) (y) (z) x)
ctx: [P : (Trit1) -> Type, x : P(a), y : P(b), z : P(c)]
=====
infer x
ctx: [P : (Trit1) -> Type, x : P(a), y : P(b), z : P(c)]
solve x : P(a)
-----
infr: P(a)

[VictorTaelin]

Boole : Type
  boole_value<P: Boole -> Type> ->
  P(ff) -> 
  P(tt) -> 
  P(boole_value)

ff: Boole
  <P> (t) (f) f

tt: Boole
  <P> (t) (f) t

Should be a type error since ff should return P((t) (f) f) (because ff = (t) (f) f, so P(self) is P((t) (f) f)), but returns P((t) (f) t) instead (because f : P(tt), and tt = (t) (f) t). Similarly, all functions that return the wrong type should fail to type-check. The JavaScript implementation is presenting the proper behavior in this case, the Haskell implementation must have this fixed.

@gabriel-barrett suggested that this could be related to an issue where

This should be an error because let bound variables are not equaled to the values they bind by definition. If it checks on Haskell I suspect it is substituting the expression by the bound value and then type-checking, which is not the correct behavior.

Note that we could make let equal its bound variables, but we'd need opt for one of those drawbacks:

1. Complicate the type-checker and evaluator considerably by carrying a "value" context.

2. Substitute the body by the expression before type-checking, which would make us unable to share values with let on compiled back-ends (since it would vanish during type-oriented compilation).

Since, in a future, we'll have a separate let (var?) that will perform a parse-time substitution, and since even without that type aliases can be done as top-level definitions, I don't think that equaling let with its bound expression is worth the complications. This is also consistent with the behavior of lambdas. For example:

test: Nat -> (Nat -> Nat) -> Nat
  (n)(f)
  (((Test) apply<Nat><Test>(n)(f)) :: Type -> Nat)(Type)

Fails to type-check on Formality-Core, Agda and Coq.