ct-gradual-typing / papers Goto Github PK
View Code? Open in Web Editor NEWThe Combination of Dynamic and Static Typing from a Categorical Perspective
The Combination of Dynamic and Static Typing from a Categorical Perspective
Be able to use :l and :r in REPL
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.
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?
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.
Consider the example:
"(squash) (\\(y:?).x ((split) y))"
There are parens around squash
and split
.
Please modify the pretty printer to remove those.
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.
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.
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".
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 have written up a section on how to extend Grady with polymorphism. We should add this to our implementation.
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?
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.
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.
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?
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, 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>
.
Now that typeCheck is compliling, work on putting it together with typeCheck_aux
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
.
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?
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.
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.
typeCheck_aux (Pair t1 t2) = do r1 <- typeCheck_aux t1 r2 <- typeCheck_aux t2
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?
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?
One thing you will need to figure out is how to get the paper compiling on your machine.
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?
Use LUnbind and LFresh to eliminate Fresh constraints
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?
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)
Finish typechecking error message. the TODO one
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.
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.
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.
In TypeChecker:
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
.
Remove tab characters from all files
This is the section you will be writing, but not until after you have implemented all the examples.
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.
There has been lots of changes to the syntax, so the pretty printer needs updating to match.
See commit b6dae76.
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"
How do I access TyCtx inside of typeCheck_aux so I can look up the variable type?
The evaluator is next up for implementation. The rules can be found in the paper. See Figure 7 captioned "Reduction rules for Grady."
Update parser with Box and unbox, taking our gen
A declarative, efficient, and flexible JavaScript library for building user interfaces.
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
The Web framework for perfectionists with deadlines.
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
We are working to build community through open source technology. NB: members must have two-factor auth.
Open source projects and samples from Microsoft.
Google ❤️ Open Source for everyone.
Alibaba Open Source for everyone
Data-Driven Documents codes.
China tencent open source team.