Split records of TauT and RhoT #388

matil019 · 2019-11-20T05:47:48Z

Part of #382, continuation of #384

This PR refacters the internal of the compiler so that the two types, TauT and RhoT no longer are simultaneously sum types and record types.

I tried as much as possible for each commit to have API change of one function, so refer to the commit logs for the detailed changes. The following are the important changes.

A breaking change

There is a breaking change visible outside of the compiler.

Only type variables are accepted as generics parameters. The following code is no longer valid:

native emptyListFoo java.util.Collections.emptyList {[a]} :: () -> STMutable s (List [a])

(the {[a]} is the offending part.) It had been an unintended use of generics parameters. This change was introduced to refine the type of the grammar gargs (see below).

Main changes

TauT

TauT.TCon and .TVar were split into independent data types: TCon and TVar, respectively.
The type of SigmaT.vars was changed from [Tau] to [TVar QName].
The types of SymT.gargs SymV.gargs and SymA.vars was changed from [Tau] to [TVar QName].
SymC.tau :: Tau was changed to SymC.clvar :: TVar QName.

RhoT

TauT.RhoTau and .RhoFun were split into dependent data types.

Grammar (Frege.y)

The type of gargs was changed from [TauS] to [TVar SName].
The types of tyvar, dvars, nativespec and methodspec were changed similarly.
A new grammar gargvars :: [TVar SName] was added.

New errors

Internal errors

The following are internal errors. I doubt any of them actually occurs unless something goes very wrong.

frege.compiler.gen.java.InstanceCode.symItau :: SymI a -> RhoTau QName is a new function that tries to extract RhoTau QName from SymI.typ.
frege.compiler.passes.Imp: a new local function nTVar was added. It is a partial function that tries to extract TVar QName from a TauA annotation. As long as annotations are kept intact, it succeeds.

Performance concerns

fregec

The performance of the compiler was tested by compiling the source at master with different versions of fregec.jar.

The command make clean compiler1 was run 15 times each.

branch	commit id	average secs	%
master	`a3c4f77`	78.583	100
no-sum-symbolt	`11bdb3f`	81.900	104.2
(refactor TauT)	`f688cda`	81.908	104.2
no-sum-rhot	`0d51a6c`	82.024	104.3

fregedoc

TODO

frege IDE

Not tested because I don't have an IDE but the same performance drop as fregedoc is expected.

This is needed by the lenses to be added later.

See frege/compiler/types/Symbols.fr As a first step to decomposing the sum-record SymbolT, SymT was isolated to an independent data type. Some parts of code were deliberately rewritten into refutable case analyses so that compiler warnings are triggered.

The field accessors of SymbolT were replaced with lenses. Partial functions were deliberately introduced to trigger compilation warnings where certain constructor is implicitly assumed (for example, an unsafe conversion `SymbolT g -> SymD g` is inserted to a piece of code which accesses `flds`, which exists only on `SymD`.)

Lots of redundant unsafeToSymVs and its friends were removed.

by tightening the types of parameters

- removed redundant pattern from `sref` - changed the type of `overSig` to take `SymV Global`

By changing the type of the local function `rbSymT` to return `SymT`

by tightening the parameter types

by tightening the types of parameters

by tightening the parameters

allvars was changed from monadic value to a plain function because it doesn't change nay state. Some functions in other modules had their parameters tightened.

For consistency with NatDcl.gargs

nTVar is a new partial function that pattern matches the return value of nTau and throws an error against non-TVars. Unless annotations are corrupted, it should not encounter an error.

Now all of the unsafe functions (partial matches) are no longer used, they were removed.

In the original implementation, it always returned 'false' if one of its argument was 'Meta'. The all use-sites of 'Methods.matches' were checked to make sure no 'Meta's are passed to it. Now the function is an alias of 'TauT.textualEq', which does compare two 'Meta' for textual equality.

The original function was renamed to tcTau for the sake of (use-site) abbreviation

Now all of the unsafe functions (partial matches) are no longer used, they were removed.

I added them because I thought they would be useful, but they weren't.

Without changing any "public" api. Added lenses and unsafe accessors. The uses of the latter will be removed in following commits.

The pattern matching becomes partial. Perhaps the return type has to be reverted to Rho but the fact that a lot of use-sites assume that the return value is RhoTau.

It's unused. Uses of unsafe functions in unifyRho were removed.

It's unused.

It's unused. Actually, sigmaInst itself is unused.

Changes in this commit affect the internals of functions or the parameters of private functions only.

The error case occurs when a data constructor is not a RhoFun i.e. has no parameter. It should never happen because matchNew is supposed to handle newtypes only.

@maybe

Ignoring pattern match failure cannot be justified because otherwise higher order functions with possibly Rank-N types will be corrupted. I think the new return type @maybe (RhoTau QName)@ is more descriptive than the original @rho@ in case of pattern match failure. Some error cases were restored. A couple of partial cases were added.

A new partial case was introduced to frege.ide.Utilities.label, but I believe it never happen because SymI.typ is not really a Sigma but a pair of [Context] and Tau. I expect the partial case will be eliminated in my upcoming work for MultiParamTypeClasses.

All of ide.Utilities, tools.doc.Utilities, and compiler.gen.java.InstanceCode rely on the same (type-unsafe) invariant, so it was extracted as a new function. Note that the function is intended to be a a temporary measure until I implement MultiParamTypeClasses and perform a required refactoring in which SymI.typ will be broken down into ctxs :: [Context] and tau :: Tau.

To avoid unnecesary performance drop. Indeed, this commit appears to eliminate the drop introduced by this branch.

@foo

Since the record update syntax @foo.{bar <- f, baz <- g, ...}@ is desugered into individual updates @foo.{bar <- f}.{baz <- g,}...@, it may be a performance loss, as it was in using lenses.

Because it was trivial to do so.

Removed unwanted diffs introduced by a series of modifications

matil019 added 30 commits October 21, 2019 13:01

Split constructors of DefinitionS to individual data types

c5fd565

Add instance Alt Maybe

f577108

This is needed by the lenses to be added later.

[nocompile] Change all of SymbolT constructors to independent types

73d651a

Add instance Nice for SymT, SymL, etc.

e9fd748

Modify findV to return SymV, same for other Sym?s

1b872dc

Lots of redundant unsafeToSymVs and its friends were removed.

Change the return type of patLocal, mkLocal, vSym to SymV

7803c9e

Remuve uses of unsafePartialView from frege.compiler.Kinds

5a0459a

by tightening the types of parameters

Reduce warnings on frege.tools.doc.Utilities

f83552d

- removed redundant pattern from `sref` - changed the type of `overSig` to take `SymV Global`

Remove uses of unsafePartialView from frege.compiler.passes.Imp

8c03d3f

By changing the type of the local function `rbSymT` to return `SymT`

Reduce uses of partial functions in frege.ide.Utilities

596b2e0

Remove redundant cases in frege.compiler.gen.java.Common

a4cb129

Change the return type of envConstructors to [SymD Global]

d9c176b

Remove uses of partial functions in frege.compiler.passes.Instances

d8ce200

by tightening the parameter types

Remove some of partial functions in frege.compiler.Classes

6f2e5a4

by tightening the types of parameters

Remove a dead case in frege.compiler.gen.java.InstanceCode

efac3c0

Remove a dead case in frege.compiler.gen.java.DataCode

727656c

Remove some partial functions and dead cases in frege.c.g.j.VarCode

9caad72

Remove partial functions in frege.compiler.gen.java.Match

81e2594

by tightening the parameters

Change the return type of allourvars and allvars to [SymV Global]

56e7ac8

allvars was changed from monadic value to a plain function because it doesn't change nay state. Some functions in other modules had their parameters tightened.

Change fundep to take SymV

fb417c4

Change ccSym to take SymV

f0b8d1c

Change the type of Global.locals to TreeMap Int (SymV Global)

8bef123

Remove some partial functions in frege.compiler.passes.Transdef

7809062

Add instance Ord for SymT, SymL, etc.

daf9a49

Remove dead cases and partial functions from f.c.passes.LetUnroll

a316f7a

Remove some partial functions and dead cases in frege.compiler.Typecheck

2c7fad5

Remove partial functions in frege.compiler.GenMeta

81a68d2

Remove unused imports

d1cbfc0

matil019 added 30 commits November 7, 2019 10:09

Change SymV.gargs :: [Tau] to [TVar QName]

50c7630

For consistency with NatDcl.gargs

Replace uses of unsafePartialView in Imp with a custom function nTVar

dd8647c

nTVar is a new partial function that pattern matches the return value of nTau and throws an error against non-TVars. Unless annotations are corrupted, it should not encounter an error.

Remove "unsafe" functions which were meant to be used temporarily

9a4e5fc

Now all of the unsafe functions (partial matches) are no longer used, they were removed.

Add TauT.traverseApp, a generalization of traversal over TauT

89f69c8

Add TauT.headTCon

fe86bba

Split TauT.TCon to its own data type

8c7522a

Change Typecheck.tc to return TCon QName

500627e

The original function was renamed to tcTau for the sake of (use-site) abbreviation

Add tnameInt, tnameLong, etc. to remove uses of partial functions

a0f0791

Remove "unsafe" functions which were meant to be used temporarily

4279cb5

Now all of the unsafe functions (partial matches) are no longer used, they were removed.

Remove TauT.traverseApp, traverseTVar and headTCon

f688cda

I added them because I thought they would be useful, but they weren't.

Split constructors of RhoT to individual data types

1e77d7f

Without changing any "public" api. Added lenses and unsafe accessors. The uses of the latter will be removed in following commits.

Change tauRho to return RhoTau

1cc9149

The pattern matching becomes partial. Perhaps the return type has to be reverted to Rho but the fact that a lot of use-sites assume that the return value is RhoTau.

Remove Global from unifyRho's parameters

57c7259

It's unused. Uses of unsafe functions in unifyRho were removed.

Remove Global from unifySigma's parameters

73e2699

It's unused.

Remove Global from sigmaInst's parameters

ce72c8c

It's unused. Actually, sigmaInst itself is unused.

Extract common local function as zapCtx

2db83f7

Remove uses of the partial functions (local changes only)

47e22b8

Changes in this commit affect the internals of functions or the parameters of private functions only.

Remove a use of unsafe function in match.matchNew

41364a5

The error case occurs when a data constructor is not a RhoFun i.e. has no parameter. It should never happen because matchNew is supposed to handle newtypes only.

Remove partial functions meant for temporary use

fe293ab

Add instance Nice (RhoTau t) and (RhoFun t)

7b31ce4

Remove unneeded TODO comments

bf15e66

Remove uses of unnecessary lenses

8902a85

To avoid unnecesary performance drop. Indeed, this commit appears to eliminate the drop introduced by this branch.

Reduce another use of lenses

094b507

Rewrite substRigidRho not to use the record update syntax

cce1b07

Since the record update syntax @foo.{bar <- f, baz <- g, ...}@ is desugered into individual updates @foo.{bar <- f}.{baz <- g,}...@, it may be a performance loss, as it was in using lenses.

Move the implementation of instance RhoT to its constructors

ec9b85a

Because it was trivial to do so.

Clean up the code

0d51a6c

Removed unwanted diffs introduced by a series of modifications

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Split records of TauT and RhoT #388

Split records of TauT and RhoT #388

matil019 commented Nov 20, 2019

Split records of TauT and RhoT #388

Are you sure you want to change the base?

Split records of TauT and RhoT #388

Conversation

matil019 commented Nov 20, 2019

A breaking change

Main changes

TauT

RhoT

Grammar (Frege.y)

New errors

Internal errors

Performance concerns

fregec

fregedoc

frege IDE