morganthomas / freecat Goto Github PK

1.0 4.0 0.0 195 KB

A programming language based on the principles of freedom and category theory.

License: Apache License 2.0

Haskell 99.12% Shell 0.88%

freecat's Introduction

This is a work in progress -- not good for anything yet!

cabal install
cabal build
./test.sh

freecat's People

Contributors

Stargazers

Watchers

freecat's Issues

Roll patterns into exprs

Instead of having a Pattern type, use Expr in place of Pattern with the expected invariant that patterns are only made of symbols and applications.

Include the type of an Expr as part of the Expr

This will entail computation on types happening in parallel with computation on exprs all the time. Omitting unnecessary type computation is an optimization.

Eliminate egregious performance problems

This issue is done when the program has been analyzed for opportunities to reduce the computational complexity class of algorithms, and all easy opportunities to do so have been pursued.

Include adequate information (source positions, etc.) in all error messages

Review digestion and evaluation algorithms for correctness

Write a small ordinary program in FreeCat, as an example

Support inference of type declarations for variables in pattern matching equations.

Support namespaces and multi-file programs

How should files and namespaces be related?

Break up Core.hs

Suggestion: three files, Core.hs, Digest.hs, Evaluate.hs. Digest and Evaluate depend on Core. Digest depends on Evaluate.

Properly define symbol equality

Write, test, and document a Prelude

TODO: what all should it include?

Support unique value inference

Be able to infer the value of an implicit argument by noticing that the context provides exactly one way of constructing a value of the argument's type. This feature should be able to replace simple uses of type classes. Example:

Bool : Type
true : Bool
false : Bool

Eq : Type -> Type
eq : {a : Type} -> {inst : Eq a} -> a -> a -> Bool

Foo : Type
foo : Foo
bar : Foo

eqFoo : Eq Foo
eq foo foo => true
eq bar bar => true
eq {inst = eqFoo} x y => false

example : Bool
example => eq foo bar

Expected result: example => false. eq foo bar is elaborated to eq {a = Foo} {inst = eqFoo} foo bar.

Have a good, short, high-level explanation of FreeCat

Remove variable type argument from LambdaExpr, SymbolExpr, DependentFunctionTypeExpr

It's redundant with the definedType of the Symbol which is the variable.

Do type checking during digestion

Update readme with detailed usage instructions

Check test coverage completeness (excluding error paths)

Find all code paths and use reasoning to verify that each code path is executed by the test cases. Error conditions are excluded from the scope of this issue.

Have a detailed design rationale for FreeCat

Brainstorm reflection primitives

Create end to end test runner

It should run freecat on all the test cases in test/cases. It should check that all equations for each test case are true in the test case's context.

Support implicit arguments

E.g., should be able to write: e.g.: map : {a : Type} -> {b : Type} -> (a -> b) -> List a -> List b, with the values of a and b inferred at the call site during digestion or evaluation if not specified explicitly.

For this issue, it's sufficient to have one tactic for inferring the value of implicit arguments, based on unification of terms and types of terms around the function call site.

Support inferred implicit arguments

Infer implicit argument declarations for free variables in type declarations. E.g., should be able to write: map : (a -> b) -> List a -> List b. This should be equivalent to: map : {a : Type} -> {b : Type} -> (a -> b) -> List a -> List b. The types of a and b should be inferred from the context of the usage of the variables. E.g., here List : Type -> Type, so from the usage List a you can infer a : Type.

Have basic I/O primitives and basic IO monad

Properly define expression equality

Write, test, document reflection library/primitives

Every FreeCat concept should be first-class reflected within FreeCat. There should be types for exprs, symbols, contexts, etc. There should be functions for context loading and expr evaluation. What else?

Don't allow anything to match a duplicate pattern variable

Turn (Maybe SourcePos) to SourcePos in Expr, Equation

Some Expr and Equation are generated dynamically, e.g. via evaluation. These can still get SourcePos values by inheriting from what they're derived from.

Implement comments

Implement Haskell-style comments: -- and {- -}. Nested comments should be supported.

Finish out error reporting coverage

This issue is done when every error condition provides meaningful, useful output including line numbers and so forth; when the error and debug output is not excessively verbose by default; when there is no debug output for an error-free program by default; and when error reporting is tested in the automated regression suite.