Improve type class syntax #420

dougalm · 2021-01-04T21:04:36Z

Lightweight syntax for class constraints in functions and instances:

 def (/=) [Eq a] (x:a) (y:a) : Bool = not $ x == y`


 instance [Eq a, Eq b] Eq (a & b)
   (==) = \(x1,x2) (y1,y2). x1 == y1 && x2 == y2

Handle superclasses in interface decls:

interface [Eq a] Ord a
  (>) : a -> a -> Bool
  (<) : a -> a -> Bool

Remove the need to name instances explicitly
Push down types from interface definitions into instance methods, reducing the annotation burden for instance methods.
Improve error messages for missing/duplicated methods.
Infer types of implicit implicit args. (No more (n:Int) ?-> n=>a -> ...)

* Handle superclasses * Remove the need to name instances explicitly * Push down types from interface definitions into instance methods * Improve error messages for missing/duplicated methods As par of this change, I moved the lowering (turning interface/instance decls into data defs and method/super class getters) from the parser to type inference where we have much more context about existing definitions. Fixes #370.

I guess that makes them implicitly typed implicit implicit arguments.

oxinabox · 2021-01-04T21:38:19Z

Handle superclasses in interface decls:
Remove the need to name instances explicitly
Push down types from interface definitions into instance methods, reducing the annotation burden for instance methods.

I love this so much. This is great.

I had been playing around in my head with the opposite of the last point. What if we were to push specially marked types of methods upwards from methods to allow methods to define interfaces. Which I still think is a cute (albeit under-developed)
idea, but not longer feels anywhere as needful.
This is so nice

Remove the need to name instances explicitly

Does this outright remove the ability to name them? (I think it should, those names are not useful for anything?)
Cool side effect this is that it masssively cleans up the output of #407 which wass showing completions for several hunderen instance names.

apaszke

Looks nice! Some things that would be good to fix before merging.

Also, I'd appreciate a walk through the inference changes related to dictionary synthesis. It's been hard enough to understand without comments that I gave up for the sake of saving time.

apaszke · 2021-01-05T10:23:13Z

src/lib/Parser.hs

@@ -258,7 +258,7 @@ findImplicitImplicitArgNames typ = filter isLowerCaseName $ envNames $
    UFor _ _ _ -> error "Unexpected for in type annotation"
    UHole -> mempty
    UTypeAnn v ty -> findVarsInAppLHS v <> findVarsInAppLHS ty
-    UTabCon _ -> error "Unexpected table in type annotation"
+    UTabCon _ -> mempty


Why did that have to change? It looks wrong to me

This is reachable with a syntactically valid but ill-typed user program so it shouldn't cause a compiler crash. We could throw a parser error (and change the type of this function to allow that) but I think it's also fine to forget about the implicit args and catch the error during type inference.

Right. So the whole explanation sounds reasonable to me, but:

This should be explained in the comment

There are more error cases that we should fix

Also, do we really have a guarantee that there will be a type error if there's a UTabCon? At some point we might add another syntactic form that turns a UTabCon into a valid type, and then this function will silently compute the wrong thing.

Sure. I'll fix the rest of the function too.

lib/prelude.dx

apaszke · 2021-01-05T10:26:22Z

src/lib/PPrint.hs

-      _ -> error "Bad projection"
-
-  nosrc = WithSrc Nothing
-  uignore = nosrc $ UPatBinder $ Ignore ()


Why is this gone? This was pretty useful, since otherwise projections are super difficult to read.

I got rid of it because it was crashing the pretty-printer when I was trying to debug some ill-formed IR I was generating. As a debugging aid, we want the pretty printer to remain faithful to the underlying IR rather than trying to rewrite it. But I hadn't appreciated that this is user-facing too. I'll replace it with something more readable.

apaszke · 2021-01-05T10:27:16Z

src/lib/Syntax.hs

 withLabels :: LabeledItems a -> LabeledItems (Label, Int, a)
 withLabels (LabeledItems items) = LabeledItems $
  flip M.mapWithKey items $ \k xs -> fmap (\(i,a) -> (k,i,a)) (enumerate xs)

+lookupLabel :: LabeledItems a -> Label -> Maybe a
+lookupLabel (LabeledItems items) l = case M.lookup l items of


Rename to lookupLabelHead? It doesn't return all values for a given label

apaszke · 2021-01-05T10:27:30Z

src/lib/Syntax.hs

@@ -784,11 +798,15 @@ instance BindsUVars UPat' where
 instance HasUVars UDecl where
  freeUVars (ULet _ p expr) = freeUVars p <> freeUVars expr
  freeUVars (UData (UConDef _ bs) dataCons) = freeUVars $ Abs bs dataCons
+  freeUVars (UInterface _ _ _) = mempty  -- TODO
+  freeUVars (UInstance _ _) = mempty     -- TODO


Seems like something worth fixing before we merge this

This was worth doing! Implementing it made me realize I've been sloppy about the scope of the binders in the instance type. They're meant to be in scope in the method implementations, so they shouldn't be represented as alpha-renameable pi binders within the type. I'll push a separate fix.

apaszke · 2021-01-05T10:33:06Z

src/lib/Syntax.hs

+pattern ClassDictDef conName superclasses methods =
+  [DataConDef conName
+     (Nest (Ignore (RecordTy (NoExt superclasses)))
+     (Nest (Ignore (RecordTy (NoExt methods))) Empty))]


Shouldn't we use BinderAnn here, so that it becomes insensitive to whether the names are used or not? Or should we just maintain an invariant that we don't use any names in class definitions? But if we go with the latter case, why do we ever use BinderAnn -- let's just keep our conventions!

Changed to BinderAnn

apaszke · 2021-01-05T10:35:27Z

src/lib/Parser.hs

+    addImplicitArg :: Name -> (UType, UExpr) -> (UType, UExpr)
+    addImplicitArg v (ty, e) =
+      ( ns $ UPi (Just uPat, uTyKind) ImplicitArrow ty
+      , ns $ ULam (uPat, Just uTyKind) ImplicitArrow e)


We did have source info for those expressions before. Maybe consider keeping it?

The source info wasn't real though, so I think it's just as good to let the source context fall back to the next level up in the AST.

apaszke · 2021-01-05T10:36:20Z

src/lib/Syntax.hs

@@ -237,6 +249,8 @@ data UExpr' = UVar UVar
 data UConDef = UConDef Name (Nest UAnnBinder)  deriving (Show, Generic)
 data UDecl = ULet LetAnn UPatAnn UExpr
           | UData UConDef [UConDef]
+           | UInterface [UType] UConDef [UAnnBinder]
+           | UInstance UType [(UVar, UExpr)]


Can you please add some comments that explain what the different fields mean?

Yes, good idea

apaszke · 2021-01-05T10:39:24Z

src/lib/Embed.hs

+
+recGet :: Label -> Atom -> Atom
+recGet l x = do
+  let (RecordTy (Ext r _)) = getType x


Shouldn't you assert that this has NoExt? Otherwise there is no way to know if there won't be more instance of your label coming later? Also, this does retrieve only the first element under a given label, without any assertion that there are no more of those. Is that expected? If so, please reflect that in the name.

I'll rename to recGetHead. I think it's fine if there are more copies of the same label coming later.

apaszke · 2021-01-05T10:39:53Z

src/lib/Embed.hs

+buildImplicitNaryLam Empty body = body []
+buildImplicitNaryLam (Nest b bs) body =
+  buildLam b ImplicitArrow $ \x -> do
+    bs' <- substEmbed (b@>x) bs


nit: this is O(n^2). Would be better to carry the substitution in a recursive call, but no big deal I guess

Good catch. I think there are many places like this in the compiler. One day we'll need to do some profiling and fix the ones that matter the most. I'll leave this one for now.

dougalm · 2021-01-05T15:51:33Z

Does this outright remove the ability to name them? (I think it should, those names are not useful for anything?)

Yes, it does for now. We're conflicted about it though, because names could be useful when you want to specify a type class instance explicitly. For example, you might want to do a reduction with an alternative monoid instance for floats like max or min instead of the usual +. Adam has some cool stuff cooking on this front!

And fix type inference to handle them properly.

apaszke · 2021-01-06T10:53:06Z

src/lib/Syntax.hs

+   ULet LetAnn UPatAnn UExpr
+ | UData UConDef [UConDef]
+ | UInterface [UType] UConDef [UAnnBinder] -- superclasses, constructor, methods
+ | UInstance (Nest UPatAnnArrow) UType [UMethodDef]  -- args, type, methods


What are "args"? Is this a list of binders to prepend to each method definition?

dougalm added 5 commits December 31, 2020 17:28

Add new syntax for type class constraints on def decls. Fixes #370.

1f9b2ef

Enable BlockArguments by default (we use the bracketing pattern a lot)

b1a6596

Infer types of implicit implicit arguments.

e6855c7

I guess that makes them implicitly typed implicit implicit arguments.

Merge branch 'main' into typeclass-def-syntax

a5209ab

google-cla bot added the cla: yes label Jan 4, 2021

apaszke reviewed Jan 5, 2021

View reviewed changes

dougalm added 2 commits January 5, 2021 14:47

Make fixes suggested in review.

beabafb

Make scoping of binders in instance declarations more explicit.

ff91d2d

And fix type inference to handle them properly.

dougalm merged commit 8283de6 into main Jan 5, 2021

apaszke reviewed Jan 6, 2021

View reviewed changes

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Improve type class syntax #420

Improve type class syntax #420

dougalm commented Jan 4, 2021 •

edited

Loading

oxinabox commented Jan 4, 2021 •

edited

Loading

apaszke left a comment

apaszke Jan 5, 2021

dougalm Jan 5, 2021

apaszke Jan 5, 2021 •

edited

Loading

dougalm Jan 5, 2021

apaszke Jan 5, 2021

dougalm Jan 5, 2021

apaszke Jan 5, 2021

apaszke Jan 5, 2021

dougalm Jan 5, 2021

apaszke Jan 5, 2021

dougalm Jan 5, 2021

apaszke Jan 5, 2021

dougalm Jan 5, 2021

apaszke Jan 5, 2021

dougalm Jan 5, 2021

apaszke Jan 5, 2021

dougalm Jan 5, 2021

apaszke Jan 5, 2021

dougalm Jan 5, 2021

dougalm commented Jan 5, 2021

apaszke Jan 6, 2021

Improve type class syntax #420

Improve type class syntax #420

Conversation

dougalm commented Jan 4, 2021 • edited Loading

oxinabox commented Jan 4, 2021 • edited Loading

apaszke left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

apaszke Jan 5, 2021 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

dougalm commented Jan 5, 2021

Choose a reason for hiding this comment

dougalm commented Jan 4, 2021 •

edited

Loading

oxinabox commented Jan 4, 2021 •

edited

Loading

apaszke Jan 5, 2021 •

edited

Loading