Conversation
Since primitive constructors are hard-wired into the Expr type, they are always in scope. However, the corresponding primitive type definitions may not be in scope. Since we have a hard-wired map `primConName` that gives the type any PrimCon constructs we could infer a non-existant type for primitive constructors! Previously, we would infer a type of `Char` for `'a'`, even when the type `Char` did not exist in the current program, or even if it had been arbitrarily defined by the user. We now check that the type-name given by the hard-wired map exists in the current program, and is a primitive type. Note that this design relies on the fact that primitive types cannot be renamed.
Otherwise it will generate ill-typed terms in the empty context: it will generate primitve constructors but they are not considered to be in scope as their corresponding types are not.
When we successfully synthesise a type for some term, that type should kind-check at the kind KType. I.e. the types we synthesise are actually recognised as types by our kind checker.
We split the module in two, to enable creation of a Primer.Import module which depends on some basic definitions in Primer.App, but should provide a new handler for Primer.App to use. If we did not do this refactor, we would create a import cycle.
|
Reviewer notes: |
| -- Not allowed to both import and dep-rename some type | ||
| for_ (Map.intersection iacImportRenamingTypes iacDepsTypes) $ throwError' . ImportRenameType . fst |
There was a problem hiding this comment.
I could combine the maps and get this by construction, but think that is less ergonomic to use. Perhaps I should given that this is a low-level API which will be wrapped by simpler "import module A, noting that A depends on B which is already imported as C"
| _typeDefName :: Lens' TypeDef Name | ||
| _typeDefName = typeDefLens #primTypeDefName #astTypeDefName | ||
|
|
||
| typeDefName :: TypeDef -> Name | ||
| typeDefName = \case | ||
| TypeDefPrim t -> primTypeDefName t |
There was a problem hiding this comment.
Given that I am defining lenses for these anyway, perhaps I should re-define the current accessors to use the lens?
I have not done this, as I was a bit worried about performance of generic-lens. I wanted to test it with inspection-testing, but that is broken with haskell.nix. However, typing this comment gave me the impetus to just dump the core and eyeball it -- it looks like everything does optimise away as expected, but I am not sure whether it gets worker-wrapper transformed in exactly the same way as the manual definition.
If we aren't too worried about this issue (and I expect we are not), it is easy to refactor this.
There was a problem hiding this comment.
You know, this is a good point that we've lost track of — we had planned to write some benchmark tests so that we could start tracking regressions. Perhaps we should get that set up before we look into writing more lenses. (I'm in favor of that in general, BTW.)
There was a problem hiding this comment.
Or indeed, given that typeDefName would just be view _typeDefName, we might then be better off just inlining it.
Side note - in #143 we agreed:
Don't use leading underscores _ for lens names, unless it's necessary to avoid a name clash.
If we inline, we free up the name typeDefName for the lens.
| _defID :: Lens' Def ID | ||
| _defID = defLens #primDefID #astDefID |
There was a problem hiding this comment.
Same comment here about lenses as for types
| , iacImportRenamingTerms :: Map ID Name | ||
| , iacDepsTerms :: Map ID ID |
There was a problem hiding this comment.
Same comment here about combining the maps as for types
brprice
force-pushed
the
brprice/module-import
branch
2 times, most recently
from
2f88af4 to
14d603e
Compare
The reason that srcProg and primSrcProg have been put into an Applicative context is that later we will want to import terms, and to test we will define some terms in these programs. This will need a MonadFresh context. To avoid changing all use sites later, we will write it monadically now.
The point of this trivial rejigging is to set up for importing terms (which will change these fields's type), so that commit will be less cluttered.
Similarly to the previous commit, set up for tests of importing terms. We need to return the ID of the new definitions, but this requires lots of knock-on changes in the tests. We do those now rather than in the commit that adds the ability to import terms.
I.e. that they look through explicit mutual recursion. When implementing importing terms, I worried whether these combinators would recuse into branches of a case expression, as that requires going from an Expr to a CaseBranch back to an Expr, and we very much need to replace names inside branches. These functions do indeed recurse into and out of other mutually recursive types in this manner.
Since the left hand side of a pattern match (the "C" in
case x of
C -> e
) is a Name in a CaseBranch, rather than a Con, it was not being
updated.
Since we allow rewiring imported type dependencies to any compatible
existing type, with any compatible bijection of their constructors, we
need to handle the case where the constructors get reordered. This is
important since the typechecker enforces that the branches of a pattern
match are in the order that constructors are declared in the
corresponding type definition.
For example, if we imported and rewired the type
data T = A | B
to
data R = C | D
via A -> D and B -> C, then we would need to reorder the import of
case x of
A -> t
B -> some_other_rhs
to
case x of
C -> some_other_rhs
D -> t
(Note that much of this commit only changes indentation)
brprice
force-pushed
the
brprice/module-import
branch
from
55336ae to
ab3ad49
Compare
| RewriteCtorTgtNotExist Name Name | ||
| | -- | This type was referenced in the source, but we have neither imported it nor rewritten it | ||
| ReferencedTypeNotHandled Name | ||
| | -- | @RewrittenCtorTypeDiffers ty1 con1 ty2 con2@: we tried to rewrite @ty1@ into @ty2@, mapping @con1@ to @con2@, but their types do not match |
There was a problem hiding this comment.
I don't mind long lines and certainly don't subscribe to any kind of antiquated 80-column line limit, but this one and a few below are probably a bit much. Is there a way to enforce a reasonable limit in Fourmolu?
There was a problem hiding this comment.
These are timely: we should consider how these import failures should be represented in the UI. Using our current category 1-5 classification, would these be category 2 (action failure)?
To answer that we'll need to think about the import workflow and UI.
There was a problem hiding this comment.
Just curious: assuming that once we have a proper module system with namespaced imports, we remove the "import-via-copy" functionality implemented in this PR, how many of these import errors will remain?
There was a problem hiding this comment.
Is there a way to enforce a reasonable limit in Fourmolu?
There's an unmerged PR adding support. IIRC, it has some issues around idempotence, which I'm a little uncomfortable with.
I am actually hoping to spend some long-overdue time on Fourmolu this weekend. But then again, I thought that last weekend...
| deriving (FromJSON, ToJSON) via VJSON ImportError | ||
|
|
||
| -- | How to rename a type, and each of its ctors | ||
| type TypeImportDetails = Map Name (Name, Map Name Name) |
There was a problem hiding this comment.
Can this type renaming code be re-used in our upcoming editable types work?
| -- - It needs to be injective for the translation, as previously distinguished | ||
| -- cases are now identified | ||
| -- - It needs to be surjective for the translated match to be exhaustive) | ||
| -- |
There was a problem hiding this comment.
This is a helpful and informative comment, but perhaps it should be an internal comment not made visible to Haddock?
|
|
||
| -- | Test whether an term contains any holes | ||
| -- (empty or non-empty, or inside a type) | ||
| noHolesTm :: (Data a, Data b) => Expr' a b -> Bool |
There was a problem hiding this comment.
Hmm, this is an interesting consequence of our "every program is valid" approach, and raises a question that I think is truly unique to Primer. Do we support importing code that contains holes? Should we?
There was a problem hiding this comment.
My inclination is that we should. A student might, for example, want to run some code from their own partially-incomplete module, and it would be frustrating if that were artificially restricted.
Perhaps we could have some kind of warning against "publishing" (whatever that means) a module containing holes.
|
Thanks. I appreciate the very helpful organization of these successive commits, as it makes it much easier to review. Speaking of review, I'll defer to @georgefst on the technical bits. In addition to my localized comments above, I do have two more points:
|
|
I am slightly concerned about the overall approach. It feels like this would make it impossible to update a dependency. The first comment here mentions "tracking of where code originally came from" - it's not obvious to me how we get there from here. While I was writing this comment, @brprice has just said that he also has some concerns about the approach, so I'll hold off on reviewing further for now. |
3 participants
We introduce a way to import code from some other
App. This is essentially automated copy-and-paste. Currently there is no notion in primer of a "module", and no tracking of where code originally came from -- this is left as future work.