Add support for user defined kinds #2486

LiamGoodacre · 2016-12-17T23:43:20Z

Initial work towards #919

Kind declarations:

foreign import kind Nat

Import/export kinds:

module F (kind N) where
import B (kind N)

Use of kinds in various places (see example/passing/ForeignKind/Lib.purs):

foreign import data Zero :: Nat
foreign import data Succ :: Nat -> Nat
...

Should I also move Symbol to use the new KindConstructor?
There are probably a lot more tests I should add, but it's a start.
Any issues, things I've missed, etc?
Thanks 😄

LiamGoodacre · 2016-12-17T23:49:10Z

src/Language/PureScript/Ide/Externs.hs

@@ -95,6 +95,7 @@ convertDecl P.EDValue{..} = Just $ IdeDeclValue $
  IdeValue edValueName edValueType
 convertDecl P.EDClass{..} = Just (IdeDeclTypeClass edClassName)
 convertDecl P.EDInstance{} = Nothing
+convertDecl P.EDKind{} = Nothing


I wasn't sure what this was. I'll investigate further to see what actually needs doing here. I assume I'll need to add a new IdeDeclaration constructor.

@kritzcreek Can you comment?

If you wanted the custom Kinds to show up in completions you'd have to add a new IdeDeclaration constructor, yep. One question though: Do kinds live in their own name space as well? So can I have a kind, type and identifier with the same name? That would require some more changes to psc-ide.

Yes they have their own namespace. What kind of changes are required?

Add a dtor to IdeDeclaration in Ide.Types and fill in identifierFromIdeDeclaration and completionFromMatch in Ide.Util.

Oh sry I read that as though they didn't :D the changes required are in extractSpans in Ide.SourceFile where I used an Either to disambiguate names on the type and value level

rightfold · 2016-12-17T23:49:46Z

Should I also move Symbol to use the new KindConstructor?

I think putting it in Prim is less surprising when someone wants to shadow it, although this is a very specific use-case. It may also simplify some of the Kind case analysis in the compiler.

Any issues, things I've missed, etc?

Kind aliases? E.g. kind Type = *. Though that could be a different PR.

LiamGoodacre · 2016-12-17T23:53:01Z

src/Language/PureScript/Sugar/Names/Exports.hs

@@ -19,7 +19,7 @@ import Language.PureScript.AST
 import Language.PureScript.Crash
 import Language.PureScript.Errors
 import Language.PureScript.Names
-import Language.PureScript.Sugar.Names.Env


All the lines that have changed but don't look different in this file are line-ending changes.

LiamGoodacre · 2016-12-18T00:40:07Z

If I move Symbol to use KindConstructor, should I also add Ordering while I'm there and cancel #2484

paf31 · 2016-12-18T00:54:56Z

I think Symbol needs to be in Prim since there is built-in syntax which needs it, but Ordering can defined in a library (and if it can, I think it should be). Maybe something like purescript-typelevel-prelude?

paf31 · 2016-12-18T01:01:05Z

src/Language/PureScript/Kinds.hs

@@ -20,6 +22,8 @@ data Kind
  | FunKind Kind Kind
  -- | Type-level strings
  | Symbol
+  -- | A kind constructor
+  | KindConstructor (Qualified (ProperName 'KindName))


Could we just call this NamedKind or OtherKind? Constructor seems to imply that we can have kinds which take other kinds as arguments, which isn't true.

Thanks, I've gone with NamedKind.

paf31 · 2016-12-18T01:02:47Z

Looks great, thanks!

paf31 · 2016-12-18T01:03:34Z

One more thing you'll probably need to update is usedModules in ModuleDependencies.hs.

LiamGoodacre · 2016-12-18T01:36:05Z

@paf31 for updating usedModules it looks like a need to update everythingOnTypes to support traversing kind annotations, is that correct?

paf31 · 2016-12-18T01:39:34Z

Yes, that sounds right.

LiamGoodacre · 2016-12-18T02:05:41Z

Changing everythingOnTypes looks really annoying :P it is used everywhere - is it acceptable to instead write an accumKinds like we have accumTypes?

LiamGoodacre · 2016-12-18T02:18:20Z

Actually, changing everythingOnTypes wouldn't be enough anyway, it wouldn't pick up kinds in foreign data declarations - I think.

LiamGoodacre · 2016-12-18T02:51:20Z

Okay so I added accumKinds because kinds don't just appear in types, they appear in type class declarations, foreign data declarations, etc.

paf31 · 2016-12-18T03:44:29Z

Actually, having thought about this more, I'm not sure why usedModules does what it does now actually. @garyb shouldn't module sort-order be determined entirely by imports now?

(in which case there would be less work to do here, so you might want to hold off until this is clarified)

garyb · 2016-12-18T04:18:00Z

shouldn't module sort-order be determined entirely by imports now?

Yep, I mentioned this a while ago in another PR!

paf31 · 2016-12-18T04:22:54Z

Sorry :) So does that mean we can just get rid of usedModules apart from the ImportDeclaration bit then?

LiamGoodacre · 2016-12-18T10:46:59Z

Even if I don't change usedModules, the accumKinds function still looks useful to have?

rightfold · 2016-12-18T13:32:43Z

Are changes to psc-docs also necessary? E.g. https://github.com/purescript/purescript/blob/master/psc-docs/Tags.hs and Markdown generation.

LiamGoodacre · 2016-12-18T13:48:36Z

I think we need to add stuff to Interactive/Completion and Sugar/BindingGroups too.

LiamGoodacre · 2016-12-18T15:00:44Z

Unfortunately I can't build psci and psc-ide-server locally, so I'll have to depend on CI for that.

paf31 · 2016-12-18T16:58:08Z

Even if I don't change usedModules, the accumKinds function still looks useful to have?

Yes, I think so.

LiamGoodacre · 2016-12-18T23:33:07Z

src/Language/PureScript/Ide/Types.hs

+  = IdeNameValue Text
+  | IdeNameType Text
+  | IdeNameKind Text
+  deriving (Show, Eq, Ord)


@kritzcreek is this okay for replacing the use of Either Text Text that you mentioned?

Maybe replace Name with NS or Namespace but other than that looks great!

LiamGoodacre · 2016-12-19T00:00:08Z

Actually I don't think anything needs adding to Interactive/Completion, right?

LiamGoodacre · 2016-12-19T23:40:25Z

src/Language/PureScript/Sugar/BindingGroups.hs

@@ -73,6 +73,7 @@ createBindingGroups moduleName = mapM f <=< handleDecls
        valueVerts = map (\d -> (d, declIdent d, usedIdents moduleName d `intersect` allIdents)) values
    bindingGroupDecls <- parU (stronglyConnComp valueVerts) (toBindingGroup moduleName)
    return $ filter isImportDecl ds ++
+             filter isExternKindDecl ds ++


I'm slightly confused about this. Without adding in this filter, does that mean that the kind declarations disappear when creating binding groups? Also is this all that is needed here?

LiamGoodacre · 2016-12-20T03:54:49Z

Updated the ForeignKind test with a kinded type annotation and I see the following error:

  1) Passing examples 'ForeignKind.purs' should compile and run without error
       Error found:
       in module ForeignKinds.Lib
       at /Users/liamgoodacre/git/purescript/examples/passing/ForeignKind/Lib.purs line 25, column 1 - line 25, column 22

         Could not match kind

           Nat

         with kind

           Nat


       while checking the kind of Kinded Zero
       in type synonym N0

Something is wrong :P

paf31 · 2016-12-20T04:19:55Z

Did you update the unify function for kinds? It's in TypeChecker.Kinds.

LiamGoodacre · 2016-12-20T14:19:52Z

@paf31 yes I believe unifyKinds is fine, it looks like the problem is that the kind in a KindedType hasn't been fully qualified. E.g:

Qualified Nothing (ProperName "Nat")
Qualified (Just (ModuleName [ProperName "ForeignKinds", ProperName "Lib"])) (ProperName "Nat")

paf31 · 2016-12-22T20:41:47Z

Ideally not, but I don't think we should make a special case for the $PSCI module either. Really, this should take into account which modules are imported, but we have a separate issue for that already, so maybe we can handle it then.

paf31 · 2016-12-23T04:06:31Z

src/Language/PureScript/Kinds.hs

-  -- | Type-level strings
-  | Symbol
+  -- | A named kind
+  | NamedKind (Qualified (ProperName 'KindName))


I wonder if Star and Bang should be moved into Prim too?

Eventually, I would like Bang to be moved into purescript-eff, but in order to do that, we need to introduce a name for it other than ! (perhaps Effect?). So how about we move it into Prim now, allow both ! and Effect in the parser, and then move it out to purescript-eff in 0.11?

While we're at it, we can alias * as Type.

That sounds great, I should hopefully be able to get this done tonight/tomorrow.

In updating this I've found that I'd missed updating primImports in Sugar/Names/Env.hs.

LiamGoodacre · 2016-12-23T21:30:21Z

I removed the ShadowPrimKind test as it now fails due to #2499 since I added primKinds to primImports in Sugar/Names/Env.

paf31 · 2016-12-24T04:14:26Z

@LiamGoodacre Looks great, but could you please see if it's possible/simple to add documentation for the kinds in Prim now that @hdgarrood's PR #2494 has been merged?

Thanks!

hdgarrood · 2016-12-24T08:49:06Z

That will require changes to Language.PureScript.Docs.Types to add a new DeclarationInfo constructor for user defined kinds. As far as I can tell, I think that would be fairly straightforward.

LiamGoodacre · 2016-12-24T10:41:46Z

@hdgarrood I had already added a new ExternKindDeclaration constructor to DeclarationInfo, so I just needed to extend what you added in your PR.

How does the "Add docs for kinds in Prim" commit look? I haven't written that much for each one.

LiamGoodacre · 2016-12-24T10:49:25Z

I renamed lookupPrimKind to lookupPrimTypeKind as I thought it was slightly confusing as it is really "lookup this type to find its kind" - and originally I was going to add a lookupPrimKind for kinds - but I can change it back if you want.

hdgarrood · 2016-12-24T14:47:50Z

Oops :) What you've got there all looks great to me, I agree that the way that you've renamed lookupPrimKind is an improvement. 👍

paf31 · 2016-12-28T03:42:17Z

@LiamGoodacre Could you please rebase this?

paf31 · 2016-12-28T18:11:24Z

Thanks very much!

LiamGoodacre commented Dec 17, 2016

View reviewed changes

paf31 reviewed Dec 18, 2016

View reviewed changes

paf31 added the status: ready for review label Dec 18, 2016

LiamGoodacre commented Dec 18, 2016

View reviewed changes

LiamGoodacre commented Dec 19, 2016

View reviewed changes

LiamGoodacre changed the title ~~Add foreign import kind~~ Add support for user defined kinds Dec 20, 2016

LiamGoodacre mentioned this pull request Dec 20, 2016

Kinded types can cause instance solving to fail #2490

Closed

LiamGoodacre mentioned this pull request Dec 22, 2016

Add Type.Data.Ordering; Reexport Data.Symbols, Type.Equality purescript/purescript-typelevel-prelude#1

Merged

paf31 suggested changes Dec 23, 2016

View reviewed changes

paf31 approved these changes Dec 24, 2016

View reviewed changes

LiamGoodacre added 14 commits December 28, 2016 12:02

Add foreign import kind

a5b85f9

Make ForeignKind.Lib visible to example tests

5c30894

Rename to NamedKind, add kind traversal, update usedModules

ddf79cb

More kind updates

441b45d

Missing type declaration

40d4a49

Undo change to usedModules.

18673db

Use the name IdeDeclNamespace and IdeNSValue/etc

fc28e77

Add extern kind filter to binding groups

e2b86f7

Replace Symbol with use of NamedKind

2d5e4a2

Add test for shadowing kind + update foreign kind test

3ab30c1

Desugar kind in KindedType when desugaring names + pretty NamedKind

6a2f357

Add fail test for unifying custom kinds across modules

7e8c4c3

Move * and ! to Type and Effect, Remove ShadowPrimKind test

470be23

Add docs for kinds in Prim

7be9647

paf31 merged commit 144dd6f into purescript:master Dec 28, 2016

paf31 mentioned this pull request Dec 28, 2016

User-defined Kinds #919

Closed

LiamGoodacre deleted the feature/custom-kinds branch December 28, 2016 18:14

chexxor mentioned this pull request Feb 5, 2017

Add docs for user-defined kinds purescript/documentation#39

Open

Add support for user defined kinds #2486

Add support for user defined kinds #2486

Conversation

LiamGoodacre commented Dec 17, 2016 • 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

rightfold commented Dec 17, 2016 • edited Loading

Choose a reason for hiding this comment

LiamGoodacre commented Dec 18, 2016

paf31 commented Dec 18, 2016

Choose a reason for hiding this comment

Choose a reason for hiding this comment

paf31 commented Dec 18, 2016

paf31 commented Dec 18, 2016

LiamGoodacre commented Dec 18, 2016

paf31 commented Dec 18, 2016

LiamGoodacre commented Dec 18, 2016

LiamGoodacre commented Dec 18, 2016

LiamGoodacre commented Dec 18, 2016

paf31 commented Dec 18, 2016

garyb commented Dec 18, 2016

paf31 commented Dec 18, 2016

LiamGoodacre commented Dec 18, 2016

rightfold commented Dec 18, 2016 • edited Loading

LiamGoodacre commented Dec 18, 2016

LiamGoodacre commented Dec 18, 2016

paf31 commented Dec 18, 2016

Choose a reason for hiding this comment

Choose a reason for hiding this comment

LiamGoodacre commented Dec 19, 2016

Choose a reason for hiding this comment

Choose a reason for hiding this comment

LiamGoodacre commented Dec 20, 2016

paf31 commented Dec 20, 2016 • edited Loading

LiamGoodacre commented Dec 20, 2016

paf31 commented Dec 22, 2016

paf31 Dec 23, 2016 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

LiamGoodacre commented Dec 23, 2016

paf31 commented Dec 24, 2016

hdgarrood commented Dec 24, 2016

LiamGoodacre commented Dec 24, 2016

LiamGoodacre commented Dec 24, 2016

hdgarrood commented Dec 24, 2016

paf31 commented Dec 28, 2016

paf31 commented Dec 28, 2016

LiamGoodacre commented Dec 17, 2016 •

edited

Loading

rightfold commented Dec 17, 2016 •

edited

Loading

rightfold commented Dec 18, 2016 •

edited

Loading

paf31 commented Dec 20, 2016 •

edited

Loading

paf31 Dec 23, 2016 •

edited

Loading