Re: Equality constraints (~): type-theory behind them
On Tue, Mar 26, 2019 at 1:05 AM Simon Peyton Jones wrote: Whoa, whoa. Your reply is making a number of presuppositions, and putting words in my mouth I did not say. Firstly: I am totally in favour of a typed intermediate language. Then the question is what type-theory do we use within the IR? Well it should be one that fits the surface language. System F-in-general broadly fits functional languages in general. Does System FC in particular fit Haskell specifically? I've seen no demonstration of that; and there are reasons to think it's only an approximate fit. That's why I've talked about "squeezing" and "straitjacket". Quite apart from FunDeps: does FC fit nicely to overlapping instances? I think not. Does FC fit nicely to Type Families? "type families in Haskell provide a powerful, modular means of defining type-level computation. However, their current design implicitly assumes that type families are total, introducing nonsensical types and significantly complicating the metatheory of type families and their extensions." say Eisenberg and Morris 2017. So that's a 'No'. E go on to translate Type Families into something that looks more like FunDeps, to my eye. The whole point about FunDeps is they are constrained by typeclasses. So they don't suffer those complications. One of the reasons coders prefer FunDeps is because they can use Overlapping Instances. Then for Schrijvers et al to translate FunDeps to Type Families that a) don't accommodate Overlaps; and b) use a feature (Type Families) that introduce "nonsensical types" and "complicating the metatheory" looks a fortiori like a poor fit. > There may be an IR based on fundeps, or CHRs or something, that has similar properties to FC. Perhaps it's already in FC and it's hiding in plain sight: the 'via CHRs' paper gives its rules in terms of quantified implications (or bi-implications). We now have in GHC the beginnings of Quantified/implication constraints. How are they translated into FC? I've tried looking at the Oliveira et al 2017 paper (section 5), but it's too dense for me. I can see it's in terms of constructing dictionaries, not Type Families. Tom should understand this far better than me: he and George are among the et al. Yet despite all 3 papers I've mentioned dating to 2017, there seems to be no mutual recognition. Tom+George's paper doesn't say they've considered Quantified/implication constraints amongst 'Related Work'. Yet this logic screams at me: class C a b | a -> b, b -> a -- two-way FunDeps instance C Int Bool Mark Jones and the 'via CHRs' paper says that translates to axioms (forall b. C Int b => b ~ Bool, forall a. C a Bool => a ~ Int) That is actual legal code in GHC today, as a constraint. Then all I need is a way to get those axioms into the program's type theory, presuming it can be expressed in FC. Look how succinct that constraint is, compare to introducing two Type Families, one for each direction of the FunDeps; and two TF instances; and two `~` superclass constraints. (I know the Schrijvers et al translates to Associated Types. But those are just sugar for top-level TFs, so they don't avoid the complications E talk about.) > I’d be happy to help explain how the current machinery works. Thank you. Is there somewhere a write-up/dummies guide for how GHC translates Quantified/implication constraints into FC? One further thing: > there may be aspects of GHC’s implementation fundeps that are unsatisfactory or argualbly just plain wrong, Yes there are. You can write code in GHC that is just incoherent. There's no hope of translating it into any type theory, and nobody should try. The tenor of your message is that the "just plain wrong" bits are still an open question. Not so: all the explanations are in the 'via CHRs' paper (not to mention flagged with Notes inside GHC source that say "bogus"). There are programs that the 'via CHRs' rules say should be rejected, but that GHC on the face of it accepts. You then find those programs are unusable/can only be used if you're very careful with your function signatures. My rule of thumb is: if Hugs accepts the code, then it will be coherent. If Hugs rejects, the error message corresponds to a rule in 'via CHRs'. No further research needed. AntC I'd far rather see GHC's implementation of FunDeps made more coherent (and learning from Hugs) than squeezing it into the straitjacket of System FC and thereby lose expressivity. > > > > To call System FC a straitjacket is to suggest that there is a > straightforward alternative that would serve the purpose better – let’s > take off the straitjacket! I’m all for that, but then we do need to > describe what the new alternative is, at a comparable level of precision. > > > > For better or worse, GHC uses FC as a statically-typed intermediate > language. Vanishingly few compilers do this; almost all use an untyped > intermediate language. With an untyped IR, all you need do is typecheck > the source
RE: Equality constraints (~): type-theory behind them
I'd far rather see GHC's implementation of FunDeps made more coherent (and learning from Hugs) than squeezing it into the straitjacket of System FC and thereby lose expressivity. To call System FC a straitjacket is to suggest that there is a straightforward alternative that would serve the purpose better – let’s take off the straitjacket! I’m all for that, but then we do need to describe what the new alternative is, at a comparable level of precision. For better or worse, GHC uses FC as a statically-typed intermediate language. Vanishingly few compilers do this; almost all use an untyped intermediate language. With an untyped IR, all you need do is typecheck the source program, and then you are done with typechecking --- provided that all the subsequent transformations and optimisations are sound. But with a statically typed IR, we have to ensure that every transformation produces a program that is itself well-typed; and that in turn pretty much rules out complicated inference algorithms, because they are fragile to transformation. Instead, GHC uses a complicated inference algorithm on the (implicitly typed) source program, but under the straitjacket restriction that the type inference algorithm must also translate the program into an explicitly-typed IR. This is a choice that GHC makes. It’s a choice that I love, and one that makes GHC distinctive. But I accept that it comes with a cost. There may be an IR based on fundeps, or CHRs or something, that has similar properties to FC. It would be a great research goal to work on such a thing. That said, there may be aspects of GHC’s implementation fundeps that are unsatisfactory or argualbly just plain wrong, and which could be fixed and still translate into FC. If anyone would like to work on that, I’d be happy to help explain how the current machinery works. Simon From: Glasgow-haskell-users On Behalf Of Anthony Clayden Sent: 25 March 2019 11:50 To: GHC Users List ; Tom Schrijvers Subject: Re: Equality constraints (~): type-theory behind them > On Mon, Dec 10, 2018 at 8:36:42 AM Tom Schrijvers wrote: > Maybe our Haskell'17 paper about Elaboration on Functional Dependencies sheds > some more light on your problem: Thanks Tom, I've also been working through the 2011 expanded version of 'System F with Type Equality Coercions' that Adam suggested. I'm finding your 2017 paper's proposals not up to the job, because it doesn't consider FunDeps for Overlapping Instances; and unnecessary because the examples it's addressing can be fixed purely using FunDeps, with their semantics per the 2006 'via CHRs' paper. The chief problems with using FunDeps in GHC code is GHC doesn't follow that semantics; neither does it follow any other well-principled/documented semantics.You can get it to accept a bunch of instances then find that taken together they're not consistent and confluent, in the sense of the 'via CHRs' paper. Specifically, re the 2017's paper Challenge 1: Enforcing (essentially Trac #10675). That set of instances in the example is not valid by the 'via CHRs' rules, and should be rejected. Hugs indeed rejects that code. GHC accepts it and #10675 shows what sort of incoherence can result. I'm not seeing we need to translate to Type Families/System FC to explain it. Re Challenge 2: Elaborating (which is Trac #9627 that gives the main example for the paper). We can fix that code with an extra `~` constraint: class C a b | a -> b instance C Int Bool f :: (C Int b, b ~ Bool) => b -> Bool f x = x (Or in Hugs with a `TypeCast` instead of the `~`.) Is that extra constraint onerous? The signature already has `Bool` hard-coded as the return type, so I don't see it's any more onerous. Or put that signature as f :: (C Int b) => b -> b Which also has the effect `b` must be `Bool`. I'd far rather see GHC's implementation of FunDeps made more coherent (and learning from Hugs) than squeezing it into the straitjacket of System FC and thereby lose expressivity. AntC ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users
Re: Equality constraints (~): type-theory behind them
> On Mon, Dec 10, 2018 at 8:36:42 AM Tom Schrijvers wrote: > Maybe our Haskell'17 paper about Elaboration on Functional Dependencies sheds some more light on your problem: Thanks Tom, I've also been working through the 2011 expanded version of 'System F with Type Equality Coercions' that Adam suggested. I'm finding your 2017 paper's proposals not up to the job, because it doesn't consider FunDeps for Overlapping Instances; and unnecessary because the examples it's addressing can be fixed purely using FunDeps, with their semantics per the 2006 'via CHRs' paper. The chief problems with using FunDeps in GHC code is GHC doesn't follow that semantics; neither does it follow any other well-principled/documented semantics.You can get it to accept a bunch of instances then find that taken together they're not consistent and confluent, in the sense of the 'via CHRs' paper. Specifically, re the 2017's paper Challenge 1: Enforcing (essentially Trac #10675). That set of instances in the example is not valid by the 'via CHRs' rules, and should be rejected. Hugs indeed rejects that code. GHC accepts it and #10675 shows what sort of incoherence can result. I'm not seeing we need to translate to Type Families/System FC to explain it. Re Challenge 2: Elaborating (which is Trac #9627 that gives the main example for the paper). We can fix that code with an extra `~` constraint: class C a b | a -> b instance C Int Bool f :: (C Int b, b ~ Bool) => b -> Bool f x = x (Or in Hugs with a `TypeCast` instead of the `~`.) Is that extra constraint onerous? The signature already has `Bool` hard-coded as the return type, so I don't see it's any more onerous. Or put that signature as f :: (C Int b) => b -> b Which also has the effect `b` must be `Bool`. I'd far rather see GHC's implementation of FunDeps made more coherent (and learning from Hugs) than squeezing it into the straitjacket of System FC and thereby lose expressivity. AntC ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users
[Haskell] [ICTH-2019] Conference on Current and Future Trends of Information and Communication Technologies in Healthcare. Coimbra, Portugal (Nov. 4-7, 2019)
Conference: The 9th International Conference on Current and Future Trends of Information and Communication Technologies in Healthcare (ICTH) Date: November 4-7, 2019 Location: Coimbra, Portugal Website: http://cs-conferences.acadiau.ca/icth-19/ ** Important Dates -- - Workshop Proposals: May 30, 2019 - Paper Submission Due: Jun 17, 2019 - Author Notification:August 6, 2019 - Final Manuscript Due: September 6, 2019 Publication - All ICTH 2019 accepted papers will be published by Elsevier Science in the open-access Procedia Computer Science series on-line. Procedia Computer Science is hosted by Elsevier on www.Elsevier.com and on Elsevier content platform ScienceDirect (www.sciencedirect.com), and will be freely available worldwide. All papers in Procedia will be indexed by Scopus ( www.scopus.com) and by Thomson Reuters' Conference Proceeding Citation Index (http://thomsonreuters.com/conference-proceedings-citation-index/). All papers in Procedia will also be indexed by Scopus (www.scopus.com) and Engineering Village (Ei) (www.engineeringvillage.com). This includes EI Compendex (www.ei.org/compendex). Moreover, all accepted papers will be indexed in DBLP (http://dblp.uni-trier.de/). The papers will contain linked references, XML versions and citable DOI numbers. Selected papers will be invited for publication, in the special issues of: - International Journal of Ambient Intelligence and Humanized Computing (IF: 1.588), by Springer ( http://www.springer.com/engineering/journal/12652) - International Journal of Computing and Informatics (IF: 0.504), ( http://www.cai.sk/ojs/index.php/cai/index) - International Journal of E-Health and Medical Communications, by IGI Global: ( http://www.igi-global.com/journal/international-journal-health-medical-communications/1158) ICTH 2019 will be held in conjunction with the 10th International Conference on Emerging Ubiquitous Systems and Pervasive Networks (EUSPN: http://cs-conferences.acadiau.ca/euspn-19/). Papers on either completed or ongoing research are invited in the following and related tracks: http://cs-conferences.acadiau.ca/icth-19/call-for-papers.html ICTH 2019 will be held in the city of Coimbra. Coimbra is a historical city and a municipality in Portugal. Among the many archaeological structures dating back to the Roman era, when Coimbra was the settlement of Aeminium, are its well-preserved aqueduct and cryptoporticus. Similarly, buildings from the period when Coimbra was the capital of Portugal (from 1131 to 1255) still remain. During the late Middle Ages, with its decline as the political centre of the Kingdom of Portugal, Coimbra began to evolve into a major cultural centre. This was in large part helped by the establishment of the University of Coimbra in 1290, the oldest academic institution in the Portuguese-speaking world. Apart from attracting many European and international students, the university is visited by many tourists for its monuments and history. Its historical buildings were classified as a World Heritage site by UNESCO in 2013: "Coimbra offers an outstanding example of an integrated university city with a specific urban typology as well as its own ceremonial and cultural traditions that have been kept alive through the ages." Its atmospheric, beautiful historic core cascades down a hillside in a lovely setting on the east bank of the Rio Mondego: it's a multicoloured collage of buildings spanning nearly a millennium. The conference take place in the environment of technology startups and laboratories within the installations of Instituto Pedro Nunes (IPN). IPN is created in 1991 through a University of Coimbra initiative, Instituto Pedro Nunes (IPN)2 is a private non-profit organization which promotes innovation and the transfer of technology, establishing the connection between the scientific and technological environment and the production sector. IPN mission is to leverage a strong university - enterprise relationship for the promotion of innovation, rigor, quality and entrepreneurship in private and public sector organizations by acting in three complementary areas: Research and technological development, consultancy and specialized services; Incubation and acceleration of businesses and ideas; Highly specialized training and promotion of science and technology. In the year of 2010, the Instituto Pedro Nunes incubator3 has been awarded as the Best Science-based Incubator in the world. Topics of interest include, but are not limited to: -- - Ambient Assisted Living for Elderly Care - Ambient Intelligence and Intelligent Service Systems - Analysis and Evaluation of Healthcare Systems - Clinical Data and Knowledge Management - Cloud Computing for Healthcare - Collaboration Technologies for Healthcare - Context-aware
