Explain rows in typeclass instances #104

chexxor · 2017-07-12T21:11:57Z

The other day I received an explanation of records and rows in typeclass instances. I'd like to have this clearly explained in one place, so here's my attempt at that. It needs fact-checking.

Also, this doesn't incorporate RowList representation of a Row, which can be used to overcome this limitation of rows in instances. I don't know how that relates to this explanation.

hdgarrood · 2017-07-12T21:32:22Z

I don't know how to answer this either, but there are a couple of things about that that don't quite seem right to me.

Firstly, you start by saying that rows cannot appear in instance heads, but then none of your examples actually show an attempt to define an instance with a row in the instance head, which I think is a bit confusing. Is there more to the restrictions on rows in instances than just this?

Then, your last paragraph which seems to be the 'why' that we've been building up to is a little unsatisfying. You say

to avoid orphan instances, its instance of a class would need to be defined in the same module as the typeclass

I think this is true but irrelevant. Even if I do attempt to define such an instance in the same module as the class it still doesn't work:

module Main where
class C a
instance a :: C ()

which fails with "Type class instance head is invalid due to use of type () "

and then,

Typeclasses like Ord and Semigroup can't have an instance for every specific row that people want to use - it's untenable.

I think it's better to say that Ord and Semigroup can't have instances for row types because it would be a kind mismatch; if you want an instance Ord A for a type A, the kind of A has to be Type. But also, I think it's safe to assume that nobody is trying to use Ord or Semigroup instances for rows, because why would they? and so, why mention this at all?

Finally, just saying "it's untenable" is not really an explanation at all; I think this needs to either be expanded or removed.

hdgarrood · 2017-07-12T21:34:17Z

Unfortunately I don't know how to address these things 😅 we'll have to wait for someone else to weigh in I think (perhaps @LiamGoodacre, @paf31, or @garyb?)

chexxor · 2017-07-12T21:52:15Z

Yeah, the "why" is still a bit unclear to me. Rather than having nothing for that, though, I thought it better to make a poor guess to encourage the answer to appear from reviewers. 😅 I think that answer is in the right ballpark, but it's poorly explained/justified.

I need to find better examples, yeah, and actually test them. The point of this entire section wasn't entirely clear, and good examples would support the point. Your idea is pretty good - I'll put that in there first, then do the Record stuff after.

Another question this could answer - do Kinds of types restrict their instances? Another thing to test before adding in there. # Type is its own kind, which might be the presumed reason it can't be an instance.

hdgarrood · 2017-07-12T22:00:21Z

Yes, I'm pretty certain that all type class parameters are restricted to a single kind. You can write e.g.

class A (t :: Type -> Type)

to say that the parameter of A has kind Type -> Type, and then the compiler will prevent you from trying to declare e.g. instance aInt :: A Int; you'll get "could not match kind Type -> Type with kind Type". If you leave off a kind annotation the compiler will assume you mean Type. The kinds of type class parameters can also be inferred based on the methods, see e.g. Functor: https://github.com/purescript/purescript-prelude/blob/3d4380c75060b6b80466c8628e9d895ee1e8c5d1/src/Data/Functor.purs#L24

hdgarrood · 2017-07-12T22:04:27Z

So I should clarify: if you write class A a, and there's no additional information for inferring the kind of a (e.g. methods whose types mention a) then the compiler will assume the kind Type. Otherwise, the compiler infers the kind of a.

hdgarrood · 2017-07-12T22:18:40Z

Also I just checked and

class A (a :: # Type)
instance inst :: A r

is fine. Note that r has kind # Type here so it is a row type. It seems like it's only when you start trying to restrict what kinds of rows you have in the instance declaration that it becomes an error; i.e. using something like () or (foo :: Int) or (foo :: Int | r).

chexxor · 2017-07-12T22:27:54Z

I've added a section on Kinds - can split it into a separate PR if desired. I haven't tested the claims it makes - can do later, after we settle on points to make.

Nice find, @hdgarrood - I've updated to remove statements saying rows aren't allowed - it's only concrete rows.

hdgarrood

I've made some more comments but before you go off and fix these let's wait for someone who knows more about this to weigh in; we might not really be looking at this from the right direction I think.

hdgarrood · 2017-07-12T22:28:55Z

language/Type-Classes.md

+-- `e` is kind `# Type`
+```
+
+If a typeclass's parameter's Kind is `Type`, an instance cannot be made for a type of kind `# Type` or `Type -> Type`.


This sounds like there's special casing going on but I don't think there is. I think you should just say something like "the kinds of any types mentioned in an instance declaration must match the kinds of those parameters as determined by the class's definition".

hdgarrood · 2017-07-12T22:29:11Z

language/Type-Classes.md

@@ -80,27 +80,50 @@ In fact, a type similar to this `AddInt` is provided in `Data.Monoid.Additive`,

 For multi-parameter type classes, the orphan instance check requires that the instance is either in the same module as the class, or the same module as at least one of the types occurring in the instance. (TODO: example)

+## Kinds
+
+A typeclass's parameter can specify the Kind. If it doesn't specify the type's Kind, it can be inferred by methods in the class.


I think it would be better style to use a lowercase 'k' for kind.

hdgarrood · 2017-07-12T22:29:54Z

language/Type-Classes.md

+
+``` purescript
+class A a
+-- `a` is kind `Type`


How about "without a kind signature, a defaults to kind Type"? and similar explanations for the other examples?

hdgarrood · 2017-07-12T22:31:13Z

language/Type-Classes.md

 instance mClosedRow :: M ()
+class M' (t :: # Type)


No need to define two different classes in this example; just put the kind signature on M I think.

chexxor · 2017-07-17T17:48:41Z

I saw @LiamGoodacre added a thumbs-up to agree with your explanation about the relationship between typeclass parameter kinds and kinds of instance datatypes. I've updated the docs to improve and clarify this section. Should fact-check/review the "An effect of adjusting the arity of kinds..." paragraph there.

We still need a better paragraph to explain why specific Rows aren't allowed in instances. I'd like it to be a technical or philosophical explanation. My test of using a specific row () in an instance declaration PS 0.11.5 just now produced the following error, which doesn't help with our explaining it, nor is it very satisfying.

Type class instance head is invalid due to use of type
      
    ()
      
  All types appearing in instance declarations must be of the form T a_1 .. a_n, where each type a_i is of the same form, unless the type is fully determined by other type class arguments via functional dependencies.

hdgarrood · 2017-07-17T18:14:24Z

I guess it must be because it would complicate solving too much. For example, what should the compiler do with the following? (assuming the proxy syntax which isn't in master just yet)

class Awesome (a :: # Type) where
  awesomeness :: @ a -> Int

instance awesomeFoo :: Awesome (foo :: Int | e) where
  awesomeness _ = 0

instance awesomeBar :: Awesome (bar :: Int | e) where
  awesomeness _ = 1

-- should this log "0" or "1"?
main = logShow $ awesomeness (@ (foo :: Int, bar :: Int))

LiamGoodacre · 2017-07-18T19:58:14Z

language/Type-Classes.md

@@ -80,6 +80,69 @@ In fact, a type similar to this `AddInt` is provided in `Data.Monoid.Additive`,

 For multi-parameter type classes, the orphan instance check requires that the instance is either in the same module as the class, or the same module as at least one of the types occurring in the instance. (TODO: example)

+## Kinds
+
+A typeclass's type parameter can specify the kind of types it applies to. If it doesn't specify the type's kind, it can be inferred by the typeclass's methods.


We usually refer to type class by two words.

How does this sound?
"Type class parameters do not need to be of kind Type. To explicitly specify a different kind, the parameter can be annotated with a kind signature. Unless the kind of a type parameter is explicitly annotated, it will be implicitly inferred based on how the type parameter is referred to by the type class's method signatures."

That's a lot more clear. I'll add that.

I was also curious about "typeclass" and "type class". I'll update this document to use "type class" if @hdgarrood agrees.

"type class" is fine, yeah. Currently there are 49 occurrences of that and only 3 of "typeclass" in this repo so let's stick with "type class".

LiamGoodacre · 2017-07-18T20:00:14Z

language/Type-Classes.md

+
+Instance selection works by looking at the "head" types of each type class parameter. Functional dependencies also plays a role, but we'll not consider that for now to simplify the explanation. The "head" of a type is the top-most type constructor, for example the head of `Array Int` is `Array` and the head of `Record r` is `Record`.
+
+As rows and records can easily be conflated to refer to the same thing, their difference is important to note here. `Record` is a simple type constructor in PureScript and therefore can be a head in an instance.


I don't think the word simple fits in here.

Yeah, that's true. 👍

LiamGoodacre · 2017-07-18T20:02:52Z

language/Type-Classes.md

+
+## Rows
+
+Concrete Row literals cannot appear in instances.


Unless the parameter is fully determined by functional dependencies.

Can you share some example of this? If using functional dependencies, you won't be using a row literal, will you? Isn't functional dependencies about declaring how type variables relate to other type variables? If so, you won't be relating to a row literal. Unless... you mean constraints like SubRow r (x :: Int, y :: Boolean)?

For example: http://try.purescript.org/?gist=b76f79d22a28a0e31ec5577504672db8&backend=core

class Ctors dt (ct :: # Type) | dt -> ct data X = X0 Int | X1 String instance ctorsX :: Ctors X ("X0" :: Int, "X1" :: String) data Y = Y0 Boolean instance ctorsY :: Ctors Y ("Y0" :: Boolean)

chexxor · 2017-07-18T20:33:37Z

I don't see how explaining instance selection in the Rows section is relevant. The problem with rows in instances is not about being in head position - it's about row literals. Yeah? I'd like to remove this explanation, or move it to a different place, unless it more directly explains the rows-in-instances conflict.

chexxor · 2017-07-18T21:07:39Z

I moved the instance selection explanation to its own section in this document.

hdgarrood · 2017-07-18T21:38:32Z

language/Type-Classes.md

+`instance functorEither :: Functor (Either e) where ...`
+```
+
+An effect of needing to adjust the kind of a data type to fit into a type class which applies to a lower arity kind, like with `Functor` and `Either` above, is that the behavior and laws of an instance will bias towards to the right-most type parameters.


I'm not sure about this sentence; I think it will only make sense to people who already understand what it's trying to explain. This topic is definitely worth addressing but I think we should do that separately from this PR.

hdgarrood · 2017-07-18T21:39:26Z

language/Type-Classes.md

+
+## Rows
+
+Concrete Row literals cannot appear in instances unless it's concrete type is fully determined by functional dependencies.


I think it's not quite clear what "it's" refers to here. Also "it's" means "it is"; for something belonging to "it" you should use "its".

hdgarrood · 2017-07-18T21:46:21Z

language/Type-Classes.md

+-- Prints the following when executed.
+this is a record
+this is an array
+```


I don't think this is right. For instance:

module Main where import Prelude import Data.Foldable (fold) import TryPureScript main = render $ fold $ [ p $ text $ describe [1, 2, 3] , p $ text $ describe [1.0, 2.0, 3.0] ] class Describe a where describe :: a -> String instance describe1 :: Describe (Array Int) where describe _ = "I am an Array Int" instance describe2 :: Describe (Array Number) where describe _ = "I am an Array Number"

The compiler has had to look beyond the head of each instance to select it here.

hdgarrood · 2017-07-18T21:50:42Z

language/Type-Classes.md

@@ -80,6 +102,63 @@ In fact, a type similar to this `AddInt` is provided in `Data.Monoid.Additive`,

 For multi-parameter type classes, the orphan instance check requires that the instance is either in the same module as the class, or the same module as at least one of the types occurring in the instance. (TODO: example)

+## Kinds
+
+Type class parameters do not need to be of kind Type. To explicitly specify a different kind, the parameter can be annotated with a kind signature. Unless the kind of a type parameter is explicitly annotated, it will be implicitly inferred based on how the type parameter is used in the type class's method signatures.


I think it's much more common that the kind of a type class parameter can be inferred from the methods than not, and so I think it would make more sense to talk about how the kind can be inferred before mentioning that a kind annotation can be provided. Also I think the "implicitly" is redundant here (is there such a thing as "explicit inference")?

chexxor · 2018-01-14T03:28:34Z

@hdgarrood I finally got around to addressing your comments on this one.

hdgarrood · 2018-01-16T12:20:47Z

There are still a few aspects of this which don't quite feel right to me, in particular the explanation of why we don't allow rows in instances. At this point I feel I really need to poke around inside the compiler to work out what is going on here and why. Unfortunately now that the semester has started again I probably won't be able to do that for quite some time.

RathishB23 · 2019-03-26T19:52:42Z

Add data type examples for a documentation project

JordanMartinez · 2021-09-19T03:44:00Z

Closing due to inactivity. Also, I think the entire doc repo could be redesigned. So, this could likely be clarified then.

Explain rows in typeclass instances

44b40c6

Add example for instance of specific row

a7477e5

Add section for Kinds. Clarify concrete rows disallowed.

1e28e7d

hdgarrood reviewed Jul 12, 2017

View reviewed changes

Extend and clarify the Kinds section of Typeclasses

e616185

LiamGoodacre reviewed Jul 18, 2017

View reviewed changes

chexxor added 2 commits July 18, 2017 15:34

Clarify Kinds section of type classes.

7bcb558

Add "Instance Selection" section to type classes

3bb61e2

hdgarrood reviewed Jul 18, 2017

View reviewed changes

chexxor added 3 commits January 13, 2018 21:22

Address review comments

40d4abc

Merge branch 'master' into chexxor-rows-in-instances

f64b4a1

Merge branch 'master' into chexxor-rows-in-instances

81699b1

hdgarrood mentioned this pull request Mar 26, 2019

Chexxor rows in instances #249

Closed

JordanMartinez closed this Sep 19, 2021


		Instance selection works by looking at the "head" types of each type class parameter. Functional dependencies also plays a role, but we'll not consider that for now to simplify the explanation. The "head" of a type is the top-most type constructor, for example the head of `Array Int` is `Array` and the head of `Record r` is `Record`.

		As rows and records can easily be conflated to refer to the same thing, their difference is important to note here. `Record` is a simple type constructor in PureScript and therefore can be a head in an instance.


		## Rows

		Concrete Row literals cannot appear in instances unless it's concrete type is fully determined by functional dependencies.

Explain rows in typeclass instances #104

Explain rows in typeclass instances #104

Uh oh!

Conversation

chexxor commented Jul 12, 2017

Uh oh!

hdgarrood commented Jul 12, 2017

Uh oh!

hdgarrood commented Jul 12, 2017

Uh oh!

chexxor commented Jul 12, 2017

Uh oh!

hdgarrood commented Jul 12, 2017

Uh oh!

hdgarrood commented Jul 12, 2017

Uh oh!

hdgarrood commented Jul 12, 2017

Uh oh!

chexxor commented Jul 12, 2017

Uh oh!

hdgarrood left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

chexxor commented Jul 17, 2017

Uh oh!

hdgarrood commented Jul 17, 2017

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

chexxor commented Jul 18, 2017

Uh oh!

chexxor commented Jul 18, 2017

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

chexxor commented Jan 14, 2018

Uh oh!

hdgarrood commented Jan 16, 2018

Uh oh!

RathishB23 commented Mar 26, 2019

Uh oh!

JordanMartinez commented Sep 19, 2021

Uh oh!

Uh oh!