From 886c0794e6799015d430a4313219a6a0375773d0 Mon Sep 17 00:00:00 2001 From: mangoiv Date: Fri, 6 Dec 2024 15:05:28 +0100 Subject: [PATCH 1/3] [feat] add polarity for haskellers --- contrib/polarity-for-haskellers/README.md | 115 ++++++++++++++++++++++ 1 file changed, 115 insertions(+) create mode 100644 contrib/polarity-for-haskellers/README.md diff --git a/contrib/polarity-for-haskellers/README.md b/contrib/polarity-for-haskellers/README.md new file mode 100644 index 000000000..d9144db69 --- /dev/null +++ b/contrib/polarity-for-haskellers/README.md @@ -0,0 +1,115 @@ +# Polarity for Haskellers + +It might be a bit confusing to understand what polarity's `data` and `codata` and `def` and `codef` do differently than Haskell's data. Especially observing infinite streams is incredibly easy in Haskell. + +Take for example: + +```haskell +data Stream a = MkStream a (Stream a) + +ones :: Stream Int +ones = MkStream 1 ones +``` +Now, we could easily just observe the 5th element by pealing off 5 `MkStream` constructors and returning the the element in the cell contained there; No need of `codata`. +However, it is not that easy in typical strict languages. For that, let us make Haskell a language with strict datatypes, using the `-XUnliftedDataTypes` extension. + +```haskell +import Data.Kind (Type) +import GHC.Exts (Int#, UnliftedType, (-#)) +import qualified GHC.Int as Int + +type SType = UnliftedType +type LType = Type + +-- strict Ints, wrapping machine Ints +type I :: SType +data I = I# Int# + +-- strict, finite lists +type L :: SType -> SType +data L a = N | C a (L a) +``` + +`SType`s are always strict, that is, they will never be thunks. That means, that our usual definition of a `Stream` falls through; as soon as we try to observe `ones`, our interpreter will hang. Try it out for yourself, by redefining `Stream` as +```haskell +type Stream a :: SType -> SType +data Stream a = MkStream a (Stream a) +``` + +Now that we cannot make infinite streams that simply anymore, we have to shift our thinking from what it means to *build* a stream to what it means to *observe* a stream. In order to achive this, we dualize the stream type by: +1. instead of using a product of compontents, use a sum of observervations +2. instead of demanding the compontents when building the stream, ask for the decision of what we are going to observe + +The former is pretty simple, we define the datatype: +```haskell +type StreamObservation :: SType -> SType -> SType +data StreamObservation a r + = Hd (a -> r) + | Tl (Stream a -> r) +``` +As you can see, everything is a strict datatype still so you know we are not cheating you. This datatype now describes what it means to observe a stream: +1. either, you see the head (`Hd`) in which case you may do something with the element you find there, or +2. you will observe the tail (`Tl`) in which case you may do something with the stream that makes up tail. + +Now, to restore the interface that we are used to, let's wrap the idea of "give us an observation and we will execute it for you" in a `newtype`: +```haskell +type Stream :: SType -> LType +newtype Stream a = MkStream {unStream :: forall r. StreamObservation a r -> r} +``` +As you may have noticed, this returns an `LType`, not an `SType`; the reason is that representationally, a `Stream` is now a function closure, the only primitive lazy datastructure in many strict langauges, just like in our imaginary strict Haskell. +In polarity, which does not have functions but instead has `codata` types, we can write this type out a bit simpler, namely as: +```polarity +codata Stream(a : Type) + { Stream(a).head(a : Type): a + , Stream(a).tail(a : Type): Stream(a) + } +``` +Just like the Haskell version, it offers you two options to observe a stream, but it leaves out the CPS encoding part. This makes it also nicer to create streams with `codef`, which we will see in a minute. In order to do so in haskell, let's define the stream that consists only of ones, that is no matter how far you go (by observing `Tl`), every time you observe head afterwards (`Hd`), you obtain a one. +```haskell +ones :: Stream I +ones = MkStream \case + Hd k -> k (I# 1#) -- observe the number one that lives in every cell of the Stream + Tl k -> k ones -- observe the remainder of the stream + where + one = I# 1# +``` +in polarity, the definition looks quite similar, except that, instead of using continuation passing style, we can write it in direct style, similarly to how it is done in object oriented programming's class methods: +```polarity +data Nat {Z : Nat, S(n : Nat) : Nat} + +codef Ones: Stream(Nat) { -- use codef to define a Stream + .head(_) => S(Z), -- when observing the head, return 1 + .tail(_) => Ones -- otherwise, we observe a stream of ones +} +``` + +So far so good, now we know how to use the non-dependent portion of polarity and how it corresponds to Haskell. + +Howerver, there's another peculiar thing happening: instead of infinitely many numbers, we now only need a single one to construct the stream, so, if we do not duplicate the stream or let the continuation use the result multiple times, there's actually only a single one we can get out of a stream. + +We can make that obvious using `-XLinearHaskell` but we have to rewrite some definitions: +```haskell +type StreamObservation :: SType -> SType -> SType +data StreamObservation a r where + Hd :: (a %1 -> r) %1 -> StreamObservation a r + Tl :: (Stream a %1 -> r) %1 -> StreamObservation a r + +type Stream :: SType -> LType +newtype Stream a where + MkStream :: (forall r. StreamObservation a r %1 -> r) %1 -> Stream a + +unStream :: Stream a %1 -> forall r. StreamObservation a r %1 -> r +unStream (MkStream s) = s +``` +Now, if we want to define a stream of some universally quantified `a`, we can write: +```haskell +mk :: a %1 -> Stream a +mk x = MkStream \case + Hd k -> k x + Tl k -> k (mk x) +``` +Now, if we were allowed to use this `a` more than one, the type checker would scream at us, but since it doesn't, we are good. + +So to recap: +- in polarity, making things observable instead of buildable is achieved using `codef` and `codata`. This is equivalent to non-strict semantics, in that we have to pass the continuation that does the observation for us. +- what Haskell does not give you is dependent types, which is why we left them out here - the encoding of dependent types that you have to do in Haskell is much more complex than in polarity From 401f90e26b4d59fb2af394f0d8af14e61c68ca6f Mon Sep 17 00:00:00 2001 From: Mango The Fourth <40720523+MangoIV@users.noreply.github.com> Date: Mon, 16 Dec 2024 22:34:37 +0100 Subject: [PATCH 2/3] [chore] add first few suggestions by Tim MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: Tim Süberkrüb --- contrib/polarity-for-haskellers/README.md | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/contrib/polarity-for-haskellers/README.md b/contrib/polarity-for-haskellers/README.md index d9144db69..ad13d9ef1 100644 --- a/contrib/polarity-for-haskellers/README.md +++ b/contrib/polarity-for-haskellers/README.md @@ -1,6 +1,6 @@ # Polarity for Haskellers -It might be a bit confusing to understand what polarity's `data` and `codata` and `def` and `codef` do differently than Haskell's data. Especially observing infinite streams is incredibly easy in Haskell. +It might be a bit confusing to understand what Polarity's `data` and `codata` and `def` and `codef` do differently than Haskell's data. Especially observing infinite streams is incredibly easy in Haskell. Take for example: @@ -10,7 +10,7 @@ data Stream a = MkStream a (Stream a) ones :: Stream Int ones = MkStream 1 ones ``` -Now, we could easily just observe the 5th element by pealing off 5 `MkStream` constructors and returning the the element in the cell contained there; No need of `codata`. +Now, we could easily just observe the 5th element by pealing off 5 `MkStream` constructors and returning the the element in the cell contained there; no need of `codata`. However, it is not that easy in typical strict languages. For that, let us make Haskell a language with strict datatypes, using the `-XUnliftedDataTypes` extension. ```haskell @@ -37,8 +37,8 @@ data Stream a = MkStream a (Stream a) ``` Now that we cannot make infinite streams that simply anymore, we have to shift our thinking from what it means to *build* a stream to what it means to *observe* a stream. In order to achive this, we dualize the stream type by: -1. instead of using a product of compontents, use a sum of observervations -2. instead of demanding the compontents when building the stream, ask for the decision of what we are going to observe +1. instead of using a product of components, use a sum of observations +2. instead of demanding the components when building the stream, ask for the decision of what we are going to observe The former is pretty simple, we define the datatype: ```haskell @@ -85,7 +85,7 @@ codef Ones: Stream(Nat) { -- use codef to define a Stream So far so good, now we know how to use the non-dependent portion of polarity and how it corresponds to Haskell. -Howerver, there's another peculiar thing happening: instead of infinitely many numbers, we now only need a single one to construct the stream, so, if we do not duplicate the stream or let the continuation use the result multiple times, there's actually only a single one we can get out of a stream. +However, there's another peculiar thing happening: instead of infinitely many numbers, we now only need a single one to construct the stream, so, if we do not duplicate the stream or let the continuation use the result multiple times, there's actually only a single one we can get out of a stream. We can make that obvious using `-XLinearHaskell` but we have to rewrite some definitions: ```haskell @@ -108,7 +108,7 @@ mk x = MkStream \case Hd k -> k x Tl k -> k (mk x) ``` -Now, if we were allowed to use this `a` more than one, the type checker would scream at us, but since it doesn't, we are good. +Now, if we were allowed to use this `a` more than once, the type checker would complain, but since it doesn't, we are good. So to recap: - in polarity, making things observable instead of buildable is achieved using `codef` and `codata`. This is equivalent to non-strict semantics, in that we have to pass the continuation that does the observation for us. From 2fb014ef5e9adab8f190dc59544a90c05ccb9e5d Mon Sep 17 00:00:00 2001 From: Mango The Fourth <40720523+MangoIV@users.noreply.github.com> Date: Mon, 16 Dec 2024 22:35:33 +0100 Subject: [PATCH 3/3] [chore] Apply suggestions from tims's code review --- contrib/polarity-for-haskellers/README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/contrib/polarity-for-haskellers/README.md b/contrib/polarity-for-haskellers/README.md index ad13d9ef1..8a93796f2 100644 --- a/contrib/polarity-for-haskellers/README.md +++ b/contrib/polarity-for-haskellers/README.md @@ -10,7 +10,7 @@ data Stream a = MkStream a (Stream a) ones :: Stream Int ones = MkStream 1 ones ``` -Now, we could easily just observe the 5th element by pealing off 5 `MkStream` constructors and returning the the element in the cell contained there; no need of `codata`. +Now, we could easily just observe the 5th element by peeling off 5 `MkStream` constructors and returning the the element in the cell contained there; no need for `codata`. However, it is not that easy in typical strict languages. For that, let us make Haskell a language with strict datatypes, using the `-XUnliftedDataTypes` extension. ```haskell