Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Sean/mandatory kinds #35

Merged
merged 104 commits into from
Sep 4, 2024
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
104 commits
Select commit Hold shift + click to select a range
04eece1
flake
gnumonik Nov 29, 2023
c6c8930
shell
gnumonik Nov 29, 2023
3e3562c
Added uplc command line option for , pulled in plutus-core dep from C…
gnumonik Nov 30, 2023
99c51cb
PlutusIR dependency sorted out
gnumonik Nov 30, 2023
75012d1
Typed CoreFn conversion & pretty printer (messy)
gnumonik Dec 6, 2023
62c4685
More detailed tracing to investigate type reprs
gnumonik Dec 6, 2023
b173baf
Switched to a typed CoreFn data type (instead of stashing type info i…
Jan 12, 2024
5b02fe1
Preserving ForAll quantifiers in output CoreFn AST (WIP/maybe broken)
Jan 17, 2024
822c6d4
Let bindings/declaration groups debugging, working on quantifier pres…
gnumonik Jan 18, 2024
23fac0a
Working on conversion of typeclass dictionaries. (Pretty messy, using…
gnumonik Jan 20, 2024
f3a86eb
Adjusted typeclass desugaring to use real source locations in the cas…
gnumonik Jan 24, 2024
28a850e
Conversion to typed CoreFn for desugared typeclass dictionaries seems…
gnumonik Jan 24, 2024
282d951
Typed CoreFn conversion now works with MPTCs, cleaned up a bunch of u…
gnumonik Jan 25, 2024
cdd4bb1
Substantial cleanup + documentation pass
gnumonik Jan 25, 2024
766b580
Merge pull request #17 from mlabs-haskell/sean/typedCoreFn.typeclasse…
gnumonik Jan 25, 2024
6e2ca01
Nested 'let' expressions w/ mix of type sigs/no type sigs w/ quantifiers
gnumonik Jan 25, 2024
51344c8
Mutually recursive binding groups, binders, attempt at generalizing T…
gnumonik Feb 1, 2024
9ffcbcf
Merge pull request #19 from mlabs-haskell/sean/typedCoreFn.wip
gnumonik Feb 1, 2024
722a0cc
fixed small mistake, deleted some traces, added comment or two
gnumonik Feb 1, 2024
e6237d8
Merge branch 'sean/typedCoreFn.wip' into sean/typedCoreFn
gnumonik Feb 1, 2024
02129dd
Fixed mutual recursion bug in declToCoreFn, removed let generalizatio…
gnumonik Feb 3, 2024
b2befc1
Fixed problem w/ object literal binders, cleaned up the interface of …
gnumonik Feb 6, 2024
5f464c5
Primitive infrastructure for golden tests, removed some dead options
gnumonik Feb 21, 2024
aa95066
testing infrastructure, ported some tests/purs/passing tests to debug…
gnumonik Feb 22, 2024
5a83437
Fixed bug discovered in test #4301 (I hope...)
gnumonik Feb 27, 2024
c99c476
Fixed issue w/ transitive imports resulting from explicitly desguarin…
gnumonik Feb 29, 2024
293acc9
Documenting/Explaining the use of new utils
gnumonik Feb 29, 2024
1e17804
Type inference/checking machinery removed from CoreFn desugaring mach…
gnumonik Mar 1, 2024
161bdef
Added some empty list tests
gnumonik Mar 1, 2024
f35cdb0
Prettyprinter replacement implemented (still needs some tweaking)
gnumonik Mar 2, 2024
b4f557e
prettyprinter improvements
gnumonik Mar 2, 2024
7876fdb
even prettier
gnumonik Mar 2, 2024
c862bd5
extremely pretty
gnumonik Mar 2, 2024
4b6112c
Refactored pretty printer update to use Reader monad (hopefully makes…
gnumonik Mar 5, 2024
cb11738
Final cleanup/tweaks to pretty printer
gnumonik Mar 5, 2024
d295a01
Module-ized prettyprinter + some small tweaks
gnumonik Mar 6, 2024
ae4f703
Nix setup
t4ccer Feb 18, 2024
991c758
Trigger CI
t4ccer Feb 18, 2024
4214ae6
Remove unused configs
t4ccer Feb 18, 2024
6349472
Disable typos check
t4ccer Feb 18, 2024
ed35645
Remove Nix Plutarch wrapper
t4ccer Feb 23, 2024
a9f7a14
Removed some dead comments, testing pre-commit hooks
gnumonik Mar 6, 2024
115cb65
working on monomorphizer (seems to work w/ non-recursive binding grou…
gnumonik Mar 15, 2024
cada4c7
re-implementing monomorphizer (wip)
gnumonik Mar 16, 2024
584cf12
monomorphizer works on the simplest possible mutually recursive examp…
gnumonik Mar 19, 2024
babc876
Support for PLC Builtins and primitive types
gnumonik Mar 20, 2024
db81559
re-organize modules
gnumonik Mar 20, 2024
3a1302d
utilities for object desugaring
gnumonik Mar 20, 2024
7106f6f
Conversion to Bound, object desugaring
gnumonik Mar 21, 2024
d08e03e
Prettyprinter for Bound AST, fixed some bugs in object desguaring, re…
gnumonik Mar 22, 2024
9e83557
Reworked final IR, prettyprinters, debugging + reworking monomorphize…
gnumonik Mar 22, 2024
8a84e77
forgot to commit new file
gnumonik Mar 22, 2024
9dbd7b7
full Purs->UPLC pipeline working for very simple examples. builtins w…
gnumonik Mar 23, 2024
71add6a
remoted test output dirs from gitignore (so can link to things)
gnumonik Mar 23, 2024
3b24eef
wrong output file name in test
gnumonik Mar 23, 2024
3f8183d
working on case expressions
gnumonik Mar 26, 2024
87fd8cc
basic PLC test infrastructure
gnumonik Mar 26, 2024
e076b6a
fixed some tests
gnumonik Mar 26, 2024
e6cb3ba
architecture doc
gnumonik Mar 28, 2024
d3a263c
Removed type annotations from CoreFn and ctors
gnumonik Mar 29, 2024
809249c
Working on better case desugaring. (Their algorithm works for us but …
gnumonik Apr 13, 2024
c8fac0a
Guard/case desugaring w/ correct types
gnumonik Apr 19, 2024
1b55f26
Fix objects introduced by forall without typeclass constraints
t4ccer Apr 24, 2024
e19e729
Add tests for objects with forall
t4ccer Apr 25, 2024
5d12065
Fix arrays introduced by forall
t4ccer Apr 25, 2024
dd62554
Remove FFI codegen
t4ccer Apr 22, 2024
722270d
Tentative fix for #30 (superclass method access)
gnumonik Apr 30, 2024
c06ac6b
Parametrize IR AST with type
t4ccer May 1, 2024
376ef2f
Initial CoreFn -> IR transformation
t4ccer May 2, 2024
ac9137b
Track object presence on type level
t4ccer May 5, 2024
b971e9c
Remove guarded patterns
t4ccer May 5, 2024
8aedd54
Merge branch 'sean/monomorph-cleanup' into t4/ast2
t4ccer May 5, 2024
5d70096
Ignore `cache-db.json` files
t4ccer May 5, 2024
1ddbe4e
WIP Monomorphizer rework for AST
t4ccer May 5, 2024
f74e778
Some stuff
t4ccer May 8, 2024
3ad78bf
Parameterized module, TypeLike class for common operations on types, …
gnumonik May 9, 2024
d1dd427
IndexedPlated instance for Exp
gnumonik May 10, 2024
df5cc44
changed IndexedPlated to Plated
gnumonik May 10, 2024
33476ce
monomorphizer utils, started reworking inlineAs
gnumonik May 11, 2024
eca9e88
types mostly line up, might break things in a sec
gnumonik May 14, 2024
1b17a50
made the types line up in the monomorphizer rewrite
gnumonik May 15, 2024
96d4b9e
monomorphizer rewrite works for simple examples
gnumonik May 16, 2024
f05bf14
Changed the body of BindE to Exps (from Scopes), cleanup, doc comments
gnumonik May 16, 2024
0993609
Removed dead code, misc cleanup
gnumonik May 16, 2024
fe6d66e
disabled UPLC tests while we rewrite things
gnumonik May 16, 2024
8d2d2df
initial draft of simplified datatype binding/translation machinery
gnumonik May 17, 2024
ee3b27e
started implementing mandatory kinds. compiles but very broken atm, n…
gnumonik May 18, 2024
764b71c
trying to fix mandatory kinds design flaws & bugs (compiles but broke…
gnumonik May 22, 2024
69397fd
Restrict kind annotations to just identifiers and arrows
klntsky May 22, 2024
8b06941
Update the parser: use kind everywhere for TypeKinded
klntsky May 22, 2024
291750e
Fixed a few bugs resulting from mandatory kind annotations for TyVars…
gnumonik May 23, 2024
fb2838f
Use square brackets for rows
klntsky May 23, 2024
faf2514
pre-merge backup commit
gnumonik May 23, 2024
426c4ff
Merge branch 'klntsky/parser-tweaks/sean/mandatory-kinds' into sean/m…
gnumonik May 23, 2024
8838a77
Disallow named instances in the parser
klntsky May 24, 2024
bbe329e
Add quantifiers for instances
klntsky May 24, 2024
141c11f
restrict kinds in `forall (a :: kind)` parser to be kinds only
klntsky May 24, 2024
ff0b89f
fixed bugs in backticked infix expressions & superclass variables types
gnumonik May 25, 2024
27d8648
fixed a bug in the CST grouper, cleaned up old passing tests
gnumonik May 25, 2024
ceb7ddb
Merge branch 'klntsky/parser-tweaks/sean/mandatory-kinds' into sean/m…
gnumonik May 25, 2024
7f10e5a
better row syntax tests to help vladimir debug
gnumonik May 25, 2024
1de91e0
more row syntax tests
gnumonik May 25, 2024
89162e4
linting
gnumonik May 28, 2024
5777b4e
Fixed mistake (ignored TVBinders in instance chains), cleaned up/fixe…
gnumonik May 28, 2024
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
The table of contents is too big for display.
Diff view
Diff view
  •  
  •  
  •  
1 change: 1 addition & 0 deletions .envrc
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
use flake
7 changes: 6 additions & 1 deletion .gitignore
Original file line number Diff line number Diff line change
Expand Up @@ -19,7 +19,7 @@ bower_components/
node_modules
tmp/
.stack-work/
output
# output
tests/purs/docs/docs/
core-tests/full-core-docs.md
tests/support/package-lock.json
Expand All @@ -38,3 +38,8 @@ TAGS
*.ps
*.svg
tests/purs/make/
.direnv/
/.pre-commit-config.yaml
/result*

tests/purus/passing/**/cache-db.json
100 changes: 100 additions & 0 deletions Architecture.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,100 @@
# Architecture

This document contains an overview of the *current* architecture of our compiler pipeline. It is not meant to be exhaustive and is intended to serve as a guide for onboarding new developers / make the giant PRs more accessible.


## Step 1: Type Deduction/Synthesis (Language.PureScript.CoreFn.Desugar)

During the research phase of this project, we determined that PIR (Plutus Intermediate Representation) should be our ultimate compilation target (with final compilation to UPLC handled by the PIR compiler). Because PIR is an explicitly typed language, and because the vanilla `CoreFn` AST is not explicitly typed, it is necessary to convert the `Language.PureScript.AST` AST into a typed variant.

Because conversion to `CoreFn` occurs after the initial (vanilla PS) typechecker pass, we receive *most* expressions (but not all of them) annotated with the inferred or explicitly declared type. Desugared expressions or declarations involving type classes, however, are not ignored by the PS typechecker, but we require explicit annotations for explicit type class dictionaries and the functions that operate on them.

This step consists of two main phases:

- First, we traverse every *type* annotation in the vanilla PS `Module` that is the input to our conversion function and desugar constraint types to types that require explicit dictionary arguments. E.g. `Eq a => a -> (...)` becomes `Eq$Dict a -> a -> (...)`.
- Next, we deduce the types. Because top-level declarations are always explicitly typed, we proceed "top-down" from the top-level signature as far as we can, and switch to a "bottom-up" synthesis strategy in cases where the type cannot be determined by the top-level signature.

Some notes:

- We want to preserve quantifiers in this step. While some quantifiers can be eliminated during monomorphization, there is no guarantee that *all* of them will be eliminated (this is not a problem, because PIR supports universal quantification). This requires special machinery when performing type deduction on expressions that contain quantified polymorphic functions, since we must take care to ensure that the type variables "line up".
- We run our desugarer in the same monad stack as the PS TypeChecker, but this is largely a convenience (since it lets us use the PS machinery for binding local variables or type variables, etc). We should *never* perform type inference or make any calls to `unify`.
- The trickiest part of this is ensuring that type information for explicit type class dictionaries is introduced at the correct point. Again, type class dictionaries are not processed by the PS typechecker.

## Step 2: Monomorphization & Inlining (Language.PureScript.CoreFn.Convert.Monomorphize)

PureScript's implementation of Records employs Row Types. Moreover, PureScript supports *polymorphic* records, which are backed by *open rows* (e.g. `{a :: Foo | r}`).

Records in PureScript (unlike in Haskell) are not just syntatic sugar for products - the order of fields in the record is *not* determined by the order of fields in the declaration or expression that introduces the record. *An* order can be established for any fully instantiated (i.e. closed - doesn't contain any type variables of kind `Row Type`) record types - we choose a lexicographic ordering to mirror PureScript's `RowToList` sorting but this is not essenital.

We must, therefore, perform monomorphization on record types in order to transform Object Literals to literal products, transform record accessors into `case` analysis of the product that corresponds to the original record, and transform record updates into product updates.

Because a single polymorphic record type may be instantiated to different concrete types at different places in the AST, we must also inline while we monomorphize.

The general monomorphization procedure is as follows (not a full algorithm):

1. We traverse the AST until we reach an `App` node.
2. We "peel" the App node and get an `(f,args)` where `f` is the "terminal" function expression and `args` is a list of the argument expressions to which it is applied.
3. We check whether the type of `f` is already monomorphic. If it is, we make no change to the node.
4. If `f` is not monomorphic, we strip the quantifiers and check whether we can specialize any bound type variables to a concrete type. E.g. if `f :: forall x. Tuple x x -> x -> Int` and the arguments are `[Tuple String String, String]`, we instantiate `x` to `String`.
5. We recurse down the list of arguments. If we encounter an argument that is a free (term-level) variable that is *not* a Plutus builtin, we inline it, monomorphizing it to the concrete type of the argument if possible.
6. We apply the (possibly monomorphized & inlined) argument to the function and procede to the next argument
until we run out of arguments to process.
7. Finally, we re-quantify the type of `f` in the resulting expression. (It may contain free type variables of kind `Type`, which can be represented in PIR)

The procedure for inlining is:
1. We check whether the (term level) variable we aim to inline is locally scoped (i.e. qualified by source position) or globally scoped (e.g. qualified by module name). For now, we only attempt to inline globally scoped variables (...I forget why...)
2. If the variable is globally scoped (i.e. is the name of a module-level declaration), we lookup the body of the declaration. There are two possibilities here: Either the declaration will be a single non-recursive binding, or it will be a member of a mutually recursive binding group. (PS compiler sorts these for us)
- If the declaration is non-recursive we "walk" its expression-body and monomorphize/inline the sub-expressions as necessary in order to properly assign the expression the type that it is to be monomorphized to.
- If the declaration the member of a recursive binding group, we pause inlining, walk the expression, and "collect" a `Map Name (Name,SourceType,Expr)` where the key is the original name of the expression, and the values are, respectively: The new "fresh" name to give to the monomorphized expression, the monomorphic type that we must assign the expression to, and the body of the declaration. We do this recursively until we have collected every member of the recursive binding group used in the target expression. Finally, we use that map to construct a *monomorphic* mutually recursive binding group (where the names are all fresh) and create a `Let`-binding for the monomorphized mutually recursive group.

The implementation of the monomorphizer/inliner consists in a few key functions that call each other recursively. To make reviewing easier, here's a brief explanation of what the key functions do (or are supposed to do at any rate):

- `monomorphizeA` is the entry point that checks whether the node is an `App`, peels the arguments and function parts from the `App`, and calls `handleFunction` on the function expression and its arguments.
- `handleFunction` branches depending on the function expression it is passed:
- If it is passed a `Var` qualified by modulename, and the modulename is `Builtin`, it just returns the variable (since Builtins cannot be meaningfully inlined).
- If it is passed an `Abs`, `handleFunction` tries to instantiate the type variables of the function type with corresponding concrete types of the arguments. If it succeeds, it subsitutes the concrete type in for the bound type variable in all sub-expressions and their types, then calls itself recursively on the body of the `Abs` until the type has been fully monomorphized.
- If it is passed a `Var` that is not a builtin, `handleFunction` attempts to inline the expression the `Var` refers to by calling `inlineAs` with the monomorphized type. If this succeeds, `handleFunction` calls itself recursively with the monomorphized/inlined expression.
- If it is passed anything else as the `f`, it checks whether the function type is monomorphic.
- If the `f` is monomorphic, it applies it to its arguments and returns the resulting expresion.
- If the `f` is not monomorphic, `handleFunction` throws an error.
- `inlineAs` performs inlining and implements the above algorithm. Note that `inlineAs` is passed a PS `Type` argument, which represents the type that the expression corresponding to the `Name` being inlined *should* have after inlining.
- `monomorphizeWithType` rewrites the type of an expression to match the supplied type and (much more importantly) rewrites the types of all sub-expressions to conform with the supplied type of the top-level expression.

## Step 3: Object desugaring and final IR (Language.PureScript.CoreFn.[IR / DesugarObjects])

By the end of step 2, all polymorphic records have been monommorphized that can be monomorphized, but record-specific expression nodes (object updates/accessors/literals) still remain in the AST. In order to ensure that all "invalid" expressions and types have been desugared/eliminated prior to final PIR conversion, we define a restricted AST and `Type` type such that only expressions which can be converted into PIR can be represented - a kind of "parse-don't-validate" approach. (This AST is implemented with the `Bound` library.)

At this stage, we construct a set of dictionaries for type and data constructors. When constructing these maps, we add an arbitrary number of constructors for anonymous products (i.e. tuples) to accommodate objects. Specifically, we add constructors for tuples of up to 100 (they look like `data $GEN.~Tuple1 a = $GEN.~Tuple1 a` etc). These dictionaries serve two purposes:
- We construct them in such a way that the SOP representation of the underlying data type is very explicit. I.e. for each *type* constructor, we construct an `[(Int,[Type])]` where the `Int` represents the corresponding data constructor's index in the data type, where this information (the constructor's index & arguments) is also available in the dictionary for each *data* constructor. (Due to the implementation of the PS AST, we need both of these dictionaries, even though in principle only the tycon dictionary is necessary)
- Embedding generated tuple types into these dictionaries allows us to treat desugared records as "normal" data types in the final compilation stage (i.e. they don't require any special handling).

Conversion into this restricted IR AST is, aside from object expressions, very straightforward. Therefore, in the rest of this section I will explain the object desugaring process.

### Object Literals

1. We extract a `Map PSString SourceType` from the object literal expression by inspecting the expressions in each field.
2. We sort the fields lexicographically (which establishes the uniform order of the product that will be constructed).
3. We generate "fake" names for the product's type and constructor. E.g. `$GEN.~Tuple2 a b`.
4. We construct a specialized function type for the product's data constructor using the sorted arguments.
5. We assemble the literal with the "fake" constructor function and the arguments.

### Record Accessors
1. We perform steps 1-4 of Object Literals conversion on the expression the accessor is being applied to, except we construct a Constructor `Binder` (a pattern), where the arguments are wildcard binders for every argument except the one that corresponds to the field being accessed.
2. We use that pattern to construct a case expression that extracts the value corresponding to the field.
- This is kind of hard to explain without an example. Suppose we have `foo = {a: 1, b :: "yup"}` in `foo.b`
- That gets turned into (something like) `case foo of {$GEN.Tuple2 _ $HERE -> $HERE} `

### Record Updates
1. Proceeds much like the accessor case, except we return a product in our case expression instead of returning a field.
- Using the above definition of `foo`, if we have `foo {b = "hello"}`, this turns into:
- `case foo of {$GEN.Tuple2 a _ -> $GEN.Tuple2 a "hello"}`

## Step 4: Final Conversion to PIR (Language.PureScript.CoreFn.Convert.ToPIR)

The final step of compilation is conceptually simple: We match on the constructors of our final IR and translate expressions (and the types they contain) into PIR `Term`s and `Type`s, using some machinery to generate fresh names when we need to construct a lambda (which should only happen when desugaring case expressions).

NOTE: The *implementation* of case expressions is incredibly complex. At the moment we support matching on simple constructor patterns. Going forward, we ought to weak the final IR so that case expressions are presented in a form that makes it simpler to handle.




16 changes: 16 additions & 0 deletions cabal.project
Original file line number Diff line number Diff line change
@@ -1,2 +1,18 @@
repository cardano-haskell-packages
url: https://input-output-hk.github.io/cardano-haskell-packages
secure: True
root-keys:
3e0cce471cf09815f930210f7827266fd09045445d65923e6d0238a6cd15126f
443abb7fb497a134c343faf52f0b659bd7999bc06b7f63fa76dc99d631f9bea1
a86a1f6ce86c449c46666bda44268677abf29b5b2d2eb5ec7af903ec2f117a82
bcec67e8e99cabfa7764d75ad9b158d72bfacf70ca1d0ec8bc6b4406d1bf8413
c00aae8461a256275598500ea0e187588c35a5d5d7454fb57eac18d9edb86a56
d4a35cd3121aa00d18544bb0ac01c3e1691d618f462c46129271bccf39f7e8ee


packages:
purescript.cabal

-- HACK: plutus core cannot build without it, remove after bump.
constraints:
nothunks < 0.2
31 changes: 31 additions & 0 deletions default.nix
Original file line number Diff line number Diff line change
@@ -0,0 +1,31 @@
{
perSystem = { self', pkgs, config, ... }:
let
cardanoPackages = pkgs.fetchFromGitHub {
owner = "input-output-hk";
repo = "cardano-haskell-packages";
rev = "3df392af2a61d61bdac1afd9c3674f27d6aa8efc"; # branch: repo
hash = "sha256-vvm56KzA6jEkG3mvwh1LEdK4H4FKxeoOJNz90H8l8dQ=";
};

purus = config.libHaskell.mkPackage {
name = "purus";
src = ./.;

externalRepositories = {
"https://input-output-hk.github.io/cardano-haskell-packages" = cardanoPackages;
};
};
in
{
devShells.purus = purus.devShell;

packages = {
purs = purus.packages."purescript:exe:purs";
};

apps = {
purs.program = "${self'.packages.purs}/bin/purs";
};
};
}
Loading
Loading