From b492c2d0fba4693f7cfca8f0d852e8780f3b88ae Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Sun, 29 Jan 2023 21:08:31 -0800 Subject: [PATCH] Add more drafts --- content/blog/haskell_newtype.md | 93 +++++++++++++++++++ content/blog/typeclasses_are_logic.md | 125 ++++++++++++++++++++++++++ 2 files changed, 218 insertions(+) create mode 100644 content/blog/haskell_newtype.md create mode 100644 content/blog/typeclasses_are_logic.md diff --git a/content/blog/haskell_newtype.md b/content/blog/haskell_newtype.md new file mode 100644 index 0000000..f91d1aa --- /dev/null +++ b/content/blog/haskell_newtype.md @@ -0,0 +1,93 @@ +--- +title: "Multiple Typeclass Instances using Newtype in Haskell" +date: 2022-04-28T23:09:42-07:00 +tags: ["Haskell"] +draft: true +--- + +> And I have known the eyes already, known them all— +> +> The eyes that fix you in a formulated phrase . . . + +It sometimes feels like the data types that we work with are simply +too locked down through their typeclass instances. A type might have multiple +law-abiding implementations of the required methods, and yet only one implementation can be used +in an `instance` declaration. First, let's take a look at some type classes and types +for which this is true, starting with `Monoid`. + +### The `Monoid` Type Class +Recall that for a type `m` with `Monoid m`, the following things are available: + +* An associative binary operation, `(<>)`. Associativity means that for any + three elements of `m`, like `a`, `b`, and `c`, the following + holds: + + ```Haskell + (a <> b) <> c == a <> (b <> c) + ``` +* An neutral element under `(<>)`, called `mempty`. It being the neutral element + means that using it with `(<>)` doesn't do anything. For any `a :: m`, we + can (with minor notation abuse) write the following: + + ```Haskell + a <> mempty == mempty <> a == a + ``` + +This is a pretty broad specification, actually. Many types have multiple different +operations that satisfy the `Monoid` laws. Let's take a look at a few of them, +starting with integers. + +#### Integers +Addition is an associative binary operation. Furthermore, it's well-known that adding zero to a +number leaves that number intact: \\(0+n = n + 0 = n\\). So we might define a `Monoid` instance for +numbers as follows. Note that we actually provide `(<>)` via the `Semigroup` class, +which _just_ requires the associative binary operation, and serves as a superclass for `Monoid`. + +```Haskell +instance Semigroup Int where + (<>) = (+) + +instance Monoid Int where + mempty = 0 +``` + +Cool and good. But hey, there are other binary operations on integers! What about +multiplication? It is also associative, and again it is well-known that multiplying +anything by one leaves that number as it was: \\(1\*n = n\*1 = n\\). The corresponding +`Monoid` instance would be something like the following: + +```Haskell +instance Semigroup Int where + (<>) = (*) + +instance Monoid Int where + mempty = 1 +``` + +But we can't have both. Haskell yells at us: + +``` +Duplicate instance declarations: + instance Semigroup Int -- Defined at test.hs:1:10 + instance Semigroup Int -- Defined at test.hs:7:10 + +Duplicate instance declarations: + instance Monoid Int -- Defined at test.hs:4:10 + instance Monoid Int -- Defined at test.hs:10:10 +``` + +Okay, so we can have at most one. But that's not good. +Fortunately, thanks to the `Num` instance for `Int`, we get +functions that are pretty much the same as `fold`, except +specialized to multiplication and addition: + +```Haskell +fold :: (Foldable t, Monoid m) => t m -> m +product :: (Foldable t, Num a) => t a -> a +sum :: (Foldable t, Num a) => t a -> a +``` + +This takes care of _most_ of the uses we have for `(+)` and `(*)`; +it does, however, prevent us from using `Int` with [`MonadWriter`](https://hackage.haskell.org/package/mtl-2.2.2/docs/Control-Monad-Writer-Lazy.html#t:MonadWriter). + +#### Booleans diff --git a/content/blog/typeclasses_are_logic.md b/content/blog/typeclasses_are_logic.md new file mode 100644 index 0000000..5566c90 --- /dev/null +++ b/content/blog/typeclasses_are_logic.md @@ -0,0 +1,125 @@ +--- +title: Typeclasses are Basically Logic Programming +date: 2021-06-28T17:11:38-07:00 +draft: true +description: "In this post, we explore the connection between typeclasses and logic programming." +tags: ["Haskell", "Prolog"] +--- + +I recently spent some time playing around with the implementation of +Haskell-like typeclasses in a toy functional language. In doing so +I noticed how similar an implementation of a little logic programming +language is to an implementation of type class search. Though this +may be very well known, I thought I'd take some time to describe +the similarities (and the differences). + +### Kicking off the `Show` +Let's begin with a very simple typeclass: `Show`. When I was a TA +for my university's programming languages course, we mentioned +this typeclass to the students, despite considering typeclasses +as a whole to be a topic beyond our scope. Four our purposes, we +can consider it to be a class with only one method: `show`. + +```Haskell +class Show a where + show :: a -> String +``` + +An instance of `Show` may look as follows: + +```Haskell +instance Show () where + show () = "()" +``` + +So far, we haven't done much: we let Haskell know of a typeclass `Show`, +and also that `()` has an implementation of show. One might write +this in Prolog as follows: + +{{< codelines "Prolog" "typeclass-prolog/kb.pl" 1 1 >}} + +Wait a moment, something was lost intranslation. What about `show`, +and its implementation? We did not carry these over into Prolog. +A truly equivalent formulation in Prolog would contain this +information; however, for simplicity, +{{< sidenote "right" "pretend-note" "we'll pretend that" >}} +I'd argue that our little make-believe is morally correct. We +can think of it in this way: to be allowed to write down +the equivalent Prolog rule you need to provide all the required methods, +and the proof that you provided them is recorded alongside the +rule. A sort of entrance ticket, if you will. +{{< /sidenote >}} +the line of code above, and any further lines of code of that sort, are +endowed with the implementation of all the required methods. + +On to something more interesting. It's well known that if you can print +the elements of a Haskell list, you can also print the list itself. The +implementation looks something like this: + +```Haskell +instance Show a => Show [a] where + show l = "[" ++ intercalate "," (map show l) ++ "]" +``` + +We can't print just any list; for instance, `[Int -> Bool]` does not have +a `Show` instance, because `Int -> Bool` itself does not have a show instance. +This dependency is encoded in Prolog as follows: + +{{< codelines "Prolog" "typeclass-prolog/kb.pl" 2 2 >}} + +Implicit in both the Haskell instance and the Prolog rule is the "forall" +quantifier: we have "for all types `a`, if `Show a`, then `Show [a]`", +and "for all terms `X`, if `show(X)` holds, then `show(list(X))` holds". + +With only these two instances, what types can we print? Let's ask Prolog: + +```Prolog +?- show(X). +X = unit ; +X = list(unit) ; +X = list(list(unit)) ; +X = list(list(list(unit))) ; +... +``` + +These correspond to `()` (naturally), `[()]`, `[[()]]`, and so on. Indeed, +in Haskell, we'd be able to use `show` to turn values of these types +(and only these types, assuming our two instances) into strings. + +```Haskell +show () = "()" +show [()] = "[()]" +show [[()],[()]] = "[[()],[()]]" +show [[[()],[()]]] = "[[[()],[()]]]" +... +``` + +A similar principle applies to tuples, `(a,b)`. Here's the Haskell instance: + +```Haskell +instance (Show a, Show b) => Show (a, b) where + show (a,b) = "(" ++ show a ++ "," ++ show b ++ ")" +``` + +The Prolog encoding is pretty much as one would expect: + +{{< codelines "Prolog" "typeclass-prolog/kb.pl" 3 3 >}} + +### What of the superclasses? + +We've explored few of the possibilities in the Haskell's typeclass system. +For instance, there's another well-known typeclas, `Ord`: + +```Haskell +class Eq a => Ord a where + -- ... +``` + +This typeclass has a _superclass_: in order for some type `a` to have +class `Ord`, it must also have class `Eq`. We haven't seen superclasses +until now, but they are quite important to Haskell: `Applicative` is a +superclass of `Monad`, which means you can use `liftA2` and `<*>` on any monad. +A typeclass having a superclass has two important implications for us. + +First, we may not put down an instance of, say, `Ord a`, if we don't +already have an implementation of `Eq a`.