- Haskell-Cafe - Haskell.org

[ANN]: traverse-code
by David Feuer 28 Jan '22

28 Jan '22

I've put up a tiny little package[1], traverse-code, offering a generic way to "traverse" in Template Haskell's `Code m`. class TraverseCode t where traverseCode :: Quote m => (a -> Code m b) -> t a -> Code m (t b) I wrote this primarily as a way to "lift" operations on polymorphic data structures into Template Haskell. For example, for Data.Sequence, you can write triple :: a -> a -> a -> Seq a triple a b c = $$(sequenceCode $ fromList [ [||a||], [||b||], [||c||] ]) The `triple` function will not form its arguments into a list and then convert it to a sequence; rather, it will build the result sequence directly, using the underlying constructors. A generic default definition is available for all instances of Generics.Linear.Generic1. See linear-generics[2] for information about how to derive those. There's nothing particularly linear about traverse-code, but linear-generics has a more general Generic1 than GHC.Generics offers. [1] https://hackage.haskell.org/package/traverse-code [2] https://hackage.haskell.org/package/linear-generics

2 1

Munich Virtual Haskell Meeting, 2022-01-31 @ 19:30
by Leah Neukirchen 28 Jan '22

28 Jan '22

Dear all, Next week, our monthly Munich Haskell Meeting will take place again on Monday, January 31 on Jitsi at 19:30 CEST. **Due to the pandemic, this meeting will take place online!** For details see here: https://muenchen.haskell.bayern/dates.html A Jitsi link to join the room is provided on the page. Everybody is welcome, especially the Haskellers from Bavaria that do not usually come to our Munich meetings due to travel distance! cu, -- Leah Neukirchen <leah(a)vuxu.org> https://leahneukirchen.org/

1 0

Question about ambiguity and defaulting in recursive bindings
by Benjamin Redelings 26 Jan '22

26 Jan '22

Hi, I am trying to understand how GHC treats the following declaration. f c i = if i == 10 then c else g c 'b' g 'a' w = f 'b' 10 g z w = z l = (f 'a' (1::Int), f 'a' (1.0::Double)) It seems to me like, after defaulting, f should have the following type: Char -> Int -> Char However, looking at -ddump-tc, GHC is deriving the polymorphic type forall a. (Eq a, Num a) => Char -> a -> Char That's much nicer, because its more flexible. But I'm confused, because it looks like GHC is defaulting 'g', but not 'f', even though they are in the same recursive group. This seems to contradict "Typing Haskell in Haskell", which is what I am looking at right now. If that is correct, can anybody point me to a paper or documentation about how this works? More detail: 1. If I understand correctly, the definitions of `f` and `g` are mutually recursive, and should be typed together, and the declaration group is not restricted. 2. It seems like, before generalization, we have f :: Char -> a -> Char g :: Char -> Char -> Char Predicates include (Eq a, Num a) 3. Looking at the paper "Typing Haskell in Haskell" (THIH), it looks like the predicates (Num a, Eq a) should cause an ambiguity in the definition of g: * a is present in the definition of f, but not the definition of g * so the type (Eq a, Num a) => Char -> Char -> Char is ambiguous. * more generally, it seems like THIH treats any predicates with a type variable that is part of some, but not all, types in the declaration group to be ambiguous. Does this sound right? 4. Then, again following THIH, this ambiguous predicate should be defaulted to Int. I THINK this should lead to f :: Char -> Int -> Char g :: Char -> Char -> Char 5. However, I'm still not sure I'm understanding this right, because a few things still don't make sense: * First, THIH seems to eliminate the defaulted predicates without substituting a -> Int. But the type for f DOES mention `a`, so how can we avoid substituting? * Second, GHC accepts the code with no warnings or errors. There is some kind of defaulting going on, because GHC rejects the code if I add "default ()". Is there some way for GHC to default only g, but not f? I wonder if this involves a difference between Haskell '98 and Haskell 2010? I also wonder how much I should rely on THIH? Maybe the language has moved on since then? -BenRI

2 2

Recursive constraints with type families
by Dmitriy Matrosov 26 Jan '22

26 Jan '22

Hi. I've stumbled upon a simple problem with recursive type family: > {-# LANGUAGE RankNTypes #-} > {-# LANGUAGE KindSignatures #-} > {-# LANGUAGE TypeApplications #-} > {-# LANGUAGE TypeOperators #-} > {-# LANGUAGE PolyKinds #-} > {-# LANGUAGE TypeFamilies #-} > {-# LANGUAGE StandaloneKindSignatures #-} > {-# LANGUAGE ScopedTypeVariables #-} > {-# LANGUAGE UndecidableInstances #-} > > import GHC.TypeLits > import Data.Proxy > import Data.Kind > > type C :: Nat -> Constraint > type family C x where > C 0 = KnownNat 0 > --C x = (KnownNat x, C (x - 1)) > C x = (KnownNat x, C 0) > --C x = KnownNat x > > --type C2 x = (KnownNat x, C2 1) > > showNat :: forall (n :: Nat). C n => Proxy n -> String > showNat _ = show $ natVal (Proxy @n) and the error is Prelude> :r [1 of 1] Compiling Main ( constraint-type-family.lhs, interpreted ) constraint-type-family.lhs:31:22: error: • Could not deduce (KnownNat n) arising from a use of ‘natVal’ from the context: C n bound by the type signature for: showNat :: forall (n :: Nat). C n => Proxy n -> String at constraint-type-family.lhs:30:3-56 Possible fix: add (KnownNat n) to the context of the type signature for: showNat :: forall (n :: Nat). C n => Proxy n -> String • In the second argument of ‘($)’, namely ‘natVal (Proxy @n)’ In the expression: show $ natVal (Proxy @n) In an equation for ‘showNat’: showNat _ = show $ natVal (Proxy @n) | 31 | > showNat _ = show $ natVal (Proxy @n) | ^^^^^^^^^^^^^^^^^ If i write just C x = KnownNat x everything works fine. I guess, the reason is UndecidableInstances, but why and then, how can i build constraints recursively and make it work? Thanks. PS. Initially, this 'showNat' was something like countDown :: forall (n :: Nat). C n => Proxy n -> String countDown _ = let x = natVal (Proxy @n) in if x > 0 then show x ++ countDown (Proxy @(n - 1)) else "end" but it does not work.

4 6

Missing feature of Coercible, or necessary caution?
by Tom Ellis 25 Jan '22

25 Jan '22

Consider the following program. {-# LANGUAGE TypeApplications #-} import Data.IntMap (IntMap, mapKeysMonotonic, Key) import Data.Coerce (coerce) newtype MyMap = MyMap (IntMap Bool) doesn'tWork :: (Key -> Key) -> MyMap -> MyMap doesn'tWork = coerce mapKeysMonotonic works :: (Key -> Key) -> MyMap -> MyMap works = coerce (mapKeysMonotonic @Bool) mapKeysmonotonic has type (Key -> Key) -> IntMap a -> IntMap a and we attempt to coerce it to type (Key -> Key) -> MyMap -> MyMap since MyMap is a newtype around IntMap Bool this ends up generating the constraint Coercible a Bool and there is no way to specify that constraint given that a doesn't otherwise appear in the top-level type. Hence doesn'tWork will not type check. If I force the type of a to be Bool using a TypeApplication then it does type check (works). But is this a missing feature of GHC's Coercible system? Since a is not otherwise constrained is it not valid for GHC to choose it to be Bool ? Coercible instances contain now observable content so no observable behaviour could depend on the particular choice of Coercible a Bool instance, and choosing a ~ Bool is the natural one. Is there some violation of type safety or otherwise broken behaviour that could arise from choosing arbitrary Coercible instances on type variables that are not otherwise constrained? Tom

2 2

Guards on variable bindings
by Tom Ellis 24 Jan '22

24 Jan '22

According to GHC there are multiple declarations of bar, but not of foo. I don't understand. Why is it not valid to have multiple clauses for a variable binding? Tom bar | False = () bar = () foo _ | False = () foo _ = ()

2 4

why OverloadedTuples extension is missing?
by Daneel Yaitskov 17 Jan '22

17 Jan '22

Cafe, There is a group of GHC extensions and complementary classes to make writing Haskell code a bit sweeter such as: - {} - Num (fromIntegral) - OverloadedStrings - IsString - OverloadedLists - IsList So I have an inductive question - why there is no OverloadedTuples? I haven't found a discussion thread about this topic. I could imagine following tuple syntax interpretation: {-# LANGUAGE OverloadedTuples #-} data Foo = FooA Int String | FooB String Foo deriving (Show, Eq, IsTuple) mkFoo :: Foo mkFoo = (1, "hello") mkFoo2 :: Foo mkFoo = ("abc", (1, "hello")) Sometimes expected type name is known without data constructor. So such expression is more concise. -- Best regards, Daniil Iaitskov

8 7

Newbie question
by Terry Phelps 16 Jan '22

16 Jan '22

I'm trying yet again to "get" Haskell. I'm reading Graham Hutton's book "Programming in Haskell", and am working on one of the exercises. Sounds easy enough: Make a function 'last' that returns the last element of a non-empty list. After struggling a while, I looked at the answer: last = head . reverse. I wish I had thought of that. But I kept trying to get my recursive version done, but I can't seem to make ghci happy. (Version 8.10.5, if you care). I wrote: last [] = [] (Yes, I know that's not a non-empty list, but I don't want ghci whining about non-exhaustive patterns). Then I added: last [x] = x And I checked the type: :t last last:: [a] -> [a] Yes, that looks right. There seems to be only one other case: 2 or more elements. So I wrote: last (x:y:xs) = last (y:xs) I ran it: Prelude> last [1,2] *** Exception: <interactive>:2:1-27: Non-exhaustive patterns in function last What the heck is the problem? I've covered every possible list, haven't I? Stranger yet, I check the type again: Prelude> :t last last :: [a] -> t The type has changed. And I don't understand what it means. What's the 't'? I'm sure this is a simple beginner error, but I'm really confused. I don't see how it isn't exhaustive, and I don't see why the 3rd clause (or whatever it's called) caused the type to change. Someone help, please.

5 6

TFPIE 2022: moving to online and extension to Feb 7th
by Elena Machkasova 14 Jan '22

14 Jan '22

Due to rescheduling of the Lambda Days because of COVID, TFPIE, together with TFP, will be held virtually on March 16th 2022, together with TFP which will be held on March 17-18. There is an optional opportunity to present at the Lambda Days July 28-29 2022 in addition to the virtual presentation in March. Updated TFPIE 2022 Call for papers: https://wiki.tfpie.science.ru.nl/TFPIE2022 The submission deadline is extended to February 7th 2022. TFPIE 2022 welcomes submissions describing techniques used in the classroom, tools used in and/or developed for the classroom and any creative use of functional programming (FP) to aid education in or outside Computer Science. Topics of interest include, but are not limited to: FP and beginning CS students FP and Computational Thinking FP and Artificial Intelligence FP in Robotics FP and Music Advanced FP for undergraduates FP in graduate education Engaging students in research using FP FP in Programming Languages FP in the high school curriculum FP as a stepping stone to other CS topics FP and Philosophy The pedagogy of teaching FP FP and e-learning: MOOCs, automated assessment etc. Best Lectures - more details below In addition to papers, we are requesting best lecture presentations. What's your best lecture topic in an FP related course? Do you have a fun way to present FP concepts to novices or perhaps an especially interesting presentation of a difficult topic? In either case, please consider sharing it. Best lecture topics will be selected for presentation based on a short abstract describing the lecture and its interest to TFPIE attendees. The length of the presentation should be comparable to that of a paper. In addition, the speaker can provide commentary on effectiveness or student feedback. Submissions Potential presenters are invited to submit an extended abstract (4-6 pages) or a draft paper (up to 20 pages) in EPTCS style. The authors of accepted presentations will have their preprints and their slides made available on the workshop's website. Papers and abstracts can be submitted via easychair at the following link: https://easychair.org/conferences/?conf=tfpie2022 After the workshop, presenters are invited to submit (a revised version of) their article for the formal review. The PC will select the best articles for publication in the Electronic Proceedings in Theoretical Computer Science (EPTCS). Articles rejected for presentation and extended abstracts will not be formally reviewed by the PC. Important Dates (updated) Submission deadline: *February 7th* 2022, Anywhere on Earth. Notification: *February 11th* 2022 (Note: earlier submissions will receive earlier response) TFPIE Registration Deadline: TBA Workshop: *March 16* 2022 Submission for formal review: *April 29th* 2022, Anywhere on Earth. Notification of full article: June 1st 2022 Camera ready: July 1st 2022 Program Committee Peter Achten, Radboud University, Netherlands Stephen Chang, University of Massachusetts Boston, USA John Hughes, Chalmers University of Technology, Sweden Elena Machkasova (Chair) - University of Minnesota Morris, USA Kristina Sojakova - INRIA, Paris, France Melinda Tóth, Eötvös Loránd University, Budapest, Hungary Keynote speaker: Our keynote talk is "The perfect Functional Programming course" by Peter Achten. Registration information: TFPIE will take place virtually on March 16 2022, together with TFP which will be held on March 17-18. Registration information will be announced shortly. There is no registration fee. Registration and online attendance are mandatory for at least one author of every paper that is presented at the workshop. Only papers that have been presented at TFPIE may be submitted to the post-reviewing process. -- Dr. Elena Machkasova Associate Professor of Computer Science Division of Science and Mathematics University of Minnesota, Morris Office: Sci 2325 (320) 589-6308 http://cda.morris.umn.edu/~elenam/ Pronouns: she/her/hers or any other

1 0

Postdoc positions on Formal Verification for Zero-Trust IoT Systems at Kyoto University and National Institute of Informatics (NII), Japan
by Taro Sekiyama 14 Jan '22

14 Jan '22

[Please distribute, apologies for multiple postings.] Dear All, We are seeking a few postdoc researchers, who works for a project “Zero-Trust IoT Systems by Collaboration of Formal Verification and System Software” by Japan Science and Technology Agency. We'd be grateful if you could spread the word to interested candidates. * Project Description The project aims at the construction of formally verified secure IoT systems that follow the concept of “zero trust architecture”, dubbed ZT-IoT systems. It consists of four research teams and two teams, led by Atsushi Igarashi, Kyoto University, Japan and Taro Sekiyama, National Institute of Informatics, Japan (NII) are investigating applications of formal verification or programming language techniques to the construction of secure IoT systems. The main research topic of Igarashi’s team is centered around the design and theory of security policy engines for ZT-IoT systems, inclucing the design of a language to describe security policies and policy enforcement algorithms and the techniques for verifying policy enforcement algorithms against given security policies. Other team members are Kohei Suenaga and Masaki Waga at Kyoto University. The main research topic of Sekiyama’s team is centered around techniques for monitoring and intervention for ZT-IoT systems. Other team members include Ichiro Hasuo and Shin-ya Katsumata at NII. Although the two teams are based in different places, we collaborate closely with each other. The appointment can start as early as April 2022 (the starting date is negotiable). The contract will initially run until the end of March 2023, with the possibility of annual renewal until the end of the project, which is March 2027 at maximum. Salary will be about 360,000–550,000 JPY/month. Applicants should have a Ph.D in computer science or related fields, and have a strong background in formal verification and/or programming language theory. Due to the project’s nature, they are required to have strong interests in applying theory to practice; they should also be (self-)motivated, dedicated, and able to work both independently and collaboratively. Strong communication skills in oral and written English are required. * Workplace Members of Igarashi’s team will work at Kyoto University, Kyoto, Japan and members of Sekiyama’s team will work at NII, Tokyo, Japan. (Living costs in Japan are not very high nowadays. An estimate is found here https://www.internations.org/go/moving-to-japan/living/the-cost-of-living-i… and we find rent can be cheaper than the cited amount.) * Applications and inquiries Inquiries can be sent to application-zt-iot [at] fos.kuis.kyoto-u.ac.jp, with the subject CREST Job Inquiry. Feel free to ask us any questions on relevance, topics, compensation, etc. We will reply when we see enough relevance. Applications should be made electronically via the following JREC-IN Portal web sites. NII: https://jrecin.jst.go.jp/seek/SeekJorDetail?fn=3&ln=1&id=D122010021&ln_jor=1 Kyoto: https://jrecin.jst.go.jp/seek/SeekJorDetail?fn=3&ln=1&id=D121122219&ln_jor=1 Please upload a pdf including - your brief CV, - short description of research interests (can be very informal and short), - the list of papers (a dblp or Google scholar link will do, for example), - a couple of representative papers (in pdf), and - (preferably) the contact of two references. We will contact you for further material and interview, provided that we find sufficient relevance in your application. Starting dates are negotiable. The positions will remain open until filled. Many thanks, Taro.

1 0