- Haskell-Cafe - Haskell.org

Re: [Haskell-cafe] RFC: "Native -XCPP" Proposal
by Johannes Waldmann 07 May '15

07 May '15

There is maybe another option: do what csharp does. Define a reduced "preprocessor" (for conditional compilation, but without macro expansion) as part of the language. (cf. https://msdn.microsoft.com/en-us/library/ed8yd1ha.aspx ) They must have have had good reasons for doing it this way. - J.W. PS: I was trying to add a proper reference (to the language spec) but this seems hard. It is Section 9.5 of ECMA-334. For viewing the newer specs, it seems you need to have MS-Word or VS installed. See also http://stackoverflow.com/questions/13467103/

7 6

Re: [Haskell-cafe] minor confusion over kinds....
by Nicholls, Mark 07 May '15

07 May '15

lets try it the other way around > instance Foo' SNat1 where > type Bar' SNat1 = Z1 > bar' = SZ1 that works! (my language will be wrong here...but the jist is) So in some something of kind "*->*" is substitutable for a parameter of kind "k -> *" "Nat->*" is substitutable for a parameter of kind "k -> *" "*->*" is substitutable for a parameter of kind "* -> *" "Nat->*" is NOT substitutable for a parameter of kind "* -> *" Hmmmm So why would I ever want to define a type class of kind (* -> *) -> Constraint Instead of (k -> *) -> Constraint ? I think I don't completely understand what's going on. From: Nicholls, Mark Sent: 06 May 2015 1:02 PM To: haskell-cafe(a)haskell.org Subject: minor confusion over kinds.... And what "*" means as opposed to other things e.g. an explicit name "Nat" or a kind variable "k" > {-# LANGUAGE DataKinds #-} > {-# LANGUAGE ExplicitForAll #-} > {-# LANGUAGE FlexibleContexts #-} > {-# LANGUAGE FlexibleInstances #-} > {-# LANGUAGE GADTs #-} > {-# LANGUAGE MultiParamTypeClasses #-} > {-# LANGUAGE PolyKinds #-} > {-# LANGUAGE StandaloneDeriving #-} > {-# LANGUAGE TypeFamilies #-} > {-# LANGUAGE TypeOperators #-} > {-# LANGUAGE UndecidableInstances #-} what I want is a typeclass with instances of type level Naturals here's the class, the parameter is of kind (* -> *) i.e. a is some sort of wrapper that maps from types to values > class Foo (a :: * -> *) where > type Bar a > bar :: a (Bar a) lets ignore DataKinds define Zero and Succ as distinct types uninhabited...but of kind "*" and "k -> *" > data Z1 > data S1 nat SNat1 :: * -> * > data SNat1 a where > SZ1 :: SNat1 Z1 > SS1 :: SNat1 a -> SNat1 (S1 a) off we go... > instance Foo SNat1 where > type Bar SNat1 = Z1 > bar = SZ1 now lets do it the datakind route > data Nat where > Z :: Nat > S :: Nat -> Nat ahhh...SNat is of kind "Nat -> *" > data SNat a where > SZ :: SNat 'Z > SS :: SNat a -> SNat ('S a) so I cant make it an instance of the same type class "The first argument of 'Foo' should have kind '* -> *', but 'SNat' has kind 'Nat -> *' In the instance declaration for 'Foo SNat'" > --instance Foo SNat where > -- type Bar SNat = 'Z > -- bar = SZ unless I redefine my class (which seems a bit silly) > class Foo' (a :: k -> *) where > type Bar' a :: k > bar' :: a (Bar' a) now it works. > instance Foo' SNat where > type Bar' SNat = 'Z > bar' = SZ clearly named kinds (?) are somehow distinct from unnames ones? CONFIDENTIALITY NOTICE This e-mail (and any attached files) is confidential and protected by copyright (and other intellectual property rights). If you are not the intended recipient please e-mail the sender and then delete the email and any attached files immediately. Any further use or dissemination is prohibited. While MTV Networks Europe has taken steps to ensure that this email and any attachments are virus free, it is your responsibility to ensure that this message and any attachments are virus free and do not affect your systems / data. Communicating by email is not 100% secure and carries risks such as delay, data corruption, non-delivery, wrongful interception and unauthorised amendment. If you communicate with us by e-mail, you acknowledge and assume these risks, and you agree to take appropriate measures to minimise these risks when e-mailing us. MTV Networks International, MTV Networks UK & Ireland, Greenhouse, Nickelodeon Viacom Consumer Products, VBSi, Viacom Brand Solutions International, Be Viacom, Viacom International Media Networks and VIMN and Comedy Central are all trading names of MTV Networks Europe. MTV Networks Europe is a partnership between MTV Networks Europe Inc. and Viacom Networks Europe Inc. Address for service in Great Britain is 17-29 Hawley Crescent, London, NW1 8TT.

2 1

Re: [Haskell-cafe] RFC: "Native -XCPP" Proposal
by Brandon Allbery 07 May '15

07 May '15

On Wed, May 6, 2015 at 11:36 AM, Stephen Paul Weber < singpolyma(a)singpolyma.net> wrote: > Yes. This is one of my favourite things in GHC-land -- that an existing, > good-enough, standardised, and widely-deployed solution was chosen over a > NiH reinvention of preprocessing I have to assume my irony detector is broken as well. Or maybe I should just assume that "all the world's Linux with gcc" is assumed to be forever true and forever reliable by "all right-thinking people" so let's just sweep the nonissue under the rug because it can oh so obviously never be a real issue.... Because I had to face this back a couple decades ago, when my employer ported an application written in a 4GL (database language) to SCO Unix. The 4GL assumed cpp was the ever reliable pcc one and broke very badly when SCO used one integrated into its lexer (making it even more tightly wedded to C syntax than clang's). Eventually we replaced its cpp with a wrapper that ran m4 and redid everything else in m4's syntax. Which is why I was always a bit worried about ghc relying on cpp, was unsurprised when clang caused issues, and am rather annoyed that there are people who believe that they can just ignore it because REAL users will always be on Linux with gcc and all them furriners using weird OSes like OS X and FreeBSD can safely be ignored with their not-the-One-True-OS-and-compiler platforms. Additional historical note that I assume True Believers will ignore as meaningless: X11 used to make the same assumption that cpp was always and forever guaranteed to be friendly to non-C and this still shows at times in things like xrdb resource databases. They did accept the inevitable and (mostly) stop abusing it that way, and are now moving away from imake which likewise assumes it's safe to use cpp on Makefiles. (And yes, I encounter the same inability to comprehend or accept change there.) -- brandon s allbery kf8nh sine nomine associates allbery.b(a)gmail.com ballbery(a)sinenomine.net unix, openafs, kerberos, infrastructure, xmonad http://sinenomine.net

1 0

How to define a type-level append?
by Bas van Dijk 07 May '15

07 May '15

Hi, At the bottom I have a type-level programming related question, but first some preliminaries: > {-# LANGUAGE GADTs #-} > {-# LANGUAGE TypeOperators #-} > {-# LANGUAGE TypeFamilies #-} > {-# LANGUAGE DataKinds #-} > > import GHC.TypeLits I've implemented a protocol where a client can send a packet of orders to a server. An OrderPacket is either empty (represented by the "NoOrders" constructor) or consists of an Order and possibly more orders (represented by the: "order :> orders" constructor). An Order is defined by a type-level list of numeric addresses and a command. The semantics is that the server should address the command to the list of addresses. When the client sends a packet of orders, the server has to return a reply for each command for each address in order. I lifted this expectation into the type signature so that when the client sends an order the type-checker will complain if it tries to pattern match on the wrong reply. The above is formalized with the following GADT for a packet of orders (I left out some off-topic stuff): > data OrderPacket replies where > NoOrders :: OrderPacket '[] > (:>) :: !(Order addrs cmd) > -> !(OrderPacket replies) > -> OrderPacket > (RepliesFor addrs cmd :++: replies) > > infixr 5 :> > > data Order (addrs :: [Nat]) command where > Order :: (Command command) > => !command -> Order addrs command > > class Command command where > type Response command :: * > -- I left out some encoding/decoding related methods. > > type family RepliesFor (addrs :: [Nat]) > (cmd :: *) :: [*] where > RepliesFor '[] cmd = '[] > RepliesFor (addr ': addrs) cmd = > Reply addr cmd ': RepliesFor addrs cmd > > type family (xs :: [*]) :++: (ys :: [*]) :: [*] where > '[] :++: ys = ys > (x ': xs) :++: ys = x ': (xs :++: ys) > > infixr 5 :++: > > data Reply (addr :: Nat) command = > Response !(Maybe (Response command)) > -- I left out some other stuff that can be in a reply. > Now my problem, I would like to have the ability to append two OrderPackets. I would say the following type properly reflects what I want: > append :: OrderPacket replies1 > -> OrderPacket replies2 > -> OrderPacket (replies1 :++: replies2) How would I implement this? The following naive defintion > append NoOrders ys = ys > append (x :> xs) ys = x :> append xs ys gives the following type error: src/Test.lhs:77:25: Could not deduce ((RepliesFor addrs cmd :++: (replies :++: replies2)) ~ (replies1 :++: replies2)) from the context (replies1 ~ (RepliesFor addrs cmd :++: replies)) bound by a pattern with constructor :> :: forall (addrs :: [Nat]) cmd (replies :: [*]). Order addrs cmd -> OrderPacket replies -> OrderPacket (RepliesFor addrs cmd :++: replies), in an equation for ‘append’ at src/Test.lhs:77:11-17 NB: ‘:++:’ is a type function, and may not be injective Expected type: OrderPacket (replies1 :++: replies2) Actual type: OrderPacket (RepliesFor addrs cmd :++: (replies :++: replies2)) Relevant bindings include ys :: OrderPacket replies2 (bound at src/Test.lhs:77:20) xs :: OrderPacket replies (bound at src/Test.lhs:77:16) x :: Order addrs cmd (bound at src/Test.lhs:77:11) append :: OrderPacket replies1 -> OrderPacket replies2 -> OrderPacket (replies1 :++: replies2) (bound at src/Test.lhs:76:3) In the expression: x :> append xs ys In an equation for ‘append’: append (x :> xs) ys = x :> append xs ys I suspect I need to adapt the type signature of "append" to suite the definition. Cheers, Bas

2 2

Re: [Haskell-cafe] RFC: "Native -XCPP" Proposal
by Herbert Valerio Riedel 07 May '15

07 May '15

On 2015-05-06 at 17:36:05 +0200, Stephen Paul Weber wrote: >>As you may be aware, GHC's `{-# LANGUAGE CPP #-}` language extension >>currently relies on the system's C-compiler bundled `cpp` program to >>provide a "traditional mode" c-preprocessor. > > Yes. This is one of my favourite things in GHC-land -- that an > existing, good-enough, standardised, and widely-deployed solution was > chosen over a NiH reinvention of preprocessing. This allows other > Haskell compilers to support CPP on basically any system (since cpp is > so standard) without much effort, or even if the compiler does not > support {-# LANGUAGE CPP -#} the user can easily run `cpp` over the > source files themselves before feeding the source into the compiler. > > Because it is a real `cpp` being used, the developmer must take care > to follow the CPP syntax in the file that will then be transformed > into Haskell by `cpp` in the same way that C, C++, and other > developers have to take extra care (especially around use of # and > end-of-line \) when using `cpp`, but this is the normal state of > affairs for a secondary preprocessor step. As a benefit, the source > code will be processable by standard `cpp` implementations available > for virtually every platform. > > In short, the current solution provides a very robust and portable way > to do pre-compile preprocessing, and I like it very much. The problem I have with that line of argument is that we're using the so-called 'traditional mode' of `cpp`[1] for which afaik there is no written down common specification different implementations commit to adhere to (well, that's because 'traditional mode' refers to some vague implementation-specific "pre-standard" cpp semantics). And how is the developer supposed to take care to follow the (traditional mode) CPP syntax, if he can't test it easily with all potentially used (traditional-mode) `cpp`s out there? This already has led to problems with Clang's cpp vs GCC's cpp. Moreover, I was under the impression that it's only a matter of time till `traditional mode` support may be dropped from C compiler toolchains. Otoh, we can't use an ISO C spec conforming c-preprocessor, as that would conflict even more heavily w/ Haskell's grammar to the point of being inpractical. [1]: https://gcc.gnu.org/onlinedocs/cpp/Traditional-Mode.html

1 0

Re: [Haskell-cafe] RFC: "Native -XCPP" Proposal
by Brandon Allbery 06 May '15

06 May '15

On Wed, May 6, 2015 at 11:27 AM, Kosyrev Serge <_deepfire(a)feelingofgreen.ru> wrote: > Why *shouldn't* TH fill that role? What can be done about it? For one, it's difficult to make it available in cross compilers (granted, work is being done on this) and not available on some platforms (ARM has been a problem, dunno if it currently is). For another, I don't think you can currently control things like imports or LANGUAGE pragmas --- and as TH is currently constructed it's not clear that you could do so, or that you could do so in a way that is sane for users. This is not to say that I like cpp --- I'd like it a lot more if it weren't actually using a C preprocessor that is not actually under our control or guaranteed to be compatible with Haskell --- but it does provide a "meta" in a different dimension than TH does. -- brandon s allbery kf8nh sine nomine associates allbery.b(a)gmail.com ballbery(a)sinenomine.net unix, openafs, kerberos, infrastructure, xmonad http://sinenomine.net

1 0

Re: [Haskell-cafe] RFC: "Native -XCPP" Proposal
by Brandon Allbery 06 May '15

06 May '15

On Wed, May 6, 2015 at 10:59 AM, Bardur Arantsson <spam(a)scientician.net> wrote: > (I'm not going to be doing any of the work, so this is just armchairing, > but this seems like an 80/20 solution would be warranted.) > Only if you're convinced it will remain 80/20 for the foreseeable future. I do not want to bet on Linux always being gcc (and dislike the One True Platform-ism that line of thought encourages). -- brandon s allbery kf8nh sine nomine associates allbery.b(a)gmail.com ballbery(a)sinenomine.net unix, openafs, kerberos, infrastructure, xmonad http://sinenomine.net

1 0

minor confusion over kinds....
by Nicholls, Mark 06 May '15

06 May '15

And what "*" means as opposed to other things e.g. an explicit name "Nat" or a kind variable "k" > {-# LANGUAGE DataKinds #-} > {-# LANGUAGE ExplicitForAll #-} > {-# LANGUAGE FlexibleContexts #-} > {-# LANGUAGE FlexibleInstances #-} > {-# LANGUAGE GADTs #-} > {-# LANGUAGE MultiParamTypeClasses #-} > {-# LANGUAGE PolyKinds #-} > {-# LANGUAGE StandaloneDeriving #-} > {-# LANGUAGE TypeFamilies #-} > {-# LANGUAGE TypeOperators #-} > {-# LANGUAGE UndecidableInstances #-} what I want is a typeclass with instances of type level Naturals here's the class, the parameter is of kind (* -> *) i.e. a is some sort of wrapper that maps from types to values > class Foo (a :: * -> *) where > type Bar a > bar :: a (Bar a) lets ignore DataKinds define Zero and Succ as distinct types uninhabited...but of kind "*" and "k -> *" > data Z1 > data S1 nat SNat1 :: * -> * > data SNat1 a where > SZ1 :: SNat1 Z1 > SS1 :: SNat1 a -> SNat1 (S1 a) off we go... > instance Foo SNat1 where > type Bar SNat1 = Z1 > bar = SZ1 now lets do it the datakind route > data Nat where > Z :: Nat > S :: Nat -> Nat ahhh...SNat is of kind "Nat -> *" > data SNat a where > SZ :: SNat 'Z > SS :: SNat a -> SNat ('S a) so I cant make it an instance of the same type class "The first argument of 'Foo' should have kind '* -> *', but 'SNat' has kind 'Nat -> *' In the instance declaration for 'Foo SNat'" > --instance Foo SNat where > -- type Bar SNat = 'Z > -- bar = SZ unless I redefine my class (which seems a bit silly) > class Foo' (a :: k -> *) where > type Bar' a :: k > bar' :: a (Bar' a) now it works. > instance Foo' SNat where > type Bar' SNat = 'Z > bar' = SZ clearly named kinds (?) are somehow distinct from unnames ones? CONFIDENTIALITY NOTICE This e-mail (and any attached files) is confidential and protected by copyright (and other intellectual property rights). If you are not the intended recipient please e-mail the sender and then delete the email and any attached files immediately. Any further use or dissemination is prohibited. While MTV Networks Europe has taken steps to ensure that this email and any attachments are virus free, it is your responsibility to ensure that this message and any attachments are virus free and do not affect your systems / data. Communicating by email is not 100% secure and carries risks such as delay, data corruption, non-delivery, wrongful interception and unauthorised amendment. If you communicate with us by e-mail, you acknowledge and assume these risks, and you agree to take appropriate measures to minimise these risks when e-mailing us. MTV Networks International, MTV Networks UK & Ireland, Greenhouse, Nickelodeon Viacom Consumer Products, VBSi, Viacom Brand Solutions International, Be Viacom, Viacom International Media Networks and VIMN and Comedy Central are all trading names of MTV Networks Europe. MTV Networks Europe is a partnership between MTV Networks Europe Inc. and Viacom Networks Europe Inc. Address for service in Great Britain is 17-29 Hawley Crescent, London, NW1 8TT.

1 0

Assistant Professorship in Nottingham
by Graham Hutton 06 May '15

06 May '15

Dear all, The School of Computer Science at the University of Nottingham is seeking to appoint a new Assistant Professor: http://www.nottingham.ac.uk/jobs/currentvacancies/ref/SCI41814 Applications in the area of the Functional Programming (FP) lab are encouraged. The FP lab is keen to receive applications from candidates with an excellent publication record, experience in combining theory with practice, and the ability to secure external funding to support their research. Further information about the FP lab is available from: http://fp.cs.nott.ac.uk The deadline for applications is Wednesday 15th July 2015. Best wishes, Graham -- Prof Graham Hutton Functional Programming Lab School of Computer Science University of Nottingham, UK http://www.cs.nott.ac.uk/~gmh This message and any attachment are intended solely for the addressee and may contain confidential information. If you have received this message in error, please send it back to me, and immediately delete it. Please do not use, copy or disclose the information contained in this message or in any attachment. Any views or opinions expressed by the author of this email do not necessarily reflect the views of the University of Nottingham. This message has been checked for viruses but the contents of an attachment may still contain software viruses which could damage your computer system, you are advised to perform your own checks. Email communications with the University of Nottingham may be monitored as permitted by UK legislation.

1 0

ANN: HList 0.4
by adam vogt 06 May '15

06 May '15

Hello List, I've uploaded HList-0.4 [1]. Some highlights from this release: * support for 7.6 <= GHC <= 7.10 * new modules HCurry and HSort * many new functions: see the changelog [2] * data HList becomes data family. Trade-offs are explained in the documentation [3] Regards, Adam [1] http://hackage.haskell.org/package/HList-0.4.0.0 [2] http://hackage.haskell.org/package/HList-0.4.0.0/changelog [3] http://hackage.haskell.org/package/HList-0.4.0.0/docs/Data-HList-HList.html…

1 0