• Remove bsort from Eq
• msg in str_error should be of (string list)
• split case syntax into case, sumcase and unpack
• case and unpack should allow omitting return-clause and try to forget unescapable variables (like what let does)
• Distill the bind pattern
• Disallow impredicative universal types
• Type inference
• Idx inference
• (Kind-of) Allow datatype to have idx arguments that do not change.
• Multi-argument idx functions.
• Add an optional idx to Quan, to link the remaining unification variables in types and the witnesses found by the Master Theorem solver.
• Infer by Master Theorem then check.
• Single variable Master Theorem case.
• Error line number on multiple files.
• Make linking between inferred existential variable values and types better.
• Copy function signature annotation to case annotation
• (Abondoned. No problem.) Unit and product types are required to define datatypes. 17. Remove unit and product types from the language, and have standard library.
• Example: Tree flatten.
• Example: Insertion sort.
• Have reference and arrays.
• RB-tree insertion.
• RB-tree lookup.
• Braun tree insertion.
• A bug of position reporting when I change bigO spec of msort in msort.timl from $m * $n * log2 $n to $n * log2 $n.
• return _ using works but return using does not in msort.timl and tree.timl.
• Change syntax order of function name and t declares.
• Be able to infer for tree_map and tree_foldl.
• (Partially) Have module system. Road map to add module system:
  • Have a barebone module system with only modules, signatures, sealing, functors and open. No hierarchy (embeded modules), module alias, signature alias, where/sharing, include.
  • Combine name-resolve and typecheck.
  • Combine cctx and tctx into tctx.
  • (\Abondoned.) Combine idx and type into constructors, sort and kind into kind, Combine sctx and kctx into kctx.
  • Add record types.
  • Add singleton kinds, dependent record kinds, dependent arrow kinds.
  • Elaborate modules and signatures into core language.
• Bug of type inference in tree_append_rlm. The inferred type has {n} tree tree and {n} list list.
• Put Unit back to mtype from base_type because Unit is not a base type like Int but a structural building block.
• Have a good error message when insertion_sort.timl/insert does not have the needed return-annotation on case.
• Be able to infer for insertion_sort.
• (Solved by new unification framework) unify's (UVar, UVar) case could be dangerous: shift_invis may not be transactional, and there is no circularity check.
• Have a standard library.
• Automatically generate premises in (VarP, Never) case of match_ptrn, from complement cover of previous rules.
• case should also copy fun's return clause even without using.
• (Abondoned. No problem.) as pattern may have a problem in balance_left.
• Bug: redundancy checker runs forever on balance_left.
• rbt.timl typecheckes when using ForgetError-less subst and ForgetError-full forget. Investigate why.
• find_habitant can further simplify covers and speed up.
• Have type = type aliasing.
• Maximally insertion of index arguments.
• Maximally insertion of index arguments in patterns.
• nouvar-expr/passp/Imply/_ is not sound, possibly losing information.
• (Solved by new unification framework) subst_invis_no_throw should be implemented in a safe way where uvars that can see the target variable are unified with a new shifted uvars that cannot see it, and bring_forward_anchor needs to be more sophisticated to only put new anchor when there is no shift (and the notifier in Exists needs to do some shift) because now not every uvar has an anchor.
• Braun tree extraction.
• rename "peel_" to "collect_".
• Register admitted things.
• Make SMT batch response parsing smarter (do not check response length beforehand)
• Simplify MaxI using SMT solver.
• Have binary search with arrays.
• Have binary heap with arrays.
• Have in-place merge sort with arrays.
• Have k-median search with arrays.
• Investigate amortized complexity analysis.
• Prove in Coq.
• Infer BigO arity.
• Have built-in indexed uint.
• Pretty-print to SML.
• Combine cctx and tctx.
• Add <> notation.
• Add a return clause in Case to mean the time including the matchee.
• Amortized complexity of queue implementation by two stacks.
• Infer type according to pattern.
• (No longer exists.) Wrongly inferred T_insert_delete_seq_0 to be (fn n => $n) without the 2.0 + 48.0 * $n annotation. The source of the problem: unsoundness in bigO-solver.sml/solve_exists().
• Have some Nat/Time inference.
• Unify UnOpI, DivI and ExpI.
• Unify True and False.
• Change unify_s to is_sub_sort.
• Should apply solvers and check no-uvar after every module, not every file (unless we enforce one-module-per-file policy).
• Move VC openings from check_decl to check_decls.
• subst should do lazy shifting, not eager.
• The last two examples in bigO-evolve.timl about using idx instead of absidx does not work now.
• Simplify unused forall in prop. The unused foralls are Big-O premises.
• BigOEvolveSealed in bigO-evolve.timl does not work yet.
• if-then-else and list syntax.
• (No longer needed because uvars can be retrieved from modules now) Restore the version of link_sig in revision 00ba072, because a module may have uvars before sealing, and uvars cannot be retrieved from modules.
• Big-O solver should heuristically distinguish "defining" side of TimeFun uvars from the "using" side, by the rule-of-thumb that only _ <= f x is a defining constraint of f.
• Do a module dependent analysis of each module and only bring the needed modules into gctx VC context.
• Have double-linked lists.
• rbt6.timl: absidx sort Time inference error in IntKey.
• Currently absidx ... with ... end is "scoped abstract index". We should have "unscoped" or "module-scoped" abstract index absidx id = ... so within the module id's definition is visible but outside the module it is not.
• Make kind's sorts dependent, or only use bsort in kind.
• Generate typing derivations. Road map (a translation validation (i.e. derivation reconstruction) approach):
  • Generate type-annotation TiML syntax
  • Translate it to type-annotated micro-TiML syntax
  • Reconstruct micro-TiML typing derivations from type-annotated micro-TiML syntax
  • The micro-TiML to assembly-TiML compilation should also use this approach
• Remove annotations on case (at least in a mode).
• datatype can introduce index variable names at the first line for every constructor.
• find_hab is too slow on array-msort.timl and array-msort-inplace.timl
• A new unification framework ("skolemized unification"): every unification variable denotes a closed entity, which could be a lambda abstraction. For example, when we see type annotation [a : ] in the sorting context [x:Nat, y:Time], we introduce a uvar ?1 of kind [Nat => Time => Type], and replace the "" with [AppV ?1 [x,y]]. When we try to unify [AppV ?1 [x,y]] with [int], in principle we can't conclude that [?1 = int]. But exploiting specific knowledge in this language, we can. When we can have such a definitive conclusion, we refine ?1 to be [int]; but when we can't have a definitive conclusion when doing unification, we should record it as a VC. For example, when we try to unify [AppV ?1 [x,y]] with [AppV ?2 [x,y]], we should put [AppV ?1 [x,y] = AppV ?2 [x,y]] in VC, instead of conclude that [?1 = ?2] (unless we want to do incomplete, over-aggressive unification).
• SML supports datatypes instantiated with different type arguments within a constructor, such as [datatype 'a ls = Nil | Cons of 'a * ('a * 'a) ls]. TiML's typechecker also supports this. So TiML's proof should also support this. It has usage in for example Okasaki's implicit queue (thesis Chapter 8).
• (Abondoned. Non-constant subtracter is needed to support minus of nat type) Change minus from a binop to an unop where the second operand can only be constant.
• Investigate array-msort-in-place.
• Generalization has some problems with higher-order uvars.
• Simplify modules in output.
• Rename [long_id]'s [ID] to "Bound" and [QID] to "Free", in accordance with locally nameless representation.
• Add native booleans. Add more integer operations (including comparisons). Add more nat operations.
• Add example links to website.
• Remove assert_b and assert_b_m to make sure when assertion are turned off no computation will be wasted.
• Add ELength.
• eq_mt()/TDatatype needs to be implemented to allow instantiating dynamic-table.timl.
• Add negative examples.
• Argument module names of functors are put into global context, which may result in name conflicts. Should prefix argument module names with the functor names.
• Complete parser support for string literals and unescape().
• If a primitive shouldn't be redefined (especially base type names because type names appear in feedback messages), it should be made a keyword in timl.lex.
• Propogate return clauses through [ifdec] and [if]; let those time specs mean entire time including the matchee.
• Have sprintf.
• Check no-UVar after typechecking.
• Write simp_mt using visitor.
• A full storage interface should support the following containers:
  • map to nullable primitives
  • map to map
  • map to tuples
  • map to tuples of maps
  • indexed vector of primitives (vectors should guarantee elements are always well-formed and allow value types not inhabited by zero)
  • indexed vector of tuples (the problem with a vector of tuples is that there is no atomic push_back operation)
  • indexed vector of maps
  • indexed vector of tuples of maps
  • ref of primitives
  • ref of tuples
  • array of primitives
  • array of tuples
  • indexed nat
  • unindexed vectors as values of the above containers. An access to an element of an unindexed vector should include a length check.
• TiML should support state polymorphism (i.e. treating the entire state as an index) as MicroTiML, in order to support the 'for' combinator for stateful computations.
• Since TiML now has full support for record idx (IState) and record types (TRecord), we should change TRecord to be a type constructor that given a record idx constructs a record type. Then TiML is as powerful as Ur/Web!

To-do for MicroTiML

• remove let x = ... when x is "_", because such case can only be from translation of wildcard patterns
• remove duplicate EAsc and EAscTime
• analysing the form of expr is complicated by the pervasion of EAscType and EAscTime; need some principled way to transparently ignore EAscType/Time.
• dynamic-table.timl needs to be instantiated to be tested by MicroTiML compiler
• tc() should add annotations only when specific flags are turned on; the client that turns on these flags should consume the annotations to prevent them from polluting later translations.
• Add level limits to export_t and export_e.
• Add a pass to remove annotations on EVar, TVar and VarI after cc().
• Uniquefy variable names.
• check_CPSed_expr() should also check types.
• anf_decls() shouldn't alway use "x" as the new variable name, because it will replace other meaningful names after post_process(); it should take suggestions from surrounding ELet.
• Add a simplification for ECase where if the two branches are identical and don't mention the local variable, combine them and remove ECase.
• Remove datatype "micro_timl" and rename "micro_timl_ex" to "micro_timl".
• Rename "micro-timl/" to "compiler/".
• Add "let nat {i} = x in ..." to name the index of nat.
• Add register-file polymorphism so that EVM snippets for new_array and string_concat can be shared instead of inlined.
• pattern-ex.sml/remove_deep_many() should handle empty datatypes.
• The changed EVM typechecker (checking ASCTIME without later premises) still works on example recursive functions annotated only with case's return clause, because TiML typechecker added EAscTime (_, return - adjust) to everybranch. This trick won't work when the truthfulness of 'return >= adjust' depends on local premises. A thorough solution should be having bi-directional typechecking on every level and in the 'check type' mode, passing in (total_time_spec, time_accumulated_already), and allowing time_accumulated_already to be larger than total_time_spec, because later code can introduce a 'false' premise.
• This code in EtherDelta.etiml causes cost bug after CPS: fun trade (tokenGet : address, amountGet : uint, tokenGive : address, amountGive : uint, expires : uint, nonce : uint, user : address, v : uint8, r : bytes32, s : bytes32, amount : uint) = (amount is in amountGet terms) let hash : bytes32 = sha256(this, tokenGet, amountGet, tokenGive, amountGive, expires, nonce); if (not ( (* (orders[user][hash] || ecrecover(sha3("\x19Ethereum Signed Message:\n32", hash),v,r,s) == user) && ) ( block.number <= expires && ) safeAdd(orderFills[user][hash], amount) <= amountGet )) then throw end; ( tradeBalances(tokenGet, amountGet, tokenGive, amountGive, user, amount); ) ( set orderFills[user][hash] safeAdd(orderFills[user][hash], amount) ) ( emit Trade(tokenGet, amount, tokenGive, amountGive * amount / amountGet, user, msg.sender) ) ( ;(orderFills[user][hash], tokens[tokenGet][msg.sender], tokens[tokenGet][user], tokens[tokenGet][msg.sender], tokens[tokenGet][user], tokens[tokenGive][msg.sender], tokens[tokenGive][user]) *) halt 0x555
• There is a bug in BlindAuction.etiml that when inline let b = placeBid(msg.sender, value) typechecking after translation generates two wrong VCs.
• Functions below CPS should have multiple arguments to avoid tuple-related costs.

To-do for Examples:

• Binary search with arrays.
• binary heap with arrays.
• In-place merge sort with arrays.
• k-median search with arrays.
• Quicksort.
• Dijkstra algorithm.
• Two-stack queue (amortized).
• Double-linked lists.
• Union-find (amortized).
• Some example showcasing the flexibility of "size".