- Haskell-Cafe - Haskell.org

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 14 Sep '20

14 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 11 Sep '20

11 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

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

10 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 Ah. Now I see a bit more of what you're getting at. We want as if the type synonym were an associated type family with a most-general instance class Num a => CPoint a where type Point a instance Num a => CPoint a where type Point a = (a, a) The semantics to be as the PTC paper, such that expanding `Point a` always requires a `CPoint a` instance, which will in turn want a `Num a`. And the expansion to be immediate (as with type synonyms) so that the client can put `Point a` in instance heads, for example. > But I really don't know what it means to expand without adding parens. ... what about > *pointX :: Point a -> a* *> ... *We don't want that type to expand to (Num a => (a, a)) -> a Ok, it was your using fancy type operators that put me off. We can represent the AST (and show the need for parens) by reverting to prefix syntax, within H98: pointX :: (->) (Point a) a -- needs parens around (Point a) And yes my naieve syntactic expansion would give the type you show, wot we do not want. AntC

1 0

Counterintuitive ScopedTypeVariables behaviour
by Tom Ellis 09 Sep '20

09 Sep '20

I have just noticed that with ScopedTypeVariables one can write the following bizarre definition -- Inferred signature: -- add :: Num a => a -> a -> a add (x :: a) (y :: b) = x + y The reason for this behaviour is that > in all patterns other than pattern bindings, a pattern type > signature may mention a type variable that is not in scope; in this > case, the signature brings that type variable into scope. https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_ext… and the justification is that > Bringing type variables into scope is particularly important for > existential data constructors But this leads to a rather puzzling user experience. Was it really not possible to design this extension in a way that would allow bringing new type variables into scope locally but not allow them to unify with other type variables from outer scopes? To be more concrete, what I would like to see is a design where `k` is allowed because the type `a` (bound within a pattern) does not need to unify with anything but `k2` is not allowed because `a` is forbidden to unify with `b`. `k3` would also be forbidden (the type variables called `a` are actually distinct) as would `k4` (the type variable for the inferred signature would be fresh and distinct from `a`). I believe this design might lead to much less puzzling behaviour. Would it be possible (within a new extension, of course) or have I overlooked something? Tom data T = forall a. MkT [a] k :: T -> T k (MkT [t::a]) = MkT t3 where (t3::[a]) = [t,t,t] data T2 a = MkT2 [a] k2 :: T2 b -> T2 b k2 (MkT2 [t::a]) = MkT2 t3 where (t3::[a]) = [t,t,t] k3 :: T2 a -> T2 a k3 (MkT2 [t::a]) = MkT2 t3 where (t3::[a]) = [t,t,t] k4 (MkT2 [t::a]) = MkT2 t3 where (t3::[a]) = [t,t,t]

5 13

Cannot update a field in a record with a polymorphic type.
by Ignat Insarov 07 Sep '20

07 Sep '20

Hello. I have a problem trying to do something very simple. Consider this conversation with GHC: λ data Y α = Y {y ∷ α} λ defaultY = Y {y = mempty} λ :type defaultY defaultY :: Monoid α => Y α λ :type defaultY {y = "c"} ∷ Y String <interactive>:1:1: error: • Ambiguous type variable ‘α0’ arising from a use of ‘defaultY’ prevents the constraint ‘(Monoid α0)’ from being solved. Probable fix: use a type annotation to specify what ‘α0’ should be. These potential instances exist: instance Monoid a => Monoid (IO a) -- Defined in ‘GHC.Base’ instance Monoid Ordering -- Defined in ‘GHC.Base’ instance Semigroup a => Monoid (Maybe a) -- Defined in ‘GHC.Base’ ...plus 7 others (use -fprint-potential-instances to see them all) • In the expression: defaultY In the expression: defaultY {y = "c"} :: Y String Why does this not work?

4 5

call tree of cost centers in a .prof file
by Marco Zocca 06 Sep '20

06 Sep '20

Hi all, I don't understand the tree-shaped visualizations produced by profiteur, profiterole and ghc-prof-flamegraph . Specifically, I initially thought that cost centers that are displayed closer to the leaves would be due to calls higher up in the tree, but that doesn't seem to be the case. Example; I've produced this basic visualization with ghc-prof and Data.Tree.drawTree (which mirrors qualitatively what flamegraph et al. produce) : MAIN 100.0 | +- Main.trained 100.0 | | | +- ER.ML.Classification.logreg 99.2 | | | | | +- ER.ML.Classification.irls 96.4 | | | | | | | +- ER.ML.Classification.hessianC 30.3 | | | | | | | | | +- ER.Math.Matrix.outerD 30.3 | | | | | | | | | | | `- Main.binMixtureData 29.8 | | | | | | | | | | | +- ER.Math.Random.SplitMix.mvNormalSM 28.8 | | | | | | | | | | | | | `- ER.Math.Matrix.matVec 28.2 | | | | | | | | | | | `- ER.ML.Common.centerDataWMEC 1.0 It looks fine down to level 4 (trained calls logreg, which calls irls, which calls hessianC, which calls outerD), and then it stops making sense (binMixtureData is not ever called by outerD). Could someone please shed some light on this? Thank you in advance

2 1