- Haskell-Cafe - Haskell.org

Design for DatatypeContexts: what was the idea, anyway?
by Anthony Clayden 15 Sep '20

15 Sep '20

Quite prosaically: the design for DatatypeContexts seems to have materialised with no visible discussion, neither agreement nor disagreement; and persisted almost unchanged until they got deprecated nearly 20 years later. I can guess there was a verbal discussion amongst the Committee circa 1990/91; that somebody was deputed to write down the conclusion (memo March 1991 [1]) ; and the implementers (both Committee members) went to work in Hugs and GHC. Much later (1999, while preparing the Haskell 1998 Report, published 2002) a fresh set of eyes spotted an under-explicitness that had been interpreted differently by the implementers; and there was a Committee thread resolving it. That thread is the best place from which to understand the intent, particularly Phil Wadler's comments [2]. Historical context: typeclasses/constraints/contexts were the new shiny thing, still rapidly evolving (Wadler early 1989, Wadler & Blott late 1989 but with several open questions). They were initially tied to overloading methods; by 1990 the Haskell report v1.0 included constraints for Numeric Literals, but with several caveats. The mailing lists had much back-and-forth about ambiguities and defaulting and (of course) the Dreaded Monomorphism Restriction for constrained terms. I see comments about the "dictionary transfer problem" and dictionaries "shared lazily between all applications to each elt [in a data structure]". The syntax of prefixing the context to the type constructor name (syntax in the 1990 Haskell Report, along with the admittedly vague descriptions there), suggests to me they were thought of as for numeric literals: `5 :: Num a => a` so `(ConsSet 5 NilSet) :: Num a => Set a`, where Set's `Eq a` is implied, as a superclass of Num. There's no visible method invocation. If the intent had been that the context attached only inside the data constructors, I'd expect syntax like one of these: data Set a = NilSet | (Eq a) => ConsSet a (Set a) data Set a = NilSet | ConsSet (Eq a) => a (Set a) (Syntax closer to that second did arrive later with GADTs.) The 1999 discussion concluded that the context should be exposed outside of a pattern match, even though a match only 'consumes' an already constructed value. Exposing makes sense if all data constructors enforce the context, but from the 1991 design, `NilSet`'s type doesn't mention the context (because there's no argument to the constructor to ground the type?). I'm confused by that: if Haskell 1990 supported `5 :: Num a => a`, what's wrong with `NilSet :: Eq a => Set a`? I sense quite a bit of exasperation in that 1991 memo: "Nobody has been able to give a satisfactory account", "Nobody has been able to explain", several phrases in block caps. The so-called "simplifications" are almost what Parliamentarians would call a 'wrecking amendment' (undermining or nullifying the intent of a proposal) or even applying Cunningham's Law (the quickest way to get the right answer is not to ask a question, but to post a wrong answer) -- except nobody (visibly) pushed back. And there's hints of dissent unresolved up to the 1999 exchange: "a broken feature of H98", "What you propose, I think, offers the worst of both worlds ", "a compile-time language feature can be hard to understand if it is not directly tied to run-time behaviour.", "Live and learn.". (Who should learn? Is that a self-admonition or aimed at others?) It's well known that SPJ dubbed the feature "stupid theta". The thing is: the scribe in 1991 was SPJ; even if he was only writing from dictation, why specify and then implement a "broken feature"? Or did it only earn the "stupid" as a result of the 1999 decision? Then it's notable in that decision that Hugs' behaviour was preferred; GHC was changed to align; but then GADTs design reverted to the GHC pre-1999 behaviour (which is reasonable considering different constructors have different constraints and return types). Pattern Synonyms support double-contexts in the signature, to be explicit about what's exposed/required outside a pattern match. I see much recent traffic (say on StackOverflow) that GADTs are DatatypeContexts 'done right'. I can't agree with that: GADTs are addressing a different set of use cases vs. the motivation Wadler explains in 1999 -- to enforce invariants -- which makes sense to me. AntC [1] http://web.archive.org/web/20160320062120/http://code.haskell.org/~dons/has… [2] http://web.archive.org/web/20151001115936/http://code.haskell.org/~dons/has… (The question is posed in the preceding message in the thread; follow the thread through to see the number of luminaries disagreeing with GHC's then behaviour.)

1 0

Need help to get started with GHC.Generics
by YueCompl 15 Sep '20

15 Sep '20

Dear Cafe, I'm tinkering with the idea for arbitrary Haskell functions to be easily called from scripting code, I see auto derive with GHC.Generics might be the most promising tool, but I'm lost after read https://wiki.haskell.org/GHC.Generics <https://wiki.haskell.org/GHC.Generics> and hackage docs. I have no clue so far with how to start with it. Specifically I want the section highlighted in blue get auto generated, within the following `runghc` ready example: ``` {-# LANGUAGE BangPatterns #-} module Main where import Prelude import GHC.Generics import Data.Dynamic -- * minimum data structures as interface with scripting code type AttrKey = String data AttrVal = NilValue | IntValue !Integer | StrValue !String deriving (Eq, Ord, Typeable) instance Show AttrVal where show NilValue = "nil" show (IntValue !x) = show x show (StrValue !x) = show x data ArgsPack = ArgsPack { positional'args :: [AttrVal] , keyword'args :: [(AttrKey, AttrVal)] } instance Semigroup ArgsPack where (ArgsPack p1 kw1) <> (ArgsPack p2 kw2) = ArgsPack (p1 ++ p2) (kw1 ++ kw2) instance Monoid ArgsPack where mempty = ArgsPack [] [] class Callable a where call :: a -> ArgsPack -> (AttrVal -> IO ()) -> IO () -- * functions to be callable from scripting code newtype Assert = Assert ( Expect -> Maybe Target -> Message -> IO Message ) type Expect = AttrVal type Target = AttrVal type Message = String instance Callable Assert where -- can this get auto-generated ? with https://wiki.haskell.org/GHC.Generics call (Assert !assert) (ArgsPack !args !kwargs) !exit = do (expect, target, message) <- parseApk result <- assert expect target message exit $ StrValue result where parseApk :: IO (Expect, Maybe Target, Message) parseApk = goParse (Left "missing arg: expect", Nothing, Left "missing arg: message") args kwargs goParse (got'expect, got'target, got'message) [] [] = case got'expect of Left msg -> error msg Right expect -> case got'message of Left msg -> error msg Right message -> return (expect, got'target, message) goParse (got'expect, got'target, got'message) args' ((name, val) : kwargs') = case name of "expect" -> case got'expect of Right{} -> error "duplicate arg: expect" Left{} -> goParse (Right val, got'target, got'message) args' kwargs' "target" -> case got'target of Just{} -> error "duplicate arg: target" Nothing -> goParse (got'expect, Just val, got'message) args' kwargs' "message" -> case got'message of Right{} -> error "duplicate arg: message" Left{} -> case val of StrValue message -> goParse (got'expect, got'target, Right message) args' kwargs' _ -> error "bad arg type for: message" _ -> error "unexpected keyword args" goParse (got'expect, got'target, got'message) (val : args') [] = case got'expect of Left{} -> goParse (Right val, got'target, got'message) args' [] Right{} -> case got'target of Nothing -> goParse (got'expect, Just val, got'message) args' [] Just{} -> case got'message of Left{} -> case val of StrValue message -> goParse (got'expect, got'target, Right message) args' [] _ -> error "bad arg type for: message" Right{} -> error "extranous positional args" -- mockup & test out main :: IO () main = call (Assert assert) (ArgsPack [IntValue 333, StrValue "as good will"] [("target", IntValue 333)] ) $ \result -> putStrLn $ "Got result: " <> show result -- | plain Haskell function meant to be easily called by scripting code assert :: Expect -> Maybe Target -> Message -> IO Message assert !expect !maybeTarget !message = case maybeTarget of Nothing -> return $ "* assertion not applicable: " <> message Just target -> if expect == target then return $ "* assertion passed: " <> message else error $ "* assertion failed: " <> message ``` I tried to understand how The compiler can provide a default generic implementation for parseJSON <https://hackage.haskell.org/package/aeson-1.5.4.0/docs/Data-Aeson.html#v:pa…>. is implemented in [aeson](https://hackage.haskell.org/package/aeson <https://hackage.haskell.org/package/aeson>) and it is overwhelming to me at the moment ... Is there easier scaffold template for me to start with GHC.Generics? Or there're even better techniques to achieve my final goal? Help please! Best regards, Compl

6 12

TypeApplications and Proxy
by Johannes Waldmann 15 Sep '20

15 Sep '20

Dear Cafe, since GHC has TypeApplication, we don't need Proxy that much? `natVal (Proxy :: Proxy w)` can be written as `natVal @w Proxy` but then, the argument `Proxy` looks unnecessary. I can define nat :: forall (n::Nat) . KnownNat n => Int nat = fromIntegral $ natVal @n Proxy and then use `nat @w`. (with -XAllowAmbiguousTypes.) I just wonder if that's already in some library. But then, what about the other direction (from value to type)? Is there a shorter way to write, e.g., reifyNat (read e) $ \ (_ :: Proxy w) -> run @w ... I see that Data.Reflection suggests `reifyNat (read 3) run` but then `run` needs the Proxy argument. Thanks, J.W.

5 6

GADT is not great - sometimes: can be almost as stupid as stupid theta
by Anthony Clayden 15 Sep '20

15 Sep '20

The sweet spot for GADTs is representing ASTs for EDSLs typefully. The characteristics of those use cases is that each data constructor: carries different constraints; returns a more specific type than `T a`; similarly recursion may be to a more specific type. There's a different use case (which is I suspect what was in mind for DatatypeContexts), with characteristics for each data constructor: * the constraints are the same for all the type's parameters; * the return type is bare `T a` * any recursion is also to bare `T a` So it's the same type `a` all the way down, and therefore the same instance for the constraint(s). Consider (adapted from the H98 Report for DatatypeContexts): {-# LANGUAGE GADTs #-} data SetG a where NilSetG :: Eq a => SetG a ConsSetG :: Eq a => a -> SetG a -> SetG a sillySetG = undefined :: SetG (Int -> Int) -- accepted, but useless -- sillySetG = NilSetG :: SetG (Int -> Int) -- rejected no Eq instance (DatatypeContext's equiv with NilSet constructor at `(Int -> Int)` is accepted, so some improvement.) elemSG x NilSetG = False elemSG x (ConsSetG y ys) | x == y = True | otherwise = elemSG x ys -- ===> elemSG :: a -> SetG a -> Bool -- no Eq a inferred The elem pattern matching test makes use of ConsSetG's Eq instance, but doesn't expose that in the inferred type. Whereas: headS (ConsSetG x _) = x -- hide the pattern match tailS (ConsSetG _ xs) = xs elemSh x NilSetG = False elemSh x yss | x == headS yss = True | otherwise = elemSG x $ tailS yss -- ==> elemSh :: Eq a => a -> SetG a -> Bool -- Eq a inferred A 'morally equivalent' elem test but with a different inferred type, exposing the `Eq a` constraint. If you give an explicit signature for `elemSh`, you must specify `Eq a` -- which is annoying same as with DatatypeContexts; an explicit signature for elemSG needn't -- which gives a more annoying imprecise type that'll get reported at some usage site. I'm concluding that for this use case, a GADT doesn't 'fix' all of the stupidness with stupid theta. AntC

2 2

Re: [Haskell-cafe] GADT is not great - sometimes: can be almost as stupid as stupid theta
by Anthony Clayden 14 Sep '20

14 Sep '20

> On Fri Sep 11 08:08:54 UTC 2020, Viktor Dukhovni wrote: > This, as I am sure you're aware, is correct, Hmm. If you mean 'working as per spec' (the OutsideIn paper), then OK. > but I'd also say unsurprising. The function indeed works for all `a`, it is just that for many `a` (those without an 'Eq' instance) the type `SetG a` is uninhabited, so the function is correct vacuously. On the basis that 'well-typed programs can't go wrong'; it allows a well-typed program that crashes. That's not correct. And it's not vacuous: `elemSG` matches on constructor; the only value of `sillySG`'s type is bottom -- i.e. no constructor. I can compile sillyElem = elemSG (id :: Int -> Int) sillySetG -- inferred type Bool Why is that not ill-typed, in the absence of an instance `Eq (Int -> Int)` ? Running that crashes *** Exception: Prelude.undefined. Whereas `elemSh (id :: Int -> Int) sillySetG` is not well-typed. I could of course specify a signature for `elemSG` with explicit `Eq a =>`, but needing to do that is exactly what people complain of with DatatypeContexts. > I wouldn't describe this situation as there being something "stupid" with GADTs. To be clear: I'm not saying there's something as stupid as with DatatypeContexts. I am saying there's a family of use-cases for which GADTs are not a good fit. The example you show using DatatypeContexts fails to compile `No instance for (Eq (Int -> Int))`, which is entirely reasonable; it does compile if supplied an instance, as you go on to show. > With this particular type, I'd argue the real problem is adding the constraints to the constructors in the first place. > With the constructors unconstrained, one gains the ability to define Functor instances, use Applicatives, ... No. Missing out the constraints is a craven surrender to the limitations in Haskell. Signatures/constraints should give maximum help to the compiler to accept only well-behaved programs. That limitation is because Functor, Applicative, etc are trying to keep backwards compatibility with H98 Prelude. One approach would be for their methods to have a signature with a type family defined constraint. Or the 'Partial Type Constructors' paper shows a possible approach -- which is really orthogonal to its main topic. AntC

2 3

Re: [Haskell-cafe] Recommended reading on non-algebraic types.
by Olaf Klinke 13 Sep '20

13 Sep '20

Dear Ignat, In the paper you linked to one should state more clearly that the two graph operations overlay and connect use an implicit equivalence relation between vertices of the two graphs involved. So these operations can be thought of as a traditional algebraic operation followed by a quotient. You might want to learn about domain semantics in general and domain environments in particular. Big names are Dana Scott and Gordon Plotkin, to name just two. Domain theory is the science of assigning (via a functor) an object of a category of partially ordered sets to each type of a (typed) lambda calculus and to each term of the calculus an arrow of that category. It turns out that algebraic domains are suitable for representing programs on algebraic data types. And if the category is just right and the lambda calculus is rich enough, then one can go the other way: Then you can prove that for each arrow in the category of domains there is a program that has that arrow as semantics. Algebraic domains match very nicely the way we build up complex data types via tuples, sums, function types and type recursion and how we build up functions via pattern matching and recursion. And every finite algebraic domain is a directed cycle-free graph. The little (free online) book by Thomas Streicher [1] might be a good start on domain semantics. A comprehensive mathematical theory of domains (not only algebraic ones) can be found in [2] but that book is expensive and hard to obtain. Sadly, with vanilla type systems such as Haskell's you can specify only algebraic domains. Anything beyond that is via "soft" definitions, meaning it can not be expressed in the type system, as you already observed. And domain theory provides mathematical proofs for this fact. Representing types like the prime numbers is possible with dependently- typed languages, but as far as I know these languages can also not go beyond algebraic domains, anyone please correct me if I'm wrong. Of course people have thought about representing other structures that are not algebraic domains. There are at least two ways I can think of: (1) What you call a sub-type: A subset of an algebraic domain. If the sub-type in question somehow sits "at the top" of the domain, then the surrounding algebraic domain is called a domain environment of the type in question. For example, the infinite binary tree is a domain environment of the type of infinite binary sequences. The important question to ask youself here is whether the sub-type is a computable one or not [*]. So if A is an algebraic data type, can you write a program that, given x :: A decides whether x is a member of the sub- type? For example, the sub-type of total functions A -> B is not a computable sub-type of the type of all functions A -> B for general A and B. (2) Quotients of algebraic domains. That means each element of your target type has several (maybe infinitely many) representations in an algebraic domain. This is fairly common. The Double data type has two representations for zero, because each Double value has a sign bit. If you want a set functor, take any container like [] or Seq and disregard multiplicities, so [x,y] and [x,y,y] represent the same set {x,y}. The art is then to write functions f that respect these quotients. Meaning if the values x and y both represent the same element in the quotient, then f(x) and f(y) represent the same element again. See section 4.2 in your linked paper on the problem of whether equivalence classes are computable. A stronger notion is a retract, that is a quotient map q :: A -> D together with a function e :: D -> A that embeds the type D back into the algebraic domain A such that q.e = id and q and e are adjoints. It is known that the retracts of algebraic domains are precisely the so- called continuous domains, a wide class that encompasses for example a real numbers object. Now you may also want to combine (1) and (2) and represent your data type as a quotient of a sub-set of an algebraic domain. As I see it your paper describes just that. It is still an open question whether certain continuous domains can be represented via expanding systems of finite domains, as is the case with algebraic domains [**]. My gut feeling is that such a description involves a description of quotients, but on another level: Since any quotient of a finite domain is algebraic, limits of such quotients will not take you beyond algebraic domains. Instead, one must describe what the quotient q :: A -> D does to the finite parts of A. Regards, Olaf [1] https://b-ok.org/book/768876/241ddb [2] Continuous lattices and domains, ISBN 0-521-80338-1 [*] One can prove that while there are uncountably many subsets of natural numbers, there are only countably many computable subsets in the sense that there exists a program that decides membership. [**] Give me any Haskell type and I show you the system of retractions of finite types whose limit is this type.

1 0

Recommended reading on non-algebraic types.
by Ignat Insarov 13 Sep '20

13 Sep '20

Hello Café. This is a request for reading. There is a huge literature on mathematics of program construction, but those are algebraic types therein considered; abstract types are hardly mentioned. At the same time, reality presents us with a range of compact mathematical constructions that are, however, not readily expressible via tagged unions, tuples and fixed points. A few examples: * The most usual `"containers" Data.Set (Set) ` is an abstract type that is not even lawful enough to be a functor. * It has been discovered that graphs can be represented by algebraic types _(see `alga` [1][1])_, but edge labels are, to my knowledge, not available. The types for graphs that have edge labels are all abstract. Coincidentally or not, the usual representations for the examples above are trees, refined with the use of smart constructors — so they are subtypes of algebraic types. There are less computationally accessible subtypes, say the type of prime numbers as a refinement of ℕ. So, my home baked theory is that abstract types represent subtyping in Haskell, so that every abstract type is a subtype of an algebraic type, matching a defining condition and equipped with a collection of constructors — functions whose range respects that condition. This means, for example, that: * Any projection of an algebraic type can be restricted to an abstract subtype for free. * There is a canonical partial one to one function from an algebraic type to its abstract subtype. Of course, we do not get anything like that in Haskell. Rather, we have _«abstract»_ abstract types, divorced from the underlying algebraic representation. As a consequence, we have only a handful abstract types in use, as each must be carefully crafted, verified and bundled with the totality of the interface — in a word, a bubble. By this point in my line of reasoning, I have to question if this fashion is justifiable. By now, the kind reader may concede that the matter is not without attraction. However, I am not aware of any prior art. For example, I wonder if there is a methodology for deciding if a given mathematical construction can be represented as an algebraic data type, and so far I have not seen this question being put forward. Please let me know if you have in mind some writing even faintly related to the line of inquiry presented above. [1]: https://github.com/snowleopard/alga-paper/releases/download/final/algebraic…

1 0

Re: [Haskell-cafe] Constraints as a moveable feast?
by Anthony Clayden 13 Sep '20

13 Sep '20

> on *Tue Sep 1 21:18:40 UTC 2020, Richard Eisenberg wrote:* > I see the core idea as a fairly straightforward generalization of the > "Partial Type Constructors" work -- except that I wouldn't phrase any of > this as "floating out". Thanks Richard, but no: I see this as exploring what was the idea in that brief example in the 1990 Report. (It's very vague, so we're all speculating.) The example there is a type synonym, which the PTC work doesn't consider. And putting the constraint syntactically before the type (synonym/data/new) name suggests to me it's 'outer'. GHC actually can express a bit what I mean by "floating out". I didn't realise that at the time of writing the O.P., so I'll rework the example. I'm correcting it because as you say: > In a few places, you've expanded Point a as Num a => (a, a). But Point a > is *not* the same thing as Num a => (a, a). Indeed, you didn't define it > that way. ... The library supplier writes: {#- LANGUAGE RankNTypes #-} type Num a => Point a = (a, a) -- proposed mkPoint :: a -> a -> Point a -- pretend to hide the constructor mkPoint x y = (x, y) -- no using numeric ops/no Num needed The compiler expands the synonym to mkPoint :: a -> a -> Num a => (a, a). Note no parens around the expansion, unlike my O.P. That expansion is not valid H98, but it is valid in GHC with RankNTypes. The docos say it's a Rank-1 type. GHC infers mkPoint :: Num a => a -> a -> (a, a) And that's why I call it "floating out". Longer example below. The idea is the library writer could later change the implementation to a datatype or a newtype, etc; or even add a further constraint. They all carry the constraint(s) 'outer'; the client code doesn't need to know about the change. > Instead, we should understand Point a to expand to (a, a) only when Num a holds. That might be a valid use case (especially for constrained classes/type families); but it's not the use case I have in mind. > So, the occurrence of Point a causes a Num a constraint to arise. > These Num a constraints then get put into the type. No floating. We all think the 1991 DatatypeContexts design is daft because it raises wanted constraints but doesn't "put" them anywhere, so the client-module programmer has to add them explicitly in signatures. To improve that, where/how should the compiler "put into the type"? The client writes scale :: a -> Point a -> Point a -- expand the synonyms; then float out and squish duplicates -- ===> scale :: a -> Num a => (a, a) -> Num a => (a, a) -- no parens added -- ===> scale :: Num a => a -> (a, a) -> (a, a) The 'no parens' step (different to my O.P.) is valid GHC with RankNTypes; the last step is as GHC infers today, with Num a floated out. (Or if you don't like that phrase: "canonicalises", "simplifies"?) > Note that types like `(Num a => a) -> a` and `Num a => a -> a` > (both very valid today) mean quite different things, Yes; although the first isn't valid H98/wasn't valid in 1990; and I'm struggling to think of a use case for it, noting there's no existential quant inside the parens. (It's not Rank-2, but is it plain Rank-1 or Rank-1-and-a-half?) Anyhoo that was an error on my part. > I think by rephrasing this without floating, we avoid the trouble with > existentials, etc., that you are worried about. I'm not sure on that, but we'll leave it for another day. > Personally, I would tack this onto "Partial Type Constructors" > instead of trying to make this happen independently, > but the two features would go nicely together. PTCs introduce a lot of heavy machinery; whereas I'm thinking of this as just-below-the-surface syntactic sugar that gets expanded before type inference. OTOH this doesn't on its own support `instance Functor Point`, treating the type synonym as an unapplied constructor -- which is what the Hughes 1999 paper is tackling. (I have an idea how that could go using this same syntactic expansion idea.) Note BTW, that I didn't add any constraints to the data constructors -- which is all the 1991 design does (and that not consistently). Constructing a `Point` doesn't need any Num ops/methods. But the type is supplying a wanted Num a 'outside', because any expression operating on a Point likely uses arithmetic. Constraints on data constructors (as with GADTs) I see as orthogonal: there will be use cases for one alone, the other alone, or both combined. AntC

2 2

Implementing parallelism using actors. How to improve the code.
by Luc Duponcheel 10 Sep '20

10 Sep '20

-- Hello, I am Luc Duponcheel. -- I started as a Haskell programmer, -- went to Java for a living, -- naturally evolved to Scala, -- and, being retired now, -- went back to my first love ... -- I am working on a library -- _______ __ __ _______ -- / ___ /\ / /\ / /\ / ___ /\ -- / /__/ / / _____/ / / / /_/__ / /__/ / / -- / _____/ / / ___ / / / ___ /\ /____ / / -- / /\____\/ / /__/ / / / /__/ / / \___/ / / -- /_/ / /______/ / /______/ / /_/ / -- \_\/ \______\/ \______\/ \_\/ -- v1.0 -- Program Description Based Programming Library -- author Luc Duponcheel 2020 - ... -- I started writing code in Scala (presented it at several conferences). -- I encountered issues with the fact that lazyness is not the default evaluation strategy. -- I switched to Haskell. -- In short: the library is about pointfree categorical programming -- (you may wish to have a look at ( https://www.youtube.com/watch?v=23VEcabMk7k (warning low sound volume)) -- below is some code with comments (you can load the code in ghci) -- it works fine but I want to get rid of the extra type class parameters x and w -- I tried to get rid of x and w in two ways -- . using forall -- . using a GADT -- -- both approaches failed -- -- the relevant code changes that I tried are commented out -- they are underneath the code that follows -- the code -- specifies parallelism -- and -- implements it using a dummy version of the hakka library -- (see https://hackage.haskell.org/package/hakka-0.2.0/docs/src/Hakka-Actor.html) -- first I need some language extensions {-# LANGUAGE TypeOperators #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE GeneralizedNewtypeDeriving #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE InstanceSigs #-} {-# LANGUAGE LambdaCase #-} {-# LANGUAGE GADTs #-} -- next I need some imports import Control.Monad.IO.Class import Control.Monad.Trans.Class import Control.Monad.Trans.State.Strict import Control.Monad.Trans.Cont -- next some useful generic code infixr `c` infixr `d` f `c` g = f . g (f `d` g) h = f `c` g h -- -- parallel specification -- -- note the extra type class parameters x and w -- type z && y = (z, y) class Parallel x w to where par :: (z `to` x) -> (y `to` w) -> (z && y) `to` (x && w) -- -- parallel implementation -- -- o msg stands for message -- o mnd stands for monad -- o rst stands for result -- -- -- three actors involved -- -- o reactor -- - reacts by using a continuation cont when both -- . an x result (at left) -- . a w result (at right) -- have been received -- -- o leftActor -- - acts to send an x result (at left) to reactor -- -- o rightActor -- - acts to send a w result (at right) to reactor -- -- reactor sends both leftActor and rightActor a message to let them act -- data ActorRef = ActorRef newtype ActorContext msg = ActorContext msg newtype ActorT msg mnd z = ActorT { runActorT :: StateT (ActorContext msg) mnd z } deriving (Functor, Applicative, Monad, MonadFail, MonadTrans, MonadIO) actor :: String -> (msg -> ActorT msg IO ()) -> ActorT msg IO ActorRef actor name messageHandler = undefined become :: (msg -> ActorT msg IO ()) -> ActorT msg IO () become messageHandler = undefined (!) :: ActorRef -> msg -> ActorT msg IO () actorRef ! message = undefined newtype ReactiveT msg rst mnd z = ReactiveT { runReactiveT :: ContT rst (ActorT msg mnd) z } deriving (Functor, Applicative, Monad, MonadFail, MonadIO) newtype KleisliT mnd z y = KleisliT { runKleisliT :: z -> mnd y } type ReactiveParallelT msg rst mnd = KleisliT (ReactiveT msg rst mnd) data Message x w = LeftReact x | RightReact w | LeftAct | RightAct type ReactiveActorBasedParallelT x w = ReactiveParallelT (Message x w) () IO runReactiveActorBasedParallelT = runContT `d` runReactiveT `d` runKleisliT instance Parallel x w (ReactiveActorBasedParallelT x w) where par z2x y2w = KleisliT (\case (z, y) -> ReactiveT (ContT (\cont -> actor "reactor" (\case LeftReact x -> become (\case RightReact w -> cont (x, w) ) RightReact w -> become (\case LeftReact x -> cont (x, w) ) ) >>= \reactorRef -> actor "leftActor" (\case LeftAct -> runReactiveActorBasedParallelT z2x z (\x -> reactorRef ! LeftReact x) ) >>= \leftActorRef -> actor "rightActor" (\case RightAct -> runReactiveActorBasedParallelT y2w y (\w -> reactorRef ! RightReact w) ) >>= \rightActorRef -> leftActorRef ! LeftAct >> rightActorRef ! RightAct ) ) ) -- class Parallel to where -- data Message = forall x. LeftReact x | forall w. RightReact w | LeftAct | RightAct -- data Message where -- LeftReact :: x -> Message -- RightReact :: w -> Message -- LeftAct :: Message -- RightAct :: Message -- type ReactiveActorBasedParallelT = ReactiveParallelT Message () IO -- instance Parallel (ReactiveActorBasedParallelT IO) where -- __~O -\ <, (*)/ (*) reality goes far beyond imagination

2 2

Re: [Haskell-cafe] Cannot update a field in a record with a polymorphic type.
by Olaf Klinke 10 Sep '20

10 Sep '20

I take it that in the expression (defaultY ∷ ∀ α. Monoid α ⇒ Y α) {y = "c"} the compiler is not smart enough to infer that the concrete value of α is irrelevant for the outcome and therefore rejects the program. The obligation here is to prove that the function λ x. x {y = "c"} :: ∀ α. Y α -> Y String is constant across all possible values of α, which I guess is undecidable for general one-parameter types? Or is there a free theorem saying that whenever a function has this general type signature, then the α cannot possibly be used? This certainly fails if Y has more type parameters that remain constant in the expression: A type class could distinguish the extra type parameters even if at the value level the result is constant across all α. Olaf

5 8