[Haskell-cafe] Haskell-Cafe Digest, Vol 158, Issue 29
Rik Howard
rik at dcs.bbk.ac.uk
Thu Oct 27 19:41:29 UTC 2016
Richard
thanks for your response and the references which I'll look into, the
Dijkstra sounds particularly relevant. "Procedural-functional" is not
novel; and as you also mentioned, Haskell, Clean and Mercury would qualify,
if you chose to look at it that way, as would other languages. Any novelty
in the note would only ever be in the way that the mix is provided. You
raise salient points about the sort of challenges that languages will need
to confront although a search has left me still unsure about PGPUs. Can I
ask you to say a bit more about programming styles: what Java can't do,
what others can do, how that scales?
Regards
Rik
On 27 October 2016 at 13:00, <haskell-cafe-request at haskell.org> wrote:
> Send Haskell-Cafe mailing list submissions to
> haskell-cafe at haskell.org
>
> To subscribe or unsubscribe via the World Wide Web, visit
> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
> or, via email, send a message with subject or body 'help' to
> haskell-cafe-request at haskell.org
>
> You can reach the person managing the list at
> haskell-cafe-owner at haskell.org
>
> When replying, please edit your Subject line so it is more specific
> than "Re: Contents of Haskell-Cafe digest..."
>
>
> Today's Topics:
>
> 1. Re: A Procedural-Functional Language (WIP) (Rik Howard)
> 2. Re: A Procedural-Functional Language (WIP) (Rik Howard)
> 3. Re: A Procedural-Functional Language (WIP) (Richard A. O'Keefe)
> 4. Proof of concept of explanations for instance resolution
> (Michael Sloan)
> 5. Re: A Procedural-Functional Language (WIP) (Joachim Durchholz)
> 6. Re: Proof of concept of explanations for instance resolution
> (Tom Ellis)
> 7. Fwd: How to best display type variables with the same name
> (Christopher Done)
> 8. CoALP-Ty'16: Call for Participation (František Farka)
>
>
> ----------------------------------------------------------------------
>
> Message: 1
> Date: Wed, 26 Oct 2016 16:48:47 +0100
> From: Rik Howard <rik at dcs.bbk.ac.uk>
> To: Joachim Durchholz <jo at durchholz.org>
> Cc: haskell-cafe at haskell.org
> Subject: Re: [Haskell-cafe] A Procedural-Functional Language (WIP)
> Message-ID:
> <CAAGBjQW+xzaU5kGQsm5S_et6v4YXOZ1QvkNN_cRfigRUOdbNMQ@
> mail.gmail.com>
> Content-Type: text/plain; charset="utf-8"
>
> Jo
>
>
> > Question is not whether these things are precluded, question is how you
> > want to tackle them. It's not even stating design goals here.
>
>
> The section on Types has been amended to note that these questions form a
> part of the ongoing work.
>
>
> >
> >
> The salient point of this and some other features is that they make it
> > easier to reason about a given program's properties, at the expense of
> > making programming harder.
> >
>
> You put that point well.
>
>
> >
> > The basic concept of subtypes is simple, but establishing a definition of
> > "subtype" that is both useful and sound is far from trivial.
> >
>
> I hope that there is nothing that I've said that could be interpreted as me
> thinking otherwise. As you mentioned elsewhere, though, they look too
> appealing to ignore.
>
>
> >
> > For example. mutable circles and mutable ellipses are not in a subtype
> > relationship to each other if there is an updating "scale" operation with
> > an x and y scaling factor (you cannot guarantee that a scaled circle
> stays
> > circular).
> > The design space for dealing with this is far from fully explored.
> >
>
> I'm not sure that the language could support mutable structures but I take
> your point that there are complications.
>
>
> >
> > Also, subtypes and binary operators do not really mix; google for
> > "parallel type hierarchy". (The core of the problem is that if you make
> > Byte a subtype of Word, declaring the (+) operator in Word as Word ->
> Word
> > will preclude Byte from being a subtype because you want a covariant
> > signature in Byte but that violates subtyping rules for functions. So you
> > need parametric polymorphism, but now you cannot use the simple methods
> for
> > subtyping anymore.)
>
>
> Clearly there is more to be done in this area.
>
>
> >
> > The key point to mention is that you want to maintain referential
> > integrity.
> >
>
> The document now mentions this.
>
>
> >
> > Sounds pretty much like the conseqences of having the IO monad in
> Haskell.
> >
>
> That seems fair to me although the broader impact on an entire program
> would be different I think.
>
>
> >
> > I think you should elaborate similarities and differences with how
> Haskell
> > does IO, that's a well-known standard it is going to make the paper
> easier
> > to read. Same goes for Clean&Mercury.
>
>
> Something like that is addressed in Related Work. Clean is already on the
> list but it sounds, from your comments and those of others, as if Mercury
> may be worth including as well.
>
>
> >
> > It's hard to tell whether it is actually new, too many details are
> missing.
>
>
> Certainly you have spotted the vagueness in the types however I think that
> that issue can be momentarily set aside from the point of view of novelty.
> The language is purely functional with respect to functions and provides
> out-vars as the only mechanism for dealing with IO. Let's assume for the
> moment that that all hangs together: if there is another language that does
> that, no novelty; otherwise, there is novelty.
>
> Once again, your feedback has been useful and stimulating. Many thanks!
>
> Regards
> Rik
> -------------- next part --------------
> An HTML attachment was scrubbed...
> URL: <http://mail.haskell.org/pipermail/haskell-cafe/
> attachments/20161026/37a44400/attachment-0001.html>
>
> ------------------------------
>
> Message: 2
> Date: Wed, 26 Oct 2016 23:33:55 +0100
> From: Rik Howard <rik at dcs.bbk.ac.uk>
> To: Joachim Durchholz <jo at durchholz.org>
> Cc: haskell-cafe at haskell.org
> Subject: Re: [Haskell-cafe] A Procedural-Functional Language (WIP)
> Message-ID:
> <CAAGBjQXSb7B7SqB7xrXKW-jWw16AK2bf4XYA__vdQ0w9k5iS6A@
> mail.gmail.com>
> Content-Type: text/plain; charset="utf-8"
>
> >
> >
> Let's assume for the moment that that all hangs together: if there is
> > another language that does that, no novelty; otherwise, there is novelty.
> >
> >
> Maybe not quite so clear-cut but still in the area, I think.
> -------------- next part --------------
> An HTML attachment was scrubbed...
> URL: <http://mail.haskell.org/pipermail/haskell-cafe/
> attachments/20161026/0afb35e7/attachment-0001.html>
>
> ------------------------------
>
> Message: 3
> Date: Thu, 27 Oct 2016 12:05:45 +1300
> From: "Richard A. O'Keefe" <ok at cs.otago.ac.nz>
> To: <haskell-cafe at haskell.org>
> Subject: Re: [Haskell-cafe] A Procedural-Functional Language (WIP)
> Message-ID: <836817a9-52f6-fdf6-50db-420c12f91efe at cs.otago.ac.nz>
> Content-Type: text/plain; charset="utf-8"; format=flowed
>
> I'd like to point out that "procedural-functional" is not novel.
> The programming language Euclid, an "industrial strength Pascal",
> was sufficiently nailed down that a blue-and-white report from
> Xerox PARC showed that it could be viewed as a pure functional
> language. And I don't know if anyone ever pointed it out, but
> the language used in Dijkstra's "A Discipline of Programming",
> and in a number of papers subsequently, was constrained in the
> same way, to the point where that language can be seen as a
> sheep in wolf's clothing too.
>
> I'd like to point out something else. We are looking at the
> end of Moore's Law. If that end hasn't already overtaken us,
> it's visible in the rear view mirror and coming up fast. HP,
> for example, are revisiting the idea of having *LOTS* of CPUs
> mixed in with the memory because conventional multicore has
> its own problems. And the Square Kilometre Array telescope's
> computers are definitely going to be chock full of FPGAs as
> well as more conventional things like PGPUs.
>
> This means that in the foreseeable future we are going to need
> to learn a new style of programming because the antique style,
> as exemplified by say Java, just isn't going to scale.
>
> APL was once described as "the language of the future for the
> problems of the past". I suspect that WIP may be headed in
> the same direction.
>
> Disciple http://trac.ouroborus.net/ddc/ may be of interest.
> Quoting that page,
> "DDC is a research compiler used to investigate program transformation
> in the presence of computational effects. It compiles a family of strict
> functional core languages and supports region and effect. This extra
> information provides a handle on the operational behaviour of code that
> isn't available in other languages. Programs can be written in either a
> pure/functional or effectful/imperative style, and one of our goals is
> to provide both styles coherently in the same language."
>
>
>
> ------------------------------
>
> Message: 4
> Date: Wed, 26 Oct 2016 17:53:31 -0700
> From: Michael Sloan <mgsloan at gmail.com>
> To: haskell-cafe <haskell-cafe at haskell.org>
> Subject: [Haskell-cafe] Proof of concept of explanations for instance
> resolution
> Message-ID:
> <CAEDDsWfSbVi60c4X3snVSbWUSrrzyjGcTZDUXy0kPPANCPy2yw at mail.
> gmail.com>
> Content-Type: text/plain; charset=UTF-8
>
> When typeclass machinery gets complicated, it can be hard to figure
> interpret
> the meaning behind GHC's messages. In particular "Could not deduce ..."
> messages
> often reference constraints that are deep in a tree of resolving
> typeclasses. I
> think it would be great if GHC provided additional information for this
> circumstance. In a way what we need is a "stack trace" of what GHC was
> thinking
> about when yielding these type errors.
>
> A couple years ago, I wrote an extremely hacky approach to yielding this
> information through TH. It is quite imperfect, and only works with GHC
> 7.8. I've
> realized that it's highly unlikely that this project will reach the level
> of
> polish for it to be very usable in practice:
> https://github.com/mgsloan/explain-instance
>
> However, rather than allow that work to be wasted, I'd like to bring
> people's
> attention to the problem in general, and how we might solve it in GHC.
> Along
> with providing more information in type errors, this could also look like
> having
> a ":explain" command in ghci.
>
> Lets take Text.Printf as an example. The expression (printf "%d %d" (1 ::
> Int)
> (2 :: A) :: String) has quite a bit of machinery behind it:
>
> printf :: (PrintfType r) => String -> r
>
> class PrintfType t
> instance (IsChar c) => PrintfType [c]
> instance (a ~ ()) => PrintfType (IO a)
> instance (PrintfArg a, PrintfType r) => PrintfType (a -> r)
>
> class PrintfArg a where
> instance PrintfArg Int where
>
> With explain-instance, all we have to do is create a module with the
> following
> in it:
>
> import ExplainInstance
> import Text.Printf
> $(explainInstance [t| PrintfType (Int -> Int -> String) |])
>
> Then, upon running the generated main function, we get the following
> explanation:
>
> instance (PrintfArg a, PrintfType r) => PrintfType (a -> r)
> with a ~ Int
> r ~ (Int -> [Char])
>
> instance PrintfArg Int
>
> instance (PrintfArg a, PrintfType r) => PrintfType (a -> r)
> with a ~ Int
> r ~ [Char]
>
> instance PrintfArg Int
>
> instance IsChar c => PrintfType ([c])
> with c ~ Char
>
> instance IsChar Char
>
> This is the recursive tree of instance instantiation! It shows the instance
> head, the particular types that it has been instantiated at in a made up
> "with"
> clause. Most importantly, it shows how the instance's constraints are also
> satisfied, giving a tree for an explanation.
>
> The implementation of this is irrelevant, but for the curious: it involves
> recursively reifying all of the typeclasses, and then generating a whole
> new set
> of typeclasses. These modified versions have the same heads (renamed) as
> the
> original typeclasses, but just have one method, which yields a description
> of
> the the types it has been instantiated with, via Typeable.
>
> Well that's quite convenient! I think it can really aid in understanding
> typeclass machinery to be able to get this variety of trace through what
> GHC is
> thinking when satisfying a constraint. However, this is just half the
> problem -
> what about type errors? I played around with a solution to this via
> UndecidableInstances, where it would create a base-case instance that
> represents
> the error case.
>
> Lets say I wanted to use (printf :: String -> A -> Int -> Maybe String)
> where A
> is a type that is not an instance of PrintfArg. Another issue with this is
> that
> the result type (Maybe String) is not allowed by PrintfType.
>
> The output of
>
> $(explainInstanceError [t| PrintfType (A -> Int -> Maybe String) |])
>
> is
>
> instance (PrintfArg a, PrintfType r) => PrintfType (a -> r)
> with a ~ A
> r ~ (Int -> Maybe [Char])
>
> ERROR instance PrintfArg a
> with a ~ A
>
> instance (PrintfArg a, PrintfType r) => PrintfType (a -> r)
> with a ~ Int
> r ~ Maybe [Char]
>
> instance PrintfArg Int
>
> ERROR instance PrintfType t
> with t ~ Maybe [Char]
>
> This explains exactly where the problem is coming from in the typeclass
> machinery. If you're just looking at the type of printf, and see a
> `PrintfType`
> constraint, it can be a total mystery as to why GHC is complaining about
> some
> class we may or may not know about:
>
> No instance for (PrintfArg A) arising from a use of ‘printf’
>
> Thanks for reading! I hope we can address this UI concern in the future.
> I
> hope I've contributed something by demonstrating the possibility!
>
> -Michael
>
>
> ------------------------------
>
> Message: 5
> Date: Thu, 27 Oct 2016 07:17:33 +0200
> From: Joachim Durchholz <jo at durchholz.org>
> To: haskell-cafe at haskell.org
> Subject: Re: [Haskell-cafe] A Procedural-Functional Language (WIP)
> Message-ID: <b3e7d84b-20a5-0028-a21f-62c6455afc6e at durchholz.org>
> Content-Type: text/plain; charset=utf-8; format=flowed
>
> Am 27.10.2016 um 01:05 schrieb Richard A. O'Keefe:
> > This means that in the foreseeable future we are going to need
> > to learn a new style of programming because the antique style,
> > as exemplified by say Java, just isn't going to scale.
>
> I think you underestimate the adaptability of existing languages.
>
> Java has been preparing to move towards immutability&FP. At glacier-like
> speed, admittedly, but once those massively multicore systems appear,
> Java will be prepared to move.
>
> Haskell can claim to be already there, but wrt. how many issues have
> been staying unaddressed, it's no better than Java, it's just different
> issues.
> IOW this is not a predetermined race.
>
>
> ------------------------------
>
> Message: 6
> Date: Thu, 27 Oct 2016 08:56:56 +0100
> From: Tom Ellis <tom-lists-haskell-cafe-2013 at jaguarpaw.co.uk>
> To: haskell-cafe at haskell.org
> Subject: Re: [Haskell-cafe] Proof of concept of explanations for
> instance resolution
> Message-ID: <20161027075656.GV4593 at weber>
> Content-Type: text/plain; charset=us-ascii
>
> On Wed, Oct 26, 2016 at 05:53:31PM -0700, Michael Sloan wrote:
> > When typeclass machinery gets complicated, it can be hard to figure
> interpret
> > the meaning behind GHC's messages. In particular "Could not deduce ..."
> messages
> > often reference constraints that are deep in a tree of resolving
> typeclasses. I
> > think it would be great if GHC provided additional information for this
> > circumstance. In a way what we need is a "stack trace" of what GHC was
> thinking
> > about when yielding these type errors.
> [...]
> > Thanks for reading! I hope we can address this UI concern in the
> future. I
> > hope I've contributed something by demonstrating the possibility!
>
> I think a "stack trace" of what GHC was thinking would be a great idea! I
> brought this idea here:
>
> https://mail.haskell.org/pipermail/haskell-cafe/2016-
> August/124622.html
>
> Tom
>
>
> ------------------------------
>
> Message: 7
> Date: Thu, 27 Oct 2016 10:43:35 +0100
> From: Christopher Done <chrisdone at gmail.com>
> To: Haskell Cafe <haskell-cafe at haskell.org>
> Subject: [Haskell-cafe] Fwd: How to best display type variables with
> the same name
> Message-ID:
> <CAAJHNPDQPvZdbkF3BqYQbJs3B_pmO6KG8QBYrnKH+-5Rnz3qDQ at mail.
> gmail.com>
> Content-Type: text/plain; charset=UTF-8
>
> Hi all,
>
> I posted the below to ghc-devs, but they suggested perhaps
> Haskell-Cafe might be interested in the problem. For convenience,
> here's the ghc-devs archive of that discussion:
> https://mail.haskell.org/pipermail/ghc-devs/2016-October/013085.html
>
> ---------- Forwarded message ----------
> From: Christopher Done <chrisdone at gmail.com>
> Date: 19 October 2016 at 12:45
> Subject: How to best display type variables with the same name
> To: "ghc-devs at haskell.org" <ghc-devs at haskell.org>
>
>
> We've encountered a problem in Intero which is that when inspecting
> types of expressions and patterns, sometimes it happens that the type,
> when pretty printing, yields variables of the same name but which have
> different provenance.
>
> Here's a summary of the issue:
>
> https://github.com/commercialhaskell/intero/issues/280#issuecomment-
> 254784904
>
> And a strawman proposal of how it could be solved:
>
> https://github.com/commercialhaskell/intero/issues/280#issuecomment-
> 254787927
>
> What do you think?
>
> Also, if I were to implement the strawman proposal, is it possible to
> recover from a `tyvar :: Type` its original quantification/its
> "forall"? I've had a look through the API briefly and it looks like a
> _maybe_.
>
> Ciao!
>
>
> ------------------------------
>
> Message: 8
> Date: Thu, 27 Oct 2016 11:54:00 +0100
> From: František Farka <frantisek at farka.eu>
> To: haskell at haskell.org, haskell-cafe at haskell.org
> Subject: [Haskell-cafe] CoALP-Ty'16: Call for Participation
> Message-ID: <20161027105400.GC25396 at farka.eu>
> Content-Type: text/plain; charset=utf-8
>
> Call for Participation
>
> Workshop on
> Coalgebra, Horn Clause Logic Programming and Types
>
> 28-29 November 2016, Edinburgh, UK
> https://ff32.host.cs.st-andrews.ac.uk/coalpty16/
>
>
> Abstract submission: 15 October, 2016
> Registration deadline: 5 November, 2016
>
> ====================================================
>
> Objectives and scope
> -------------------
>
> The workshop marks the end of the EPSRC Grant Coalgebraic Logic
> Programming for
> Type Inference, by K. Komendantskaya and J. Power and will consist of two
> parts:
>
> Part 1 - Semantics: Lawvere theories and Coalgebra in Logic and
> Functional Programming
>
> Part 2 - Programming languages: Horn Clause Logic for Type
> Inference in
> Functional Languages and Beyond
>
> We invite all colleagues working in related areas to present and share
> their
> results. We envisage a friendly meeting with many stimulating discussions,
> and
> therefore welcome presentations of already published research as well as
> novel
> results. Authors of original contributions will be invited to submit their
> papers to EPTCS post-proceedings. We especially encourage early career
> researchers to present and participate.
>
> Venue
> -----
>
> The workshop will be held at the International Centre for Mathematical
> Sciences,
> in Edinburgh city centre, just 2 minutes walk from the Informatics Forum.
>
> Registration
> ------------
>
> To register please fill in https://goo.gl/forms/KAm83p1bcNAxw0ss2
> Although the registration is free it is compulsory. Please register
> by the 5th of November 2016.
>
>
> Programme
> ---------
>
> Monday 28 November
>
> 9:10 - 9:20 Registration
> 9:30 - 9:40 Welcome to CoALP-Ty'16
> - Ekaterina Komendantskaya
> 9:40 - 11:10 Invited talk I
> - John Power: Logic Programming: Laxness and Saturation
> 11:10 - 11:30 Coffee break
> 11:30 - 12:00 Contributed talk
> - Henning Basold and Ekaterina Komendantskaya: Models of
> Inductive-Coinductive Logic Programs
> 12:00 - 13:00 Invited talk II
> - Steven Ramsay and Luke Ong: Refinement Types and
> Higher-Order
> Constrained Horn Clauses
> 13:00 - 14:00 Lunch
> 14:00 - 15:00 Invited talk III
> - Tarmo Uustalu: Comodels and Interaction
> 15:00 - 15:30 Coffee break
> 15:30 - 17:00 Contributed talks
> - František Farka: Proofs by Resolution and Existential
> Variables
> - Bashar Igried and Anton Setzer: Defining Trace Semantics
> for
> CSP-Agda
> - Clemens Kupke: Coalgebra and Ontological Rules
> 18:00 - 20:00 Workshop dinner
> - Lebanese restaurant Beirut, 24 Nicolson Square
>
>
> Tuesday 29 November
>
> 9:30 - 10:30 Invited talk IV
> - Claudio Russo: Classes for the Masses
> 10:30 - 11:00 Contributed talk
> - J. Garrett Morris: Semantical Analysis of Type Classes
> 11:00 - 11:30 Coffee break
> 11:30 - 12:30 Invited talk V
> - Davide Ancona: Abstract Compilation for Type Analysis of
> Object-Oriented Languages
> 12:30 - 13:30 Lunch
> 13:30 - 14:30 Invited talk VI
> - Ki Yung Ahn: Relational Specification of Type Systems
> Using
> Logic Programming
> 14:30 - 15:15 Discussion Panel
> - Horn Clause Logic: its Proof Theory, Type Theory and
> Category
> Theory — do we have the full picture yet?
> 15:15 - 15:45 Coffee break
> 15:45 - 16:45 Contributed talks
> - Martin Schmidt: Coalgebraic Logic Programming:
> Implementation
> and Optimization
> - Luca Franceschini, Davide Ancona and Ekaterina
> Komendantskaya:
> Structural Resolution for Abstract Compilation of
> Object-Oriented Languages
>
>
> Important dates
> ---------------
>
> Workshop registration: 5 November, 2016
> Workshop: 28–29 November, 2016
>
>
> Programme committee
> -------------------
>
> Ki Yung Ahn, Nanyang Technological University, Singapore
> Davide Ancona, University of Genoa, Italy
> Filippo Bonchi, CNRS, ENS de Lyon, France
> Iavor Diatchki, Galois, Inc, USA
> Peng Fu, Heriot-Watt University, Edinburgh, UK
> Neil Ghani, University of Strathclyde, UK
> Patricia Johann, Appalachian State University, USA
> Ekaterina Komendantskaya, Heriot-Watt University, Edinburgh, UK
> Clemens Kupke, University of Strathclyde, UK
> J. Garrett Morris, University of Edinburgh, UK
> Fredrik Nordvall Forsberg, University of Strathclyde, UK
> John Power, University of Bath, UK
> Claudio Russo, Microsoft Research Cambridge, UK
> Martin Schmidt, DHBW Stuttgart and Osnabrück University , Germany
> Stephan Schulz, DHBW Stuttgart, Germany
> Aaron Stump, The University of Iowa, USA
> Niki Vazou, University of California, San Diego, USA
> Joe Wells, Heriot-Watt University, Edinburgh, UK
> Fabio Zanasi, Radboud University of Nijmegen, The Netherlands
>
>
> Workshop chairs
> --------
> Ekaterina Komendantskaya, Heriot-Watt University, UK
> John Power, University of Bath, UK
>
>
> Publicity chair
> ---------------
> František Farka, University of Dundee, UK and University of St Andrews, UK
>
> --
>
> František Farka
>
>
> ------------------------------
>
> Subject: Digest Footer
>
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
>
>
> ------------------------------
>
> End of Haskell-Cafe Digest, Vol 158, Issue 29
> *********************************************
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20161027/0f569261/attachment.html>
More information about the Haskell-Cafe
mailing list