Sean/typed core fn #20
Open
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
…HaP, added basic nix shell with build deps & locale config, placeholder UPLC codegen module & functions. You almost certainly need the hie.yaml and .envrc to work on this so I committed those intentionally.
…n the annotation) + reworked pretty printer to... print prettily
… this as a temporary work branch)
…e expressions, necessary for fully typing the desugared typeclass declarations
…gly CoreFn desugaring code
…s-wip Sean/typed core fn.typeclasses wip
…Unknowns, small tweak to pretty printer
Sean/typed core fn.wip
klntsky
reviewed
Feb 1, 2024
| type M m = (MonadSupply m, MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m) | ||
|
|
||
| -- | Traverse a literal. Note that literals are usually have a type like `Literal (Expr a)`. That is: The `a` isn't typically an annotation, it's an expression type | ||
| traverseLit :: forall m a b. Monad m => (a -> m b) -> Literal a -> m (Literal b) |
| import Control.Monad.IO.Class (MonadIO (liftIO)) | ||
|
|
||
| import Language.PureScript.AST qualified as AST | ||
| import Language.PureScript.CoreFn (Ann, Module(..), Expr(..), Literal(..), Meta) |
There was a problem hiding this comment.
Please use explicit exports/imports, as suggested by https://github.com/mlabs-haskell/styleguide?tab=readme-ov-file#modules
…instantiatePolyTypes
Too many of them to fix now
…g dictionary types, (sort of) fixed let-generalization, ported over more tests
…inery. (We're now properly *reconstructing* the types)
Too many of them to fix now
Sean/typed core fn.test infra
Set up Nix CI
klntsky
reviewed
Mar 8, 2024
| inferExprTypes = \case | ||
| _ -> undefined | ||
|
|
||
| {-| nil = constr 0 [] |
There was a problem hiding this comment.
Please, if you leave any commented-out code, describe how it can be useful/illustrative for the readers (if it can't, please remove).
| are qualified by their ModuleName. What we do here is first look for a "local" type for the identifier using the provided source position, | ||
| then, if that fails, look up the identifier in the "global" scope using a module name. | ||
|
|
||
| I *think* this is fine but I'm not *certain*. |
There was a problem hiding this comment.
If you can't name a single reason why it may not work, it's better to omit comments about uncertainty, because it is implied anyway - everywhere in our industry. If you have known concerns, please write them down.
|
|
||
| {- Converts declarations from their AST to CoreFn representation, deducing types when possible & inferring them when not possible. | ||
|
|
||
| TODO: The module name can be retrieved from the monadic context and doesn't need to be passed around |
| bindLocalVariables [(ss,name,valDeclTy,nv)] $ do | ||
| expr <- exprToCoreFn mn ss (Just valDeclTy) e -- maybe wrong? might need to bind something here? | ||
| pure [NonRec (ssA ss) name expr] | ||
| -- Recursive binding groups. This is tricky. Calling `typedOf` saves us a lot of work, but it's hard to tell whether that's 100% safe here |
There was a problem hiding this comment.
Do you have any specific concerns about the correctness here?
| -- NOTE: This should be OK because you can data declarations can only appear at the top-level. | ||
| declToCoreFn mn (A.DataBindingGroupDeclaration ds) = wrapTrace "declToCoreFn DATA GROUP DECL" $ concat <$> traverse (declToCoreFn mn) ds | ||
| -- Essentially a wrapper over `exprToCoreFn`. Not 100% sure if binding the type of the declaration is necessary here? | ||
| -- NOTE: Should be impossible to have a guarded expr here, make it an error |
There was a problem hiding this comment.
This should've been a TODO, right? Please address it as well
| -> m (CaseAlternative Ann) | ||
| altToCoreFn mn ss ret boundTypes (A.CaseAlternative bs vs) = wrapTrace "altToCoreFn" $ do | ||
| env <- gets checkEnv | ||
| bTypes <- M.unions <$> zipWithM inferBinder' boundTypes bs -- Inferring the types for binders requires some special machinery & knowledge of the scrutinee type. NOTE: Not sure why multiple binders? |
There was a problem hiding this comment.
Not sure why multiple binders?
Maybe due to case a, b, c of syntax (which is not tuple construction)
| $ "untyped binding group element in mutually recursive LET binding group after initial typechecker pass: \n" | ||
| <> LT.unpack (pShow $ lefts types) | ||
| where | ||
| go :: ((SourceAnn, Ident), A.Expr) -> Either ((SourceAnn,Ident), A.Expr) ((SourceAnn, Ident), (A.Expr, SourceType)) |
There was a problem hiding this comment.
(SourceAnn,Ident) is present in both alternatives. Consider moving it out of Either
| guardToExpr [A.ConditionGuard cond] = cond | ||
| guardToExpr _ = internalError "Guard not correctly desugared" | ||
|
|
||
| {- Dirty hacks. If something breaks, odds are pretty good that it has something do with something here. |
There was a problem hiding this comment.
Suggested change
| {- Dirty hacks. If something breaks, odds are pretty good that it has something do with something here. | |
| {- Dirty hacks. If something breaks, odds are pretty good that it has something to do with something here. |
|
|
||
|
|
||
|
|
||
| {- "Type Constructor analysis" machinery. (This requires some explaining) |
Comment on lines
+218
to
+219
| in error $ "Internal error. Expected a function type, but got: " <> showty | ||
| {- This function more-or-less contains our strategy for handling polytypes (quantified or constrained types). It returns a tuple T such that: |
There was a problem hiding this comment.
Suggested change
| in error $ "Internal error. Expected a function type, but got: " <> showty | |
| {- This function more-or-less contains our strategy for handling polytypes (quantified or constrained types). It returns a tuple T such that: | |
| in error $ "Internal error. Expected a function type, but got: " <> showty | |
| {- This function more-or-less contains our strategy for handling polytypes (quantified or constrained types). It returns a tuple T such that: |
klntsky
reviewed
Mar 8, 2024
|
|
||
| deriving instance Eq a => Eq (Module a) | ||
|
|
||
| data DiffResult a = |
There was a problem hiding this comment.
Could you please explain the purpose of this module within the larger context
| | C.I_functionApply <- fn -> App a x y | ||
| | C.I_functionApplyFlipped <- fn -> App a y x | ||
| (App a t1 (App _ t2 (Var _ t3 fn) x) y) | ||
| | C.I_functionApply <- fn -> App a t1 x y -- NOTE @klntsky not sure about the type here, needs reviewed. I *think* the type shouldn't change? |
There was a problem hiding this comment.
I agree, please remove the comment
| prettyTypeStr = T.unpack . smartRender . asOneLine prettyType | ||
|
|
||
|
|
||
| {- TYPES (move later) -} |
There was a problem hiding this comment.
Suggested change
| {- TYPES (move later) -} | |
| {- TOD: TYPES (move later) -} |
| @@ -122,12 +122,14 @@ updateCacheDb codegenTargets outputDirectory file actualFile moduleName = do | |||
| let moduleCacheInfo = (normaliseForCache cwd (fromMaybe file actualFile), (dayZero, contentHash)) | |||
|
|
|||
| foreignCacheInfo <- | |||
There was a problem hiding this comment.
Is there a todo to make this used? If not, please remove
Comment on lines
+123
to
+124
| -- pTrace regrouped | ||
| -- pTrace exps |
There was a problem hiding this comment.
Uncomment these and make traces visibility configurable by a global var or a flag
| @@ -75,7 +78,7 @@ convertPrettyPrintType = go | |||
| -- Guard the remaining "complex" type atoms on the current depth value. The | |||
| -- prior constructors can all be printed simply so it's not really helpful to | |||
| -- truncate them. | |||
| go d _ | d < 0 = PPTruncated | |||
| -- go d _ | d < 0 = PPTruncated | |||
There was a problem hiding this comment.
A bit more of these in this module
| => [SourceType] | ||
| -> SourceType | ||
| -> [CaseAlternative] | ||
| => [SourceType] -- the types of the scrutinee values |
There was a problem hiding this comment.
Use doc-comments
Suggested change
| => [SourceType] -- the types of the scrutinee values | |
| => [SourceType] -- ^ the types of the scrutinee values |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Description of the change
This is the up-to-date branch of our typed CoreFn conversion machinery. It should handle every language construct now, and appears to work for a nontrivial, but by no means exhaustive, set of examples
I still need to setup the scaffolding for a real test suite & implement most of the minor changes that came up during our live review session so this isn't really ready for final review, but I thought it'd be important to get it up before the meeting tomorrow.
Checklist: