ct-gradual-typing / papers Goto Github PK

The evaluator is next up for implementation. The rules can be found in the paper. See Figure 7 captioned "Reduction rules for Grady."

1. Make a file that houses functions that can be pulled into the REPL and those functions can be used within the REPL.
2. Finish TypeChecker.hs
3. Once TypeChecker is finished, make a list of test cases
4. Practice using question mark type

How do I access TyCtx inside of typeCheck_aux so I can look up the variable type?

Need to think more about the error cases in the evaluation.

If the argument to unbox is in head-normal form, and not a box, then throw an error.

If the argument to unbox is a box t, but t doesn't have the right type, then through an error.

Currently, in the implementation we have:

split : ? -> (? -> ?)
squash : (? -> ?) -> ?

but we now need to change these to:

split S : ? -> S
squash S : S -> ?

where S is either ? -> ? or ? x ?.

I know you showed me an example of the syntax for using the free variables functions found in Unbound-LocallyNameless. Its type:
fv :: (Rep a, Alpha t, Collection f) => t -> f (Name a)
Is a bit confusing for me. I know the Collection f piece is to basically tell fv what type of collection to return. Can you post an example?

Update parser with Box and unbox, taking our gen

Can you take a look at what I just pushed? I left a hole that needs to be filled with the type TE.typeError. When I put in the typeError I want to throw, NoMatchError, it keeps saying there is no data constructor for it. Is that because I'm trying to throw a type and not a value of that type? If that is the case, I don't see anything in the code of that type. I hope this makes sense.

Use LUnbind and LFresh to eliminate Fresh constraints

1. Fix squash and split, add to aterm
2. Makes more examples, include what the output should be:
   a. include types that don't fail in a file
   b. include types that do fail in another file
   c. include types that push the constraints for each type
   d. look into using QuickCheck
   i. generate types
   ii. generate random expressions
3. Make a branch (after finishing TypeChecker and merged into master) to start implementing loading and reloading a file into the REPL

1. Should
   data Prog = Def Vnm Type Term
   be
   data Prog = Vnm Type Term
   For example, from out test file:

     true : ? -> ? -> ?
     true = \(p:?).\(q:?).p
   

   Would Vnm be true, Type be ? -> ? -> ?, and Term be \(p:?).\(q:?).p? If this is correct, what would Def be?

I have written up a section on how to extend Grady with polymorphism. We should add this to our implementation.

1. Use parse with parseFile, which should return a [Prog], if so then, convert to GFile
2. Work on typchecking

1. In TypeChecker add x to the context before calling typeCheck_aux
2. Make constructor for Box error
3. Implement Squash
   ex. :t (x:? -> ?).(x (squash x)) should get (? -> ?) -> ?
4. Implement Split
5. Make example for each type of Term
6. Fix pretty printer, it's printing out "U" instead of ?
7. System should be able to do anything in untyped lambda calculus

I'm working on implementing Squash. Looking at the draft, Squash doesn't take in any arguments. Is this correct? Looking at the example from Monday's meeting: (x:? -> ?).(x (squash x)) it seems to take an argument. Am I just not understanding Squash, or is that a change in the draft that needs to be made?

Currently items added to the queue are not type checked before being added to the queue. Correct this for both loading an external file and adding definitions in the Repl

Currently, box and unbox have the following type:

box<T> :: T -> ?
unbox<T> :: ? -> T

However, the boxing and unboxing algorithms never apply box nor unbox to anything other than an atomic type. This suggests that we can simplify our system, and hence its semantics.

I think, we really only need:

box<C> :: C -> ?
unbox<C> : ? -> C

where C is an atomic type. It's grammar is as follows:

C ::= Nat | Unit

Now using the boxing and unboxing algorithms we can show that the rules we have now are derivable. That is, we can show that they can be defined in terms of the rules we already have.

One interesting point about boxing and unboxing is that they do form a retract, but only after some evaluation. That is, (informally) unboxing (boxing t) ~>* t instead of unboxing (boxing t) ~> t.

One thing you will need to figure out is how to get the paper compiling on your machine.

Be able to use :l and :r in REPL

Dr. Eades,

When you get a second will you look at the latest push to the branch? It won't compile because of a change I made to the TypeErrors module. However, I can't understand why this doesn't work. I'm trying to use the prettyTerm function which returns an LFreshM String, I'm trying to get the string back and use it in the error message but for some reason it won't work. Can you shed some light as to why?

Consider the following example:

Grady> let x = triv 3
Grady> :d
["let x = triv (3)"]
Grady> :t x
NotArrowType Unit
Grady> 

However, the repl should never allow a definition that doesn't type check to be added to the queue.

Finish typechecking error message. the TODO one

When running Repl.hs, if you load a file with definitions and then ask it to dump the state. It will show the state and then exit the Repl. It needs to stay in the Repl after dumping the state.

Currently, we only squash function types. That is, types of the form ? -> ?. However, this will prevent the proof we need from going through, because the Siek:13 language allows for types of the form ? x ? to be squashed. I think we need to add this to our system.

1. Finish Free vars checking
2. Worker on parser for reading in definition file
   a. Parser should read in one line at a time
   a. use "eol" instead of "eof"

This is the section you will be writing, but not until after you have implemented all the examples.

I ran across this example and I don't think this should typecheck.

Grady> :t \(m:Nat) -> unbox<Nat> m 
Nat -> Nat

It's my understanding we should not be able to unbox a Nat? Is that correct?

When a new file is loaded into the Repl, dumb the state first and then load the file. Currently, you must quit the Repl to empty the state.

Can you take a look at the latest loadfile branch? I've tried figuring these two issues out over the last two days but I'm still stuck. Here are the issues. If you could just help point me in the right direction, that would be helpful.

1. For some reason, the file loading only parses out the first definition and expression. This is especially confounding as the code has parseFile = many parseDef which should use the parseTypeDef and parseExpDef parsers multiple times. I also had to add the separator \\ between the end of one expression and the next definition. Without this, the parser was mixing an expression with the following definition. It didn't stop parsing one expression at the white space separating that expression from the next definition.

2. I've also found another issue revolving around variables starting with 't'. For example:
   let true = \(p:?).\(q:?).p
   works just fine. But if you try to typecheck this, you get the error:

unexpected 't'
expecting "triv" or end of input

I first thought this was coming from the REPL parser but then we should have the same issues any variables starting with 'd', or 'u'. So I'm not really sure where this is coming from. Any thoughts?

Loading same file more than once continues to load the file more than once into the queue. Create a check before loading the definitions into queue to see if there are already there.

There has been lots of changes to the syntax, so the pretty printer needs updating to match.

See commit b6dae76.

1. Church Encodings for Numbers/operations and Booleans
2. Improve error messaging
3. Pretty printing, e.g. numbers with too many parenthesis

Currently, this won't typecheck anymore:
\(m:?).\(f:? -> Nat).box<Nat> (f m)

It should typecheck to:
? -> Nat -> (? -> Nat) -> ?

It fails to parse in anything after box<T> or unbox<T>.

REPL commands should not be reserved operators:

https://github.com/heades/gradual-typing/blob/loadfile/impl/Parser.hs#L33

They need to be removed from there.

fileParser is not implemented correctly. See:

https://github.com/heades/gradual-typing/blob/loadfile/impl/Parser.hs#L222

Don't parse in ":l" as a token, instead do it like the other parsers. As is this parser doesn't support both ":l" and ":load".

Implement changes from syntax rules for box and unbox. Unbox now takes in an expected type, T. Unbox should check to make sure t can be "casted" to T.

1. Update with runParser and readFile instead of parse when parsing in grady file
2. Flesh out more examples, esp. List -> untyped list holding typed data

Now that typeCheck is compliling, work on putting it together with typeCheck_aux

1. In draft file, should box accept a parameter in the term definition. It seems to in the syntax rules (box t : ?).
2. Does subscript T in the draft file mean that the function takes a parameter of type T?
3. In the code:
   typeCheck_aux (Pair t1 t2) = do r1 <- typeCheck_aux t1 r2 <- typeCheck_aux t2
   Why are r1 and r2 (Maybe Type) and not Types when typeCheck_aux :: Term -> TCM Type?

Consider the example:

"(squash) (\\(y:?).x ((split) y))"

There are parens around squash and split.

Please modify the pretty printer to remove those.

1. Improve error messages to make them more readable
2. Implement Y combinator, call file Y.gry but give its definition name "Fix"
3. Implement Repl help command, :h

I know I need to use liftM in the typeCheck function so that it returns (Either TypeError LFreshM). I took another stab at doing this today but still can't figure it out. It's like (ask) pealed away the first layer of the ReaderT and now I need to use LiftM to peal back the last layer. Can you provide some hints on what I need to do?

Consider the following example:

Grady> :l Examples/Combinator.gry
Examples/Combinator.gry  does not exist.
Grady> :l Examples/Combinator.gry
(line 11, column 12):
unexpected "\n"
expecting digit or ";"
Grady>

The first load command has a space at the end of the line, and the second does not.

Now consider the following:

Grady> :l Examples/Combinator.gry                    
Examples/Combinator.gry                     does not exist.
Grady> 
```

Notice the spaces before "does".  

Whitespace needs to be trimmed off of the end of the file name.

The natural number eliminator needs to be implemented. See the definition of the syntax Definition 4.1 "Syntax of Grady" and the definition of its typing rule in Figure 6 "Typing rules for Grady", and the definition of its evaluation rules in Figure 7 "Reduction rules for Grady"

When testing the REPL I noticed that the order of assigning variables is quite strict. This may be a design decision or it could be a bug, let me know where you want to go with this.

Try this in the REPL:

let p = fun m (triv triv)
let m = (succ unit)
:u p

Your output is fun m (triv triv) whereas I had expected it to use the value of m and display fun (succ unit) (triv triv) . It will display that if you switch the order of commands to this:

let m = (succ unit)
let p = fun m (triv triv)
:u p

Again this may be expected behavior but it just surprised me so I wanted to bring it up and get your thoughts on it.

Remove tab characters from all files

I am thinking it might be nice to try and see if we could get importing working.

The syntax might look like this:

import file1
import file2
import file3
import file4
...
import filei

where each filej corresponds to a Grady file filej.gry.

We need to go over the pretty printer and add more parens in places. For example,

Grady> :t \(X<:*)->\(x:X)->x
forall (X<:*).X -> X

The output type should actually be:

forall (X<:*).(X -> X)

In TypeChecker:

1. Implement ReaderT monad transformer
2. Use except monad transformer, where you must catch the exception
3. Put exception handling in REPL
4. Make data type for each exception
5. Implement Data.Map for type TyCtx

I've been messing with the REPL for a while now but I realize I keep trying to evaluate expressions! I have come up with other non-evaluate commands but I haven't come up with a command that uses the ? type. Could you give me a basic example so that I could mess with it and get a feel for working with it?