- Haskell-Cafe - Haskell.org

Re: [Haskell-cafe] ANN: haskell for mathematicians
by Olaf Klinke 10 Apr '22

10 Apr '22

>Dear Olaf, > >On Sat 09 Apr 2022 10:45:56 PM GMT, Olaf Klinke wrote: >> my monograph "Haskell for Mathematicians" has found a home online: >> https://hub.darcs.net/olf/haskell_for_mathematicians > >I just had a first look, your monograph looks awesome! Thank you for >sharing! > >In haskell_for_mathematicians.tex, you mention as a further idea that >Hask is like a Heyting algebra. Could you elaborate on that point? Are >you thinking of types as propositions here? > >Cheers, >Ingo Hi Ingo, Types as propositions is dealt with in haskell_for_logicians.lhs. Hask has an arrow that is a right adjoint, just like a Heyting algebra. It is less clear, however, whether the the arrow gives rise to a partial order as it does in Heyting algebras. I am interested in the complete Heyting algebras, a.k.a. frames a.k.a. locales. Many concepts in point-free topology heavily rely on partial orders and lattice theory, so without a good analogue I would not dare declare a similarity. For example, in a Heyting algebra x <= y iff x -> y equals the top element. But then, what is the top element of Hask? Do we declare x <= y if x -> y is inhabited? That seems to collapse all inhabited types. In a future chapter I would like to tell a story around this: In point-free topology (locale theory), there are several inter-definable concepts of sub-object. One of them is a "nucleus", that is an endo-function j with the following properties. x <= y implies j(x) <= j(y) (j is a functor) x <= j(x) (return :: x -> j x) j(j(x)) <= j(x) (join :: j (j x) -> j x) j(x) /\ j(y) <= j(x /\ y) (liftM2 (,) :: j x -> j y -> j (x,y)) In other words: sub-objects of point-free spaces are (strong) monads. In that respect, every monad j is a sub-object of Hask, and indeed it is: It defines the sub-category (Kleisli j). There are more analogues: The identity function is a nucleus and corresponds to the greatest sub-object, and in Hask (Kleisli Identity) is the largest Kleisli category. Nuclei can not be combined easily, and neither can monads. Another interesting question is: What are the "points" of Hask? A point of a locale is a mapping from opens (types of Hask) to Bool that preserves finite products and arbitrary coproducts, where True is considered as the empty product and False as the empty coproduct. How many of such mappings can be defined in Haskell? How would we implement them? As a class? Type family? GADT? The funny thing about locales is that one can have few or no points but still a rich supply of sub-objects. Olaf

2 1

ANN: haskell for mathematicians
by Olaf Klinke 09 Apr '22

09 Apr '22

Dear Café, my monograph "Haskell for Mathematicians" has found a home online: https://hub.darcs.net/olf/haskell_for_mathematicians The intended audience of this course is mathematicians. While there are many (and excellent) introductions and complete books on Haskell available, most of them target programmers. But Haskell, despite being practically useful, is very good at modelling certain branches of mathematics. The aim of this course is to supplement the pen-and-paper mathematics with a more palpable, more interactive variant of exploring mathematical concepts. Each chapter contains exercises and is a self-contained literate haskell file that requires no package dependencies other than those included in a basic Haskell installation. Selected goodies you can find in Haskell for Mathematicians: * Constructive topology via domain semantics of Haskell * Let the compiler verify theorems of intuitionistic logic * Two implementations of exact real numbers: signed-digit and Conway's surreal numbers * Categories (of course!) * Detailed discussion of mathematical properties of monads such as commutative and affine monads * Detailed derivation of a probability measure monad that is actually affine (unlike sampling-based ones) Please use the darcs issue tracker for reporting typos, strange wording or incaccuracies. Also please don't hesitate to point me to existing work that might be worth mentioning or incorporating in the monograph. Cheers Olaf

3 2

Utrecht Summer School on Advanced Functional Programming 2022
by Swierstra, W.S. (Wouter) 08 Apr '22

08 Apr '22

# Call for Participation SUMMER SCHOOL ON ADVANCED FUNCTIONAL PROGRAMMING Utrecht, the Netherlands, 04 July – 08 July 2022 http://www.afp.school ## ABOUT The Advanced Functional Programming summer school has been running for more than ten years. We aim to educate aspiring Haskell programmers beyond the basic material covered by many textbooks. After running remotely for the past two years, we're thrilled to announce that this year's edition will take place on site in Utrecht. We are monitoring the pandemic closely - and will make contingency plans if we cannot meet in person; at the moment, we do not have plans for remote participation. The lectures will cover several more advanced topics regarding the theory and practice of Haskell programming, including topics such as: * lambda calculus; * monads and monad transformers; * lazy evaluation; * generalized algebraic data types; * type families and type-level programming; * concurrency and parallelism. The summer school consists of a mix of lectures, labs, and a busy social program. ## LECTURERS * Gabriele Keller * Trevor McDonell * Wouter Swierstra ## PREREQUISITES We expect students to have a basic familiarity with Haskell already. You should be able to write recursive functions over algebraic data types, such as lists and trees. There is a great deal of material readily available that covers this material. If you've already started learning Haskell and are looking to take your functional programming skills to the next level, this is the course for you. ## DATES Soft registration deadline: 24 June, 2022 School: 04 July – 08 July 2022 ## COSTS 750 euro - Profession registration only 250 euro - Student registration fee 200 euro - Housing fee We will charge a registration fee of 750 euros (or 250 euros for students) to cover our expenses. If this is problematic for you for any reason at all, please email the organisers and we can try to offer you a discounted rate or a fee waiver. We have a limited number of scholarships or discounts available for students that would not be able to attend otherwise, especially for women and under-represented minorities. ## FURTHER INFORMATION Further information, including instructions on how to register, is available on our website: http://www.afp.school

1 0

Typechecker complains about untouchable types
by rowan goemans 07 Apr '22

07 Apr '22

Hello everyone, I'm running into a type error I don't quite understand why it's happening. Consider this type class and function: ``` class KnownNat n => F (n :: Nat) foo :: forall n. F n => (F n => Proxy n -> Proxy n) -> Int foo f = let _ = f (Proxy @n) in 0 ``` This typechecks with no issues. But once I add an LTE constraint to the type class it won't typecheck and complains about an untouchable type. ``` class (KnownNat n, 1 <= n) => F (n :: Nat) foo :: forall n. F n => (F n => Proxy n -> Proxy n) -> Int foo f = let _ = f (Proxy @n) in 0 ``` with this error: ``` test.hs:11:8: error: • Could not deduce (F n0) from the context: F n bound by the type signature for: foo :: forall (n :: Nat). F n => (F n => Proxy n -> Proxy n) -> Int at test.hs:11:8-58 The type variable ‘n0’ is ambiguous • In the ambiguity check for ‘foo’ To defer the ambiguity check to use sites, enable AllowAmbiguousTypes In the type signature: foo :: forall n. F n => (F n => Proxy n -> Proxy n) -> Int | 111 | foo :: forall n. F n => (F n => Proxy n -> Proxy n) -> Int | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ test.hs:11:8: error: • Couldn't match type ‘n0’ with ‘n’ ‘n0’ is untouchable inside the constraints: F n0 bound by a type expected by the context: F n0 => Proxy n0 -> Proxy n0 at test.hs:11:8-58 ‘n’ is a rigid type variable bound by the type signature for: foo :: forall (n :: Nat). F n => (F n => Proxy n -> Proxy n) -> Int at test.hs:11:8-58 Expected type: Proxy n0 -> Proxy n0 Actual type: Proxy n -> Proxy n • In the ambiguity check for ‘foo’ To defer the ambiguity check to use sites, enable AllowAmbiguousTypes In the type signature: foo :: forall n. F n => (F n => Proxy n -> Proxy n) -> Int | 111 | foo :: forall n. F n => (F n => Proxy n -> Proxy n) -> Int | ^^^^^^^^^^^^^^^^^^^^ ``` Interestingly adding an equality constraint on `n` does also work: ``` class (KnownNat n, 1 ~ n) => F (n :: Nat) foo :: forall n. F n => (F n => Proxy n -> Proxy n) -> Int foo f = let _ = f (Proxy @n) in 0 ``` Anyone have any clue what is going on here? Best regards, Rowan Goemans

3 2

[ANN] Jacinda 1.0.0.0 - a functional text processing language complementing sed, awk, etc.
by Vanessa McHale 07 Apr '22

07 Apr '22

Hi all, I have released the 1.0.0.0 version of Jacinda, an expression-oriented text processing language for the command-line. You can find it here (Linux, mainly): https://github.com/vmchale/jacinda/releases/tag/1.0.0.0 Cheers, Vanessa McHale

2 1

RFC: removing “alternative installation methods” from haskell.org (or finding them owners)
by Tom Ellis 04 Apr '22

04 Apr '22

The Haskell.org committee is considering removing the "alternative installation options" section from the [downloads page of haskell.org](https://www.haskell.org/downloads/) and we seek the opinion of the community. If you would like to share your opinion we prefer that you do so [on the haskell.org issue tracker](https://github.com/haskell-infra/www.haskell.org/issues/170), but failing that, in this email thread is fine too. ### Background The [downloads page of haskell.org](https://www.haskell.org/downloads/) suggests using ghcup and stack to obtain a toolchain. These two tools are widely used in the community, actively maintained and kept up-to-date. The page also provides a number of "alternative installation options" (see below, or on the page itself, for the list). The Haskell.org committee does not have the resources to ensure that these alternative installation options are kept maintained and confirmed working. We don't even know if anyone uses them. Anyone who uses them is likely to be an "advanced user" anyway, since they require more expertise to implement. stack and ghcup presumably work well on all those platforms, are the most well-maintained installation options and most suitable for beginners. ### Possibilities We have a couple of options: 1. Remove all the alternative installation options. 2. Keep (some of) the alternative installation options and find community volunteers to maintain them. The volunteers will be responsible for ensuring verifying on a regular basis that their instructions are still working, submitting timely corrections when necessary, and responding promptly on the issue tracker to questions about their installation instructions. ### What we would like from you * Please share your opinion about removing the alternative installation options, especially if you are a user of one of them! * If you are willing to maintain an alternative installation option, please speak up! ### Current alternative installation options * Linux Ubuntu (confusing (see https://github.com/haskell-infra/www.haskell.org/issues/16) and probably outdated) * Linux Debian (links to https://downloads.haskell.org/~debian/ which doesn't support Debian 11 Bullseye) * Linux Fedora * Linux EPEL for RHEL/CentOS/etc * Linux Arch * Linux openSUSE Leap * Linux openSUSE Tumbleweed * Linux Gentoo * Windows Chocolatey

11 32

Model beverage
by Daneel Yaitskov 04 Apr '22

04 Apr '22

Hi List, I came to Haskell from Java. At the beginning I was trying to map traditional notions of mainstream languages onto the FP world as “How to replace inheritance and late binding?”, etc. If Java developers drink coffee, then what is the model beverage for haskellers? “Psyllium Husk” fits the role, because besides phonetic similarities, the beverage is lazy (the recipe is simple - mix powder with water) and immutable (goes through the intestinal tract largely unaltered). Plus it is far off mainstream. -- Best regards, Daniil Iaitskov

2 1

Default http2 library to use for client side?
by Ruben Astudillo 04 Apr '22

04 Apr '22

Hello Cafe I have been looking at hackage on what is the status for http2 **client** libraries. I haven't be able to grasp what is the default or recommended solution on this space. So far I have gotten the following impressions: 1. The usual candidates such as req / wreq libraries don't seem to support it. This is caused by they being based on `http-client`. 2. There is an http2-client [1] library that fits the bill. It uses Kazu's http2 [2] underneath, but it is upper bounded to major version 2 of that library. Kazu's library is now at major version 3 and it cannot be made to use the updated version easily. 3. Kazu's http2 library on major version 3 has a module called Network.HTTP2.Client which is even more low-level than what the previous option provided but it seems recently developed. It has a code sample. 4. Haskellers are not that interested on client side http2. I am no expert on this protocol, but it seems that there is some compatibility on it where you can make an http1.1 call and the server will handle it transparently (don't quote me on this). But Haskellers certainly were (are?) excited for http2 server support on warp which landed around 2015-2016. I have concluded that using `http2` [2] with the client module as my best bet. Is this analysis correct? or should I be looking a other packages that I haven't considered? Thanks for you time reading this email. [1]: <https://hackage.haskell.org/package/http2-client> [2]: <https://hackage.haskell.org/package/http2> -- Rubén. (pgp: 1E88 3AC4 89EB FA22)

1 0

Re: [Haskell-cafe] Model beverage
by Olaf Klinke 03 Apr '22

03 Apr '22

>Well if that's the path we're going down, consider: > >Mushroom tea. > >It will take you outside of time, make you contemplate infinity, and take >your thoughts in abstract directions few other experiences can prepare >you >for; but in the end you come away surprisingly refreshed! > I'd rather reserve that one for dependently-typed languages. ;-) But it shows once more how biased we Europeans are towards alcoholic drugs. Olaf >On Sat, Apr 2, 2022, 9:00 AM Olaf Klinke <olf(a)aatal-apotheke.de> wrote: > >> Absinthe comes to mind. It is very potent, popular among >> philosophers but >> drives you crazy if consumed regularly, in large quantities.

1 0

Fully Funded PhD Positions in the Safety and Security of Advanced Systems Group (Exeter, UK, Deadline 2022-04-29)
by Achim D. Brucker 03 Apr '22

03 Apr '22

We have two fully funded PhD scholarships for UK applicants in the Security and Trust of Advanced Systems Group [1] (Prof. Achim Brucker [2] and Dr. Diego Marmsoler [3]) at the Department of Computer Science of the University of Exeter, UK [4]. We are looking for enthusiastic and outstanding Computer Science or Mathematics students with a strong background in at least one of the following topics: * safety or security of (software) systems, * formal modelling or formal reasoning/verification, * program analysis or program verification, * language-based security, * semantics of programming languages, * theorem proving, model checking, * cryptographic protocols, * distributed systems (e.g., blockchain), * software security, * cyber-physical systems, * specification-based testing, and * design and implementation of security architectures. The positions offer the flexibility to define the PhD topic jointly between the successful candidate and the supervisors. Interested candidates should contact the potential supervisor Prof. Achim Brucker (a.brucker(a)exeter.ac.uk) or Dr. Diego Marmsoler (d.marmsoler(a)exeter.ac.uk) to discuss their application. For more details, please consult the official advertisements: * Compositional Verification of Smart Contracts in Isabelle: https://www.exeter.ac.uk/study/funding/award/?id=4326 * Formal Verification for Safety- or Security-Critical Systems: https://www.exeter.ac.uk/study/funding/award/?id=4328 The closing date for applications is midnight on the 29th April 2022. Best, Achim and Diego [1] http://emps.exeter.ac.uk/computer-science/research/cyber-security/ [2] https://www.brucker.ch/ [3] https://marmsoler.com/ [4] http://emps.exeter.ac.uk/computer-science/ -- Prof. Achim Brucker | Chair in Cybersecurity & Head of Group | University of Exeter https://www.brucker.ch | https://logicalhacking.com/blog @adbrucker | @logicalhacking

1 0