From 44b40c6591f9efcec2c68cfa90e9192158fbef96 Mon Sep 17 00:00:00 2001 From: Alex Berg Date: Wed, 12 Jul 2017 16:09:52 -0500 Subject: [PATCH 1/7] Explain rows in typeclass instances --- language/Type-Classes.md | 20 ++++++++++++++++++++ 1 file changed, 20 insertions(+) diff --git a/language/Type-Classes.md b/language/Type-Classes.md index 3ebd1d3b..a346dc5d 100644 --- a/language/Type-Classes.md +++ b/language/Type-Classes.md @@ -80,6 +80,26 @@ 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) +## Rows + +Rows can't appear in instances as the head. Following is an explanation for this. + +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`. Row is of kind `# Type`, and this kind is simply restricted from being the head in an instance. + +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, however, can not. See this example: + +``` +class M t +-- OOO We can write an instance for a generic `Record`. +instance mRec :: M (Record r) +-- But we *can't* write one for a "specific" Record row. +-- XXX Can't specify an empty row. +instance mRec' :: M (Record ()) +-- XXX Can't specify a row having a label. +instance mRec'' :: M (Record (a :: Int)) +``` + +A reason for this is that PureScript doesn't allow orphan instances. Row has an unbounded/open set of labels and combination of labels and types. Each unique row has a unique type. A unique row value's type doesn't have a name in a module, so to avoid orphan instances, its instance of a class would need to be defined in the same module as the typeclass. Typeclasses like Ord and Semigroup can't have an instance for every specific row that people want to use - it's untenable. ## Functional Dependencies From a7477e5cb7bf08488d337f650c18eb9b05485c10 Mon Sep 17 00:00:00 2001 From: Alex Berg Date: Wed, 12 Jul 2017 16:57:53 -0500 Subject: [PATCH 2/7] Add example for instance of specific row --- language/Type-Classes.md | 21 +++++++++++++-------- 1 file changed, 13 insertions(+), 8 deletions(-) diff --git a/language/Type-Classes.md b/language/Type-Classes.md index a346dc5d..183529a7 100644 --- a/language/Type-Classes.md +++ b/language/Type-Classes.md @@ -82,24 +82,29 @@ For multi-parameter type classes, the orphan instance check requires that the in ## Rows -Rows can't appear in instances as the head. Following is an explanation for this. +Rows can't appear in instances as the head. + +``` purescript +class M t +-- XXX Can't write an instance for a specific row. +instance mClosedRow :: M () +``` 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`. Row is of kind `# Type`, and this kind is simply restricted from being the head in an instance. -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, however, can not. See this example: +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. -``` +``` purescript class M t --- OOO We can write an instance for a generic `Record`. +-- OOO Can write an instance for a `Record` without specifying the row inside. instance mRec :: M (Record r) --- But we *can't* write one for a "specific" Record row. --- XXX Can't specify an empty row. +-- XXX Can't specify a Record having an empty row, specifically. instance mRec' :: M (Record ()) --- XXX Can't specify a row having a label. +-- XXX Further, can't specify a Record having a one-label row, specifically. instance mRec'' :: M (Record (a :: Int)) ``` -A reason for this is that PureScript doesn't allow orphan instances. Row has an unbounded/open set of labels and combination of labels and types. Each unique row has a unique type. A unique row value's type doesn't have a name in a module, so to avoid orphan instances, its instance of a class would need to be defined in the same module as the typeclass. Typeclasses like Ord and Semigroup can't have an instance for every specific row that people want to use - it's untenable. +A reason for rows being disallowed from appearing in instances is that PureScript doesn't allow orphan instances. Row has an unbounded/open set of labels and combination of labels and types. Each unique row has a unique type. A unique row value's type doesn't have a name in a module, so to avoid orphan instances, its instance of a class would need to be defined in the same module as the typeclass. ## Functional Dependencies From 1e28e7d6fc88739e284f9834685f5c8d6e7348c5 Mon Sep 17 00:00:00 2001 From: Alex Berg Date: Wed, 12 Jul 2017 17:25:19 -0500 Subject: [PATCH 3/7] Add section for Kinds. Clarify concrete rows disallowed. --- language/Type-Classes.md | 35 +++++++++++++++++++++++++++++------ 1 file changed, 29 insertions(+), 6 deletions(-) diff --git a/language/Type-Classes.md b/language/Type-Classes.md index 183529a7..4afc5e1a 100644 --- a/language/Type-Classes.md +++ b/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. + +``` purescript +class A a +-- `a` is kind `Type` +class B (b :: Type) +-- `b` is kind `Type` +class C c + f :: forall a b. (a -> b) -> c a -> c b +-- `c` is kind `Type -> Type` +class D (d :: Type -> Type) +-- `d` is kind `Type -> Type` +class E (e :: # Type) +-- `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`. + ## Rows -Rows can't appear in instances as the head. +Concrete Row literals cannot appear in instances. ``` purescript class M t --- XXX Can't write an instance for a specific row. +-- Can't write an instance for a specific row. instance mClosedRow :: M () +class M' (t :: # Type) +-- Can write an instance for a generic row. +instance mAnyRow :: M r ``` -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`. Row is of kind `# Type`, and this kind is simply restricted from being the head in an instance. +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. ``` purescript class M t --- OOO Can write an instance for a `Record` without specifying the row inside. +-- Can write an instance for a `Record` without specifying a concrete row inside. instance mRec :: M (Record r) --- XXX Can't specify a Record having an empty row, specifically. +-- Can't specify a Record having an empty row, specifically. instance mRec' :: M (Record ()) --- XXX Further, can't specify a Record having a one-label row, specifically. +-- Further, can't specify a Record having a one-label row, specifically. instance mRec'' :: M (Record (a :: Int)) ``` From e6161856c968e4fd476cd091e79f492e043300fa Mon Sep 17 00:00:00 2001 From: Alex Berg Date: Mon, 17 Jul 2017 12:32:39 -0500 Subject: [PATCH 4/7] Extend and clarify the Kinds section of Typeclasses --- language/Type-Classes.md | 35 +++++++++++++++++++++++++---------- 1 file changed, 25 insertions(+), 10 deletions(-) diff --git a/language/Type-Classes.md b/language/Type-Classes.md index 4afc5e1a..a799cd09 100644 --- a/language/Type-Classes.md +++ b/language/Type-Classes.md @@ -82,33 +82,48 @@ For multi-parameter type classes, the orphan instance check requires that the in ## 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. +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. ``` purescript class A a --- `a` is kind `Type` +-- with a kind signature or methods, `a` defaults to kind `Type`. class B (b :: Type) --- `b` is kind `Type` +-- `b` is specified as kind `Type`, so its instances must also be this kind. class C c f :: forall a b. (a -> b) -> c a -> c b --- `c` is kind `Type -> Type` +-- `c`'s kind is unspecified, so it is inferred to be `Type -> Type` by its method `f`. class D (d :: Type -> Type) --- `d` is kind `Type -> Type` +-- `D` has no methods, but we can still declare it to apply to types of kind `Type -> Type`. class E (e :: # Type) --- `e` is kind `# Type` +-- Row is its own kind, so we can specify a class to operate on types of rows, `# Type`. ``` -If a typeclass's parameter's Kind is `Type`, an instance cannot be made for a type of kind `# Type` or `Type -> Type`. +The kinds of any types mentioned in an instance declaration must match the kinds of those parameters as determined by the typeclass's definition. + +For example: + +``` purescript +-- Functor can only be considered for types of kind `Type -> Type`. +class Functor f where + map :: forall a b. (a -> b) -> f a -> f b +-- Either is kind `Type -> Type -> Type`. +data Either a b = Left a | Right b +-- This means we can't write an instance of Functor for Either. +`instance functorEither :: Functor Either where ...` -- compile error +-- To make Either into kind `Type -> Type`, we simply include the first type parameter. +`instance functorEither :: Functor (Either e) where ...` +``` + +An effect of needing to adjust the kind of a data type to fit into a typeclass 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. ## Rows Concrete Row literals cannot appear in instances. ``` purescript -class M t --- Can't write an instance for a specific row. +class M (t :: # Type) +-- Cannot write an instance for a specific row. instance mClosedRow :: M () -class M' (t :: # Type) -- Can write an instance for a generic row. instance mAnyRow :: M r ``` From 7bcb55858d9d715c8b0ace28902bdaecf8f9a5df Mon Sep 17 00:00:00 2001 From: Alex Berg Date: Tue, 18 Jul 2017 15:34:32 -0500 Subject: [PATCH 5/7] Clarify Kinds section of type classes. --- language/Type-Classes.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/language/Type-Classes.md b/language/Type-Classes.md index a799cd09..d7a76420 100644 --- a/language/Type-Classes.md +++ b/language/Type-Classes.md @@ -82,7 +82,7 @@ For multi-parameter type classes, the orphan instance check requires that the in ## 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. +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. ``` purescript class A a @@ -130,7 +130,7 @@ instance mAnyRow :: M r 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. +As rows and records can easily be conflated to refer to the same thing, their difference is important to note here. `Record` is a type constructor in PureScript and therefore can be a head in an instance. ``` purescript class M t From 3bb61e253ddda89bb53cd2855956a40f59f3bc58 Mon Sep 17 00:00:00 2001 From: Alex Berg Date: Tue, 18 Jul 2017 16:05:58 -0500 Subject: [PATCH 6/7] Add "Instance Selection" section to type classes --- language/Type-Classes.md | 52 ++++++++++++++++++++++++++-------------- 1 file changed, 34 insertions(+), 18 deletions(-) diff --git a/language/Type-Classes.md b/language/Type-Classes.md index d7a76420..12aa89e6 100644 --- a/language/Type-Classes.md +++ b/language/Type-Classes.md @@ -6,7 +6,7 @@ Types appearing in class instances are must be of the form `String`, `Number`, ` Type class instances are resolved based on the order in which they appeared in the source files. Overlapping instances are currently permitted but not recommended. In simple cases the compiler will display a warning and list the instances it found and which was chosen. In the future they may be disallowed completely. -Here is an example of the `Show` typeclass, with instances for `String`, `Boolean` and `Array`: +Here is an example of the `Show` type class, with instances for `String`, `Boolean` and `Array`: ```purescript class Show a where @@ -25,6 +25,28 @@ instance showArray :: (Show a) => Show (Array a) where example = show [true, false] ``` +## Instance selection + +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`. + +``` purescript +class C t where + f :: t -> String +-- Instances are chosen +instance cRec :: C (Record r) where + f _ = "this is a record" +instance cArr :: C (Array a) where + f _ = "this is an array" + +main = do + -- The `f` function resolves to the instance for the argument type's head. + log (f {}) -- Resolves to cRec's f. + log (f []) -- Resolves to cArr's f. +-- Prints the following when executed. +this is a record +this is an array +``` + ## Multi-Parameter Type Classes TODO. For now, see the section in [PureScript by Example](https://leanpub.com/purescript/read#leanpub-auto-multi-parameter-type-classes). @@ -98,7 +120,7 @@ class E (e :: # Type) -- Row is its own kind, so we can specify a class to operate on types of rows, `# Type`. ``` -The kinds of any types mentioned in an instance declaration must match the kinds of those parameters as determined by the typeclass's definition. +The kinds of any types mentioned in an instance declaration must match the kinds of those parameters as determined by the type class's definition. For example: @@ -114,11 +136,11 @@ data Either a b = Left a | Right b `instance functorEither :: Functor (Either e) where ...` ``` -An effect of needing to adjust the kind of a data type to fit into a typeclass 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. +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. ## Rows -Concrete Row literals cannot appear in instances. +Concrete Row literals cannot appear in instances unless it's concrete type is fully determined by functional dependencies. ``` purescript class M (t :: # Type) @@ -126,23 +148,17 @@ class M (t :: # Type) instance mClosedRow :: M () -- Can write an instance for a generic row. instance mAnyRow :: M r -``` - -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 type constructor in PureScript and therefore can be a head in an instance. - -``` purescript -class M t --- Can write an instance for a `Record` without specifying a concrete row inside. -instance mRec :: M (Record r) --- Can't specify a Record having an empty row, specifically. -instance mRec' :: M (Record ()) --- Further, can't specify a Record having a one-label row, specifically. -instance mRec'' :: M (Record (a :: Int)) +-- The row's type is determined by the type of `dt`. +class Ctors dt (ct :: # Type) | dt -> ct +-- Can use a row literal in instances of this class. +data X = X0 Int | X1 String +instance ctorsX :: Ctors X ("X0" :: Int, "X1" :: String) +data Y = Y0 Boolean +instance ctorsY :: Ctors Y ("Y0" :: Boolean) ``` -A reason for rows being disallowed from appearing in instances is that PureScript doesn't allow orphan instances. Row has an unbounded/open set of labels and combination of labels and types. Each unique row has a unique type. A unique row value's type doesn't have a name in a module, so to avoid orphan instances, its instance of a class would need to be defined in the same module as the typeclass. +A reason for rows being disallowed from appearing in instances is that PureScript doesn't allow orphan instances. Row has an unbounded/open set of labels and combination of labels and types. Each unique row has a unique type. A unique row value's type doesn't have a name in a module, so to avoid orphan instances, its instance of a class would need to be defined in the same module as the type class. ## Functional Dependencies From 40d4abcfee87083d0b15d1c8bd2c1dff3a1cbc5a Mon Sep 17 00:00:00 2001 From: Alex Berg Date: Sat, 13 Jan 2018 21:22:48 -0600 Subject: [PATCH 7/7] Address review comments --- language/Type-Classes.md | 32 +++++++++++++++++--------------- 1 file changed, 17 insertions(+), 15 deletions(-) diff --git a/language/Type-Classes.md b/language/Type-Classes.md index 12aa89e6..97a10d60 100644 --- a/language/Type-Classes.md +++ b/language/Type-Classes.md @@ -27,24 +27,28 @@ example = show [true, false] ## Instance selection -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`. +Instance selection works by looking at the "head" type 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 an instance is the type declared after the class name in an instance. For example, the head of `instance cRec :: C (Array a)` is `Array a`. ``` purescript class C t where f :: t -> String -- Instances are chosen +instance cArr :: C (Array a) where + f _ = "this is an array of 'a'" +instance cArrInt :: C (Array Int) where + f _ = "this is an array of ints" instance cRec :: C (Record r) where f _ = "this is a record" -instance cArr :: C (Array a) where - f _ = "this is an array" main = do -- The `f` function resolves to the instance for the argument type's head. - log (f {}) -- Resolves to cRec's f. - log (f []) -- Resolves to cArr's f. + log (f []) -- Resolves to cArr's f, because `Array a` is the argument, which matches `Array a` + log (f [1]) -- Resolves to cArr's f, because `Array Int` matches `Array a` before trying the cArrInt instance + log (f {}) -- Resolves to cRec's f -- Prints the following when executed. +this is an array of 'a' +this is an array of 'a' this is a record -this is an array ``` ## Multi-Parameter Type Classes @@ -104,16 +108,16 @@ For multi-parameter type classes, the orphan instance check requires that the in ## 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. +A type class parameter's kind is commonly inferred by its use in the class's methods. If its kind cannot be inferred, it defaults to kind `Type`. To explicitly specify a different kind for a type parameter defaulting to `Type`, annotate it with a kind signature, as shown in the `class D` example below. ``` purescript +class C c + f :: forall a b. (a -> b) -> c a -> c b +-- `c`'s kind is inferred to be `Type -> Type` by how it's used in the method, `f`. class A a --- with a kind signature or methods, `a` defaults to kind `Type`. +-- with no methods or explicit kind signature, `a` defaults to kind `Type`. class B (b :: Type) -- `b` is specified as kind `Type`, so its instances must also be this kind. -class C c - f :: forall a b. (a -> b) -> c a -> c b --- `c`'s kind is unspecified, so it is inferred to be `Type -> Type` by its method `f`. class D (d :: Type -> Type) -- `D` has no methods, but we can still declare it to apply to types of kind `Type -> Type`. class E (e :: # Type) @@ -132,15 +136,13 @@ class Functor f where data Either a b = Left a | Right b -- This means we can't write an instance of Functor for Either. `instance functorEither :: Functor Either where ...` -- compile error --- To make Either into kind `Type -> Type`, we simply include the first type parameter. +-- Either can be made into kind `Type -> Type`, however, by simply including the first type parameter. `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. - ## Rows -Concrete Row literals cannot appear in instances unless it's concrete type is fully determined by functional dependencies. +A concrete Row literal cannot appear in an instance unless it is fully determined by functional dependencies. ``` purescript class M (t :: # Type)