Forall statements right now are parsed, then ignored. Forall statements should validate that they resolve to [True]

Solution: The result of the body of a forall statement should resolve to a term with the Constant value True.

Problem:
It would be nice to say things like Natural => Integer and autoderive a proof in strict mode.

Solution:
Apparently this is decidable for DFAs.

Kind Projection does not work in Unify V2.

[1] + Integer :: Term => Integer
[1] + Integer :: Constant => [1]

Expected Behavior
Projected types should be narrowed by their Kind.

problem: by default arbitrary algebra is permitted.

[if a%2==0 then 1 else 2]\[a%2|1] : [if 1==0 then 1 else 2] : [2]

solution: only permit algebra that is attached as an invariant of some property

(x:Odd) \ [self%2|1]

Types that associate with a Constant value must be annotated with constant in their declaration.

Type declarations should permit a constant marker similar to how normal is now.

type constant Boolean = True | False

Problem:
Documentation runs HVM code in browser, but not LSTS.

Solution:
Make an endpoint for LSTS code to run from.

Problem
Division is fallible if the denominator is 0. It would be nice to know if the operation can fail and prove if it will or won't fail. Right now the best action is to just crash or throw out an Exception. For strict mode "crashes" are definitely not valid.

Describe the solution you'd like
Mark a function as fallible with a description of the conditions under which it will fail.

let $"/"(n: Number, d: Number): Number
     where fails if d == 0;

1 + 2 * 3 : [7]

Recursive application of functions with dependent variables may clobber variable names before they should unify under proper order. This only affects recursive application of the same function candidates, i.e. "-(-(1))" so is only medium priority.

To reproduce the bug, uncomment the related code in tests/open_issues.rs and run "cargo test".

Problem:
1 + 1 == 2 should be easy to prove.

Solution:
Introduce a default proof tactic that connects to a Call-by-Value backend.

Describe alternatives you've considered
HVM et al. are alternatives, but codegen to a third-party for the default evaluation tactic is less than ideal.

Problem
Strict Mode is a setback for proof tactics.

Solution
Reintroduce some existing tactics to work in Strict Mode.

import "algebra.tlc";
1 + 1 == 2 : [True]

problem: type parameters aren't allowed on constructors

solution: add syntax for parameterization of constructors

Ok<Odd,String> { ok: 1 }

Problem:
There may be several function candidates available for @reduce to consider. Only function candidates can be overloaded, so other variables never have this problem.

Solution:
Apply the most general function candidate in @reduce. i.e. use Integer -> Integer instead of Even -> Even. If one does not imply the other then fail.

Describe alternatives you've considered:
Developers could manually add precedence labels, but that feels dumb.

Problem: Types can be created that are not in CNF.

Solution: Create a type definition for Types that disallows non-CNF types.

Alternative: Would dependent typing make this easier or harder to describe?

Should type constructors be allowed to be shared across type unions? Is that necessary or appropriate?

Problem:

let range(end: Integer): Tensor<Integer>;
let range(start: Integer, end: Integer): Tensor<Integer>;
let range(start: Integer, end: Integer, step: Integer): Tensor<Integer>;

Solution
This might already be working, this ticket is just to add test cases for the feature.

Some of the test cases for dependent types don't work in Unify V2. Specifically constant lifting and variable unification is not working.

1 + 1 : [2]

Expected behavior
Test cases should pass, with whatever strategy is chosen for dealing with dependent type variable unification.

Problem: foralls are only allowed at the global level.

Solution: Add foralls to the Term language.

let f(xs: Integer[]) = {
   forall x: xs. x : Odd
}

Describe the bug
Type invariants have probably been spuriously passing. Now strict mode has caught them and they need to actually do the footwork now.

To Reproduce
Unquote tests/prime.rs

Expected behavior
Green tests with unquoted invariants.

Problem:
Axiomatic Strict Mode has nothing to build on.

Solution:
Use simple algebraic axioms to start a prelude for Strict Mode

axiom @reflexive a. [True] = a == a

Problem:
Currently all statements are axiomatic due to lack of Strict Mode feature. In Strict Mode all statements would need to reduce to Axioms. Axioms are just statements that are not verified to be True.

Solution:
Introduce a new keyword: axiom. An axiom is just a forall statement that doesn't get verified in Strict Mode.

axiom @reflexive a:A. [True] = a == a;
axiom @symmetric a:A, b:A. [True] = a == b => b == a;
axiom @transitive a:A, b:A, c:A. [True] = a == b && b == c => a == c;

Problem:
It is not possible yet to pattern match against substrings of literal values.

Solution
Use string destructuring syntax to evaluate and process literals. The special "literal" keyword should be added to the match syntax and also to literal value creation.

match (x, y) {
   (literal '0', _) => literal '0',
   (_, _) => literal (x y) //x and y are concatenated
}

Problem:
Soundness here is defined as "only True statements can be proven", which is what most would expect from a theorem prover.

Solution:
Define a reduction step to a more widely accepted logical framework. CoC has everything according to the Lambda Cube, so at least try to reduce to that.

https://en.wikipedia.org/wiki/Lambda_cube

Problem:
Term::Arrow doesn't even try to typeck.

Solution
Implement typeck for Term::Arrow.

Context

exists x:Aa. x>2;           //sugared
$"exists"(fn(x: Aa) = x>2); //desugared

If a return type is provided on the Arrow, then send it in the implied field, otherwise implied is None and return type should be inferred.

problem: Iterator sugar is not implemented.

solution: implement iterator syntax in parser.

for i:Integer in ls yield i+1;
{for a:Integer in s yield a*a};
[for a:Integer in s yield a*a];
{for a:Integer in s yield a=a*a}

Problem
The TLC object is needed to discern if a type has a constant value. This increases cross-dependencies and prevents meaningful unification of Constants.

Describe the solution you'd like
Make Type Constants into Either<Term,Constant> instead of just Term.

Additional context
This could potentially greatly reduce the TLC object's God Object status in current design.

Problem:
Prove that Even + Odd : Odd in strict mode.

Solution
It is not clear whether anything needs to be done here beyond the currently approved feature set.

let $"+"(x: Even, y: Odd): Odd = ...proof

may be sufficient.

Problem:
Specialization happens when a language chooses a more specific function candidate over more general one. In LSTS all function candidates that fit are applied. If this results in multiple differently-valued functions being applied, then an Error should be generated.

Solution
For now, multiple valued function application should be forbidden. Later maybe it would be possible to show that two functions are equivalent under evaluation.

let incr(x: Integer): Integer = x + 1;
let incr(x: Even): Odd = x + 1;

incr(2) : Odd; //this is OK

Problem:

Succ (Succ (Succ 0))

is less than ideal for many situations and goes against the literal definition of Integer so far.

Solution
Break open the constant literals to prove structural properties of constants.

11 * 3 == 33

Other Thoughts
This could take weight off the dependent type system and free up some space for novel proof strategies.

Problem:
Preludes and programs should define their own literals and operations on them.

Solution:
Create destructuring primitives for literals with a match expression or similar.

Alternatives:
It would be possible to expose more information about constant evaluation. However, this strategy would be limited to a hard-coded set of features. After exposing literal operations and properties, new properties would have to be hard-coded again leading to an endless number of feature requests.

Problem: It is untenable to expect lhs AND rhs auto matching of forall type inference.

i.e. quickly prove that incrementing an Even number results in an Odd number.

((x: Even) + 1) : Odd

Solution: add optional name labels to forall rules that reduce the search time-space to O(1).

forall @inc_odd x: Odd. Even = x + 1
forall @dec_odd x: Odd. Even = x - 1
forall @inc_even x: Even. Odd = x + 1
forall @dec_even x: Even. Odd = x - 1

((x: Even) + 1) @inc_even

problem: there are entirely way too many clones in the type checker

solution: Non Lexical Lifetimes should enable smarter lifetimes.

Problem:
Division is fallible if divisor is zero. Division is complete if divisor is not zero.

let $"/"(x: Integer, d: Integer): Integer
     where fails if d == 0 = ...;

Solution
Create a branch arm in literal destructuring that "fails" to prove completeness.

match d {
   0 => fails
}

Alternatives
Syntax is arbitrary. Presence of branch arm is just a hint to the compiler. This could be inferred sometimes.

Describe the bug
Tensor constants don't unify and fail if opened in test cases.

To Reproduce
Unquote tests/tensor.rs

Expected behavior
The tests should pass

problem: LSTS has no backends

solution: HVM is a great match to start with as a backend

Problem
Add block expressions from the documentation.

Describe the solution you'd like
while, for, loop while, if let, match

Additional context
if let and match need a new term type, but others can just desugar.

Advanced data types like Map are not implemented in the parser.

Solution: Lex, Parse, and Desugar values.

True: Boolean;
1: Integer;
1.2: Real;
1.2+3i: Complex;
'a': Character;
"bc": String;
(1,True): (Odd, Boolean);
[7, 11]: Prime[];
{2, 6, 10}: Set<Even>;
{1=2, 3=4, 5=6, 7=8}: Map<Integer,Integer>;

Describe the bug
1 creates a span of src 1,1-1,1. It should be src 1,1-1,2.

To Reproduce
Parse anything and look at span.

Expected behavior
Spans should represent the beginning to end of an expression. Currently they are roughly near the beginning.

Additional context
There should be a test case covering each parse rule as well as separately testing the lexer spans.

Problem:
Some programs may need to prove that one operation will occur before another. Types are responsible for describing Terms, but currently the Type system isn't powerful enough to handle stuff like Linear Types.

Solution:
Implement Linear Types and demonstrate that they are sufficient to describe evaluation order.

Problem
The RHS of implication shouldn't narrow. For Type Parameters there is an implied step where they are substituted after implication unification.

Solution
Separate unification and substitution into two steps. I can't think of a test case where this would make a difference, but it helps build a more strict interpretation of the vocabulary used to explain the project.

(x: A -> A)(y: Integer) : Integer

but not

(Integer -> Integer) => (A -> A) = (Integer -> Integer)

because the RHS of implication doesn't narrow.

Problem
-1 lexes - first

Solution
Make lexer take longest-first-match so that Values can take any syntax.

-1 should yield -1 if Integer accepts it.

Problem:
The theoretical basis for LSTS is lacking as of 0.6.*. This isn't good enough for a 1.0.0. It is nice to prove simple things simply, but it should also be possible to prove hard things with enough work. For example here is an Agda program proving equivalence of all statements before and after skolemization:

open import Data.Product
open import Function
open import Relation.Binary.PropositionalEquality

iso : Set → Set → Set
iso A B =
  ∃₂ λ (f : A → B)(g : B → A) → (∀ x → f (g x) ≡ x) × (∀ x → g (f x) ≡ x)

ac : ∀ {A : Set}{B : A → Set}{C : ∀ a → B a → Set}
     → iso ((a : A) → Σ (B a) λ b → C a b)
           (Σ ((a : A) → B a) λ b → (a : A) → C a (b a))
ac = (λ f → proj₁ ∘ f , proj₂ ∘ f)
   , (λ {(b , c) a → b a , c a})
   , (λ _ → refl)
   , (λ _ → refl)

Solution
With an appropriate prelude is should be possible to prove the same result in strict mode in LSTS. This is just kicking tires before 1.0 release.

Problem:
Types are marked with constant if they can appear as values in types.

Solution:
Use all valued types as constants and remove the flag.

Problem:
A partial function could be defined to look like a complete one. This breaks the promises of strict mode.

Solution:
Require "completeness" of literal destructuring patterns according to type definition.

Problem:
Constant::eval is either unsound or nearly useless in strict mode.

Solution:
Make preludes define their own operations on constants, always. Then just remove the whole Constant::eval concept.

problem: pattern matching is not implemented

solution: implement match and if let statements

if let Some(a) = b {
   a: Odd
};

match x {
   EnumBranch1(y) => { y: Prime; },
   EnumBranch2(z,w) => { z: Odd; w: Even; },
}

problem: marking a Term as normal is allowed

solution: issue an error when a Term is marked as normal

type normal constant Boolean = True | False

should result in an error.

Problem:
It is not always clear what expression takes precedence in the parser. Also, there are some ugly expressions as well as plain dead code.

Solution:
Update parser to follow the "rule of least surprise". Coming from other languages, what is the most expected result of any given expression. Specifically please remove the one-semicolon per statement requirement.

Problem:
It may be helpful to pun statements onto the same hint label to allow "overloading" hints.

Solution
Try to apply all statements that have a given label. If any succeed then Accept. If all fail then Reject.

forall @hintpun a:Aa. Aa = a;
forall @hintpun b:Bb. Bb = b;

Problem:
CLI still has no backend.

Solution:
Expose the evaluation strategy that is default in the type-checker.

problem: LSTS has no proof backends

solution: HVM is a great match to start with as a validator