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

majestic: Type-checking improvements + unifying overload resolution + simple REPL #173

Open
wants to merge 8 commits into
base: majestic
Choose a base branch
from

Conversation

phantamanta44
Copy link

Brief summary of changes:

  • Registers alex and happy as Cabal build tools so cabal2nix can pick them up properly
  • Fixed crash when type-checking non-dependent products
  • Fixed builtins being called with free variables during type checking
  • Added variants of checkLType and inferLType that run inside EvalM (i.e. are not trapped inside a runEvalOneM)
  • Added a simple REPL executable (gfci) for working with the GF programming language
  • Allows overload resolution to match more than one overload (e.g. when applied to a term with unknown type as in \x -> foo x)
    • The unfoldings of the matching overloads are bundled into a variants expression which is typed with the unifier of all the overloads' RHS types

Supervised by @krangelov

Copy link
Member

@krangelov krangelov left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The line:

when (bt == Implicit)

should be:

unless (bt == Implicit)

also in tcApp it would be cleaner to just collect the arguments without pattern matching on ImplArg. After that in reapply you can check for ImplArg instead of pattern matching on the booleans.

@phantamanta44
Copy link
Author

After thinking about it a bit more, I think it might make more sense to revert the open term check and to let the builtins themselves handle their args however they want. One could imagine, for example, a builtin that doesn't want to force all of its args immediately---this would not work with the current implementation, since we need to force the arg thunks to check for free variables. The idea, then, would be to instead offer a library of combinators that give pre-defined common behaviours for builtins; for example, the open term check might be handled by a combinator:

closedArgs :: GlobalDef -> GlobalDef
closedArgs f args = do
  open <- anyM isOpen args
  if open then return RunTime else f args

A similar combinator could also be used to address the partial application issue we discussed earlier by refusing to evaluate until enough args are provided:

withArity :: Int -> GlobalDef -> GlobalDef
withArity n f args = if length args < n then return RunTime else f args

There's also the possibility of wrapping the builtin functions in a newtype, like so:

newtype GlobalDef = GlobalDef { evalDef :: forall s. [Value s] -> EvalM s (ConstValue (Value s)) }

This would discourage API consumers from accidentally passing an "unsafe" raw function, but it has the unfortunate side effect of breaking any existing builtin implementations.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants