Re: [Haskell-cafe] Interfacing Java/Haskell
CJ van den Berg c...@vdbonline.com: I have successfully written Java/Haskell programs using the Java Native Interface. You can find my JNI to Haskell binding library at https://github.com/neurocyte/foreign-jni. I am primarily using it to write Android Apps with Haskell, Just out of curiosity, have you got any complete apps that you built that way? Are they in the Google Store? Manuel ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] install cuda
Geoffrey Mainland mainl...@apeiron.net: Fantastic, glad you got it working! Maybe it's time for me to send Trevor a pull request... That sounds like an excellent idea! Manuel On 04/01/2013 04:27 PM, Peter Caspers wrote: indeed, not very helpful ... When I installed Cuda the latest driver (296.0) that was running on my laptop (a W520 ThinkPad) was not sufficient for version 5.0. However as I noticed today in February Lenovo released a driver update (311.0) and with that 5.0 is in fact running. :-) With that the Haskell bindings work well. Thanks again very much, Geoff Peter Am 01.04.2013 12:25, schrieb Geoffrey Mainland: That is not a very elucidating crash message, so I don't see how to proceed. After ghci print Loading package cuda-0.5.0.0 ... linking ... done. it just exits? No error dialog, nothing? Did you try building any of the examples in the cuda package that don't require ghci? Is your graphics card incompatible with CUDA 5.0, or do you just not want to update your driver? Geoff On 04/01/2013 10:33 AM, Peter Caspers wrote: yes, the installation seems to work fine now. However, doing the following test in ghci Prelude :m +Foreign.CUDA Prelude Foreign.CUDA props 0 Loading package bytestring-0.9.2.1 ... linking ... done. Loading package cuda-0.5.0.0 ... linking ... done. results in a crash. The CUDA version I am using is 4.1.28. You think there is something I could try to analyze this further ? Thanks a lot for your help Peter Am 31.03.2013 21:48, schrieb Geoffrey Mainland: You need to generate the configure script using autoconf: https://www.gnu.org/software/autoconf/manual/autoconf.html#autoconf-Invocation On 03/31/2013 08:27 PM, Peter Caspers wrote: Hmm, I get Configuring cuda-0.5.0.0... setup.exe: configure script not found. can you help ? Peter I was able to install the cuda package under 32-bit GHC 7.4.2 using the 5.0 SDK and use it from within ghci. This required using my fork of the cuda repo and following the instructions in my WINDOWS.md. Make sure nvcc is in your path (the CUDA installer should have made this so) and try 'cabal configure'. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Which advanced Haskell topics interest you
Most existing Haskell books and similar teaching material is aimed at programmers who are new to Haskell. This survey is to assess the community interest in teaching material covering advanced topics beyond the commonly taught introductory material. https://docs.google.com/spreadsheet/viewform?formkey=dE1QZFNRLTFMdkllYWIyR2FkYnRzZHc6MQ Manuel ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Which advanced Haskell topics interest you
Kristopher Micinski krismicin...@gmail.com: On Thu, Oct 4, 2012 at 1:21 PM, Stephen Tetley stephen.tet...@gmail.com wrote: As for an advanced book, maybe limiting the subject to one domain (concurrency / DSLs for graphics / pick a favourite ...) might make a better book than one targeting a mix of advanced topics. Another problem is that the topics in these domains don't simply deal with Haskell, they deal with real computer science that is not to be understated. Concurrency for Haskell involves tackling the real implementation issues inherent in making things work, but also a good taste of semantics, and actual concurrency. Those are very good points. Thanks, Manuel ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Haskell Platform - BSD License?
Thomas Schilling nomin...@googlemail.com: You may concatenate the licenses of all the packages you are using. GHC includes the LGPL libgmp. The license file for each package is mentioned in the .cabal file. If you need a version of GHC free of the LGPL, you can build GHC from source using the package 'integer-simple' instead of 'integer-gmp'. Manuel ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] DPH matrix product
Firstly, especially when you are talking about performance, please provided
detailed information on (a) the versions of the compiler and libraries that you
used and (b) of the command line options that you used for compilation.
Secondly, your function 'transposeP' doesn't make for a good nested
data-parallel program. I haven't looked at the generated code, but I wouldn't
be surprised if it doesn't optimise very well.
The core benefit of nested data parallelism is that the sub-arrays in a nested
array of arrays can be of varying size leading to irregular parallelism.
However, that flexibility comes at a price, namely that it is a fairly
inefficient representation for *rectangular arrays*, such as regular
two-dimensional matrices (as in your example). It shouldn't be quite as
inefficient as what you report, but it will never be competitive with a
dedicated regular representation.
Hence, for code, such as yours, we recommend to use our Repa library:
http://hackage.haskell.org/package/repa
It generates very fast code for regular array problems, see also
http://www.cse.unsw.edu.au/~chak/papers/LCKP12.html
Manuel
mblanco blanco...@gmail.com:
Hi, I'm trying to implement a matrix product example using DPH. This is the
code:
---
type MMultType = Double
type Matrix = [:[:MMultType:]:]
type MVector = [:MMultType:]
type Matrix_wrapper = PArray (PArray MMultType)
{-# NOINLINE matMult_wrapper #-}
matMult_wrapper :: Matrix_wrapper - Matrix_wrapper - Matrix_wrapper
matMult_wrapper mA mB = toPArrayP (mapP toPArrayP (matMult (fromNestedPArrayP
mA) (fromNestedPArrayP mB)))
matMult :: Matrix - Matrix - Matrix
matMult mA mB = mapP (\row - mapP (\col - dotp row col) (transposeP mB)) mA
dotp :: MVector - MVector - MMultType
dotp row col = D.sumP (zipWithP (D.*) row col)
transposeP :: Matrix - Matrix
transposeP m =
let
h = lengthP m
w = lengthP (m !: 0)
rh = I.enumFromToP 0 (h I.- 1)
rw = I.enumFromToP 0 (w I.- 1)
in
if h I.== 0 then [: :]
else mapP (\y - mapP (\x - m !: x !: y) rh) rw
---
My problem is at execution time, on matrices of size 300*300 the program does
finish (although it is very slow), but on 700*700 it consumes GBs of RAM
until the process is aborted.
In the paper Work Efficient Higher-Order Vectorisation it is explained that
a work complexity problem (wich involved unnecesary array replication) was
recently treated. So at first I thought the code implementation related to
the paper had not been uploaded to hackage. But as I understand it must have
been, as that seems to be the motive of the dph-lifted-vseg package.
Does anybody notice the problem with the example or if the problem is related
to the subject treated in the paper?
Thanks in advance!
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] [ANN] Accelerate version 0.12: GPU computing with Haskell
We just released version 0.12 of Data.Array.Accelerate, the GPGPU[1] library for Haskell: http://justtesting.org/gpu-accelerated-array-computations-in-haskell This is a beta release. The library is not perfect, but it is definitely usable, and we are looking for early adopters. Manuel [1] Currently only NVIDIA GPUs are supported via NVIDIA's CUDA framework. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Can Haskell outperform C++?
Ryan Newton: But, anyway, it turns out that my example above is easily transformed from a bad GHC performance story into a good one. If you'll bear with me, I'll show how below. First, Manuel makes a good point about the LLVM backend. My 6X anecdote was from a while ago and I didn't use llvm [1]. I redid it just now with 7.4.1+LLVM, results below. (The below table should read correctly in fixed width font, but you can also see the data in the spreadsheet here.) Time (ms) Compiled File size Comple+Runtime (ms) GHC 7.4.1 O0 24441241K GHC 7.4.1 O2 925 1132K1561 GHC 7.4.1 O2 llvm 931 1133K GHC 7.0.4 O2 via-C 684 974K So LLVM didn't help [1]. And in fact the deprecated via-C backend did the best! I would classify that as a bug. [1] P.P.S. Most concerning to me about Haskell/C++ comparisons are David Peixotto's findings that LLVM optimizations are not very effective on Haskell-generated LLVM compared with typical clang-generated LLVM. There is some work underway to improve the situation, but I am sure more could be done. Manuel ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Can Haskell outperform C++?
Ryan Newton: As a community I think we have to face the fact that writing the hot inner loop of your application as idiomatic Haskell is not [yet] going to give you C/Fortran performance off the bat. Though in some cases there's not really anything stopping us but more backend/codegen work (I'm thinking of arithmetically intensive loops with scalars only). For example, the following Mandel kernel is in many ways the *same* as the C version: https://github.com/simonmar/monad-par/blob/662fa05b2839c8a0a6473dc490ead8dd519ddd1b/examples/src/mandel.hs#L24H We have the types; we've got strictness (for this loop); but the C version was 6X faster when I tested it. Did you use the LLVM backend? I am asking because I have seen dramatic differences between the code generators in similar example. Have a look at https://wiki.cse.unsw.edu.au/cs3141/12s1/Parallelism%20notes With GHC's native code generator, the C version is much faster than the Haskell version (by a factor of 2 or 3 IIRC), but using GHC's LLVM backend, the Haskell version is even a few percent faster than the C version on my machine. (This is on OS X using llvm-gcc to compile the C code — that is, the code generator for the C and Haskell version goes via LLVM.) I think that is an interesting example, because it shows (a) just how much of a difference a good code generator can make and (b) that using the same code generator, a Haskell compiler has no inherent disadvantage to a C compiler. (Nevertheless, especially for small examples, it is much easier to write a slow Haskell than to write a slow C program.) Manuel ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Haskell development in Mac OS X after Gatekeeper
Stefan Monnier: I think, Apple has made their stance quite clear by releasing the command line dev tools: I'm not sure what you mean by that, but looking at the history of Apple devices, especially the recent history with iPad, iPhone, etc... it's pretty clear to me where this is headed: keep as tight a control on the machine as possible without alienating too many users. It means that Apple likes to accommodate devs who prefer a traditional Unix environment over using IDEs (such as Xcode) and devs that use alternative tool chains (such as GHC). Manuel ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Data.Array.Accelerate initialization timings
Martin Dybdal: On 20 February 2012 16:39, Paul Sujkov psuj...@gmail.com wrote: Ah, it seems that I see now what's going wrong way. I'm not using the 'run' function from the CUDA backend, and so by default I guess the code is interpreted (the test backend used for semantics check). However, it's not perfectly clear how to use CUDA backend explicitly. Neither the interpreter or the CUDA code are used in your example. Everything in Data.Array.Accelerate are front-end stuff, your arrays are allocated on the host, so it is here there is an inefficiency. The use method inserts a statement in the syntax tree generated by the front-end, which the back-end can use as a hint to transfer that array to the GPU, while compiling the rest of the program into CUDA code. The Data.Array.Accelerate.CUDA.run function is the one that actually moves the arrays to the GPU. I haven't tried executing your code and I'm not sure why the front-end is that slow. The 'fromList' function is mostly meant for testing or to initialise small arrays. It is not particularly optimised. (Going via a vanilla list is just a bad idea if you want performance.) For efficient data marshalling have a look at the modules under Data.Array.Accelerate.IO. Manuel ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Haskell development in Mac OS X after Gatekeeper
Austin Seipp: The only two things not clear at this point, at least to me, are: 1) Will Apple require the paid development program, as opposed to the free one, if you only want to self-sign applications with a cert they trust? You can self-sign applications with a certificate that you get with a free developer ID. Cf. http://daringfireball.net/2012/02/mountain_lion Apple is calling it “Gatekeeper”. It’s a system whereby developers can sign up for free-of-charge Apple developer IDs which they can then use to cryptographically sign their applications. If an app is found to be malware, Apple can revoke that developer’s certificate, rendering the app (along with any others from the same developer) inert on any Mac where it’s been installed. In effect, it offers all the security benefits of the App Store, except for the process of approving apps by Apple. 2) What will the default Gatekeeper setting in Mountain Lion be? The default is the middle option — i.e., AppStore and self-signed apps run. From the same source, The default for this setting is, I say, exactly right: the one in the middle, disallowing only unsigned apps. This default setting benefits users by increasing practical security, and also benefits developers, preserving the freedom to ship whatever software they want for the Mac, with no approval process. In an ideal world, you won't require the paid dev ID (I don't know the expense of giving out certs however,) and the default setting would be App store + Dev signed. It is an ideal world :) Manuel ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Haskell development in Mac OS X after Gatekeeper
Austin Seipp: On Sun, Feb 19, 2012 at 8:39 PM, Tom Murphy amin...@gmail.com wrote: On the other hand, it's impossible for a software company to maintain a sense of professionalism, when a user has to know a weird secret handshake to disable what they may perceive as equivalent to antivirus software. I'll also just add that if you're an actual software company, large or small, the $100 for the developer ID, certificate, ability to do iOS/App store apps, whatever, is a business expense, that is utterly dominated by a million other factors, as developing high quality applications isn't exactly cheap, and the price of a license is really the last thing you're going to worry about. If you're more worried about the potential to impact individual developers and small open source teams who want to get their work out there, you are right it's a concern. I think, Apple has made their stance quite clear by releasing the command line dev tools: http://kennethreitz.com/xcode-gcc-and-homebrew.html Manuel ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] XCode Dependency for HP on Mac
In addition to the excellent reasons that Mark outlined, there is another important reason to *not* include gcc and friends in the HP. Every software developer (as opposed to friend of a friend who just wanted to try to learn programming with Haskell on a road trip) will already have Xcode installed on their Mac. Having two versions of gcc, make, lots of other tools, library headers, library objects, etc is going to lead to subtle bugs and headaches; at the latest, when you compile your first multi-language project. (This is where this is not comparable to the situation on Windows with mingw. A software developer on Windows, will have Visual Studio installed, but usually not some flavour of the GNU tools.) Manuel PS: I am sure there is demand for a self-contained, lightweight beginners/teaching Haskell environment, but let's not confuse that with the main distribution. Mark Lentczner: Hiho - I'm the maintainer of the Mac installer for HP. I thought I'd chime in a bit: On Mac OS X, developer tools is essentially synonymous with Xcode. That is, to get the set of standard utilities needed for development on compiled executables (notably the binutils), you install Xcode. True, it also includes the IDE called Xcode, but the vast bulk of that installation are things like headers, link libraries, command line tools, and other utilities for development of compiled executables in general. As several have pointed out, you can download Xcode for free. If you have Lion, you can get Xcode 4 for free from the Mac Store. Xcode 3 for 10.6 and 10.5. Traditionally, Apple has included Xcode on one of the CD-ROMs that came with a new computer, and/or as an installer already present on the hard disk. (I haven't bought a new Air... yet... but perhaps someone can check to see if the Xcode installer is one the SSD volume already?) It is conceivably possible to build and distribute some of those tools, but not the whole bundle. But the difficulty of getting such a build just right, and all the pieces in the right place, seems absurd to attempt to recreate when Apple has done it, and gives it away for free. Apple's versions of bintools also includes many extensions extra options for the OS X environment (like supporting multi-arch binaries) Finally, there is also licensing questions regarding the parts supplied by the OS vendor (headers, stub libs, debug libs, etc) Given the above, perhaps it is a little more clear why we choose to not include the system development tools in the Haskell Platform installer. - Mark ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Software patents covered in GHC?
Erik de Castro Lopo: Manuel M T Chakravarty wrote: In fact, you are better of not to know. Given that GHC (like all non-trivial software) surely infringes on some patents, the damages that a patent holder can sue you for are less if you do not know about the patents you are infringing on. IIRC, a plaintiff can triple the charges if they can reasonably show that you have been aware of the patents that you are infringing on. Nasty business! ON the up side, the fact that GHC is Open Source software available from a public repository and a lot of what is in GHC is published in papers which are widely and freely available on the internet means that stuf fthat was in GHC first can never be patented (or at least can be successfully challenged when it is). That's right, but it doesn't help any of us anything. The costs of defending against a patent claim (even if the claim can eventually be overturned) are much to high to bear for anybody, but major corporations. In other words, it doesn't matter if you are right or wrong if you can't pay the legal bill. This is not just theory as a fair number of mobile app developer recently found out: http://fosspatents.blogspot.com/2011/05/lodsys-sues-7-app-developers-in-eastern.html Manuel ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Software patents covered in GHC?
austin seipp: *sigh* CC'ing to the rest of haskell-cafe for completeness. I need to change 'reply all' to a default in my email I guess. On Mon, Jun 20, 2011 at 12:19 PM, austin seipp a...@hacks.yi.org wrote: Hello, Realistically, there probably is. Considering everything down to linked lists are patented by the USPO, I'd be willing to bet (at least a dollar or two) that there are many patents out there that apply to the code used in GHC. I don't know if you could say anything different about *any* nontrivial software, to be quite honest. IANAL however, so I won't attempt to claim in what countries these patents apply, nor could I cite you patent numbers (legalese being terse and software patents so seemingly open to interpretation sometimes, it would be hard to narrow down anyway I think.) In fact, you are better of not to know. Given that GHC (like all non-trivial software) surely infringes on some patents, the damages that a patent holder can sue you for are less if you do not know about the patents you are infringing on. IIRC, a plaintiff can triple the charges if they can reasonably show that you have been aware of the patents that you are infringing on. Nasty business! Manuel On Mon, Jun 20, 2011 at 12:10 PM, Shakthi Kannan shakthim...@gmail.com wrote: Hi, I would like to know if there are any software algorithms used in the Glasgow Haskell Compiler that have been patented? If yes, in which countries do they apply? Just curious to know. SK -- Shakthi Kannan http://www.shakthimaan.com ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe -- Regards, Austin -- Regards, Austin ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Haskell *interpreter* on iPad? (Scheme and Ocaml are there)
And while we are dreaming, in an iOS port of GHCi (meaning GHCi runs on iOS and doesn't just generate code for it), it would be great to make bytecode persistent — ie, the bytecode that GHCi currently generates internally to interpret programs should be serialized to save and load it. (Note that iOS apps are not allowed to generate binary code, so we wouldn't need the gcc tool chain etc, but just have a stripped down GHCi that generates bytecode only. All pre-compiled libraries that are part of the GHCi app can of course still be native code and load and interact with the interpreter as usual.) Manuel Don Stewart: Oh, Scheme is trivial to implement, when compared with Haskell. So people write it from scratch as a tutorial exercise. Haskell isn't trivial to implement from scratch, so instead we port existing implementations mostly. That means really, porting Hugs or GHC. And you've been pointed at examples. I think people are clearly keen for this, now it is a small matter of programming talent and will. -- Don On Sat, Jun 18, 2011 at 3:03 PM, John Velman vel...@cox.net wrote: On Sat, Jun 18, 2011 at 10:44:01PM +0400, MigMit wrote: Well, this is my point. THERE ARE 3 SCHEME INTERPRETERS in the iPad app store. They run on factory iPads, not jailbroken. The GUI for the gambitREPL (Read, Evaluate, Print, Loop) is just like a console. Input a scheme expression. CR. Answer appears, new prompt. In haskell we need to allow for some way to input layout. I don't recall how Hugs handles this, if at all. There are probably 5 or 10 people out there who want to learn functional programming, and they are studying Scheme on their iPads. Or Ocaml. I don't forsee doing production programming ON THE IPAD, but experimenting, testing some functions, and, by the way, learning Haskell. While I'm fantasizing, something like Hugs or ghci with SOE would really be neat. Sorry for shouting :-) John Velman Well, Haskell is fun, isn't it? And that's what iPhone is perfect for: fun. Back when I had iPod Touch 1G (jailbroken, of course), I used to run Hugs on it. Now I would love to see a Haskell interpreter in the App Store -- which, by the way, is possible; as there are Scheme interpreters there, why not Haskell? Отправлено с iPhone Jun 18, 2011, в 22:27, Jack Henahan jhena...@uvm.edu написал(а): I suppose you could make a GUI, by why? Given that you'll have to be working on a jailbroken device, anyway, one could just as well use one of the numerous terminal emulators now floating around for jailbroken iOS. That said, the idea of people writing Haskell on phones and iPads and so on makes me just a little bit grinny. On Jun 18, 2011, at 2:17 PM, Alexander Solla wrote: On Sat, Jun 18, 2011 at 10:46 AM, John Velman vel...@cox.net wrote: To further emphasize, I'd like to type in (or paste in) Haskell code and have it executed on the iPad. To reiterate: Something like Hugs, or ghci on the iPad. Since the iPhone OS is pretty much OS X for ARM, and GHC apparently now supports cross-compilation, you can compile GHC for iOS. I guess you could cross compile Hugs with GCC. Doing so probably isn't trivial, but it should be straightforward. I bet you could even use Xcode to make a graphical user interface to GHCi. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Status of Haskell + Mac + GUIs graphics
Jurriën Stutterheim: A few weeks ago I set out to build a GUI app using wxHaskell. Long story short, we ditched the entire idea of a desktop GUI and went for a web application instead, because it was easier to develop a front-end for it and it was easier to style it. So here's my (perhaps slightly provoking) question: do we need to care at all about good GUI toolkits being available? Web applications, especially with an HTML 5 front-end, have become increasingly more powerful. If we can also find a good, standardized way to generate JS from our Haskell code, we're pretty much all set. For cross-platform apps, I have to agree. The effort required to build and maintain a cross-platform GUI toolkit is hard to justify given HTML 5 and related technologies. Nevertheless, there are good reasons to develop native applications (especially on the Mac with its user-base spoiled by high-end UX). Luckily, the choice of toolkit is trivial in this case. For Mac OS, we need a Haskell-Cocoa binding. I don't think there are any serious technical obstacles to develop one. Somebody would just have to spend the time and effort to write one. Manuel On 18 May, 2011, at 08:29 , Tom Murphy wrote: I still haven't found any way to do GUIs or interactive graphics in Haskell on a Mac that isn't plagued one or more of the following serious problems: * Incompatible with ghci, e.g., fails to make a window frame or kills the process the second time one opens a top-level window, * Goes through the X server, and so doesn't look or act like a Mac app, * Doesn't support OpenGL. If there doesn't currently exist something without these handicaps, that's a serious problem for the use of Haskell for developing end-user software. If we as a community want to be able to develop software for end-users (i.e. people who'll be thrown off by gtk widgets or x11 windows)*, then it would be a very good idea to focus our energies on one or two promising pre-existing libraries, and hammer them into completion. A roadmap for this could be worked on at Hac Phi? Just my 2¢, Tom *This, of course, would NOT be avoiding success at all costs. :) ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Is Harper right that Haskell cannot model the natural numbers?
In this context, I'd suggest to have a look at the POPL'06 paper Fast and Loose Reasoning is Morally Correct http://www.comlab.ox.ac.uk/people/jeremy.gibbons/publications/fast+loose.pdf The paper is quite technical, so here the gist. It says that if you formally proof that two Haskell expressions do the same thing by reasoning *as if* you were using a total language (one without non-termination), then the two expressions are also morally the same in Haskell.[1] They formally define what morally the same means. In particular, the Introduction says: Our results justify the hand reasoning that functional programmers already perform, and can be applied in proof checkers and automated provers to justify ignoring ⊥-cases much of the time. In other words, yes, 'Nat' in Haskell is not the same as the natural numbers as axiomised by Peano. Does it matter? Not really. Manuel PS: Given that ML is impure, a lot of equational reasoning in ML is also no more than morally correct. [1] The paper doesn't show that statement for the entirety of Haskell, but for a core language with a comparable semantics using lifted types. Richard O'Keefe: In one of his blog posts, Robert Harper claims that the natural numbers are not definable in Haskell. SML datatype nat = ZERO | SUCC of nat Haskell data Nat = Zero | Succ Nat differ in that the SML version has strict constructors, and so only finite instances of nat can be constructed, whereas Haskell has lazy constructors, so inf = Succ inf is constructible, but that's not a natural number, and it isn't bottom either, so this is not a model of the natural numbers. Fair enough, but what about data Nat = Zero | Succ !Nat where the constructors *are* strict? It's perfectly good Haskell 98 as far as I can see. Now Nat itself isn't _quite_ a model of the naturals because it includes bottom, but then an SML function returning nat can also fail, so arguably SML's nat could or should be thought of as including bottom too. What am I missing? ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Robert Harper on monads and laziness
I completely agree that laziness enables a number of nice coding idioms and, as Lennart described so eloquently, it does facilitate a combinator-based coding style among other things: http://augustss.blogspot.com/2011/05/more-points-for-lazy-evaluation-in.html (Note that even Bob admits that this is an advantage.) What I meant is that if asked what is more important about Haskell, its laziness or purity, I think most people would pick purity. (But then it's a strange decision to make as laziness implies a need for purity as discussed.) Manuel Jan-Willem Maessen: On Tue, May 3, 2011 at 1:32 AM, Manuel M T Chakravarty c...@cse.unsw.edu.au wrote: ... Interestingly, today (at least the academic fraction of) the Haskell community appears to hold the purity of the language in higher regard than its laziness. As someone who implemented Haskell with quite a bit less laziness, I'm inclined to agree. That said, I think it's easy to underestimate just how much of the structure of the language really encourages a lazy evaluation strategy. One example: where blocks scope over groups of conditional RHSs. This is very handy, in that we can bind variables that are then used in some, but not all, of the disjuncts. Grabbing the first example that comes to hand from my own code: tryOne (gg, uu) e | not (consistent uu) = (gg', uu) | uu==uu' = (gg, uu) | otherwise = (gg', uu') where gg' = gg `addEquation` e uu' = uu `addEquation` e This kind of thing happens all over the place in Haskell code -- it's a very natural coding style -- but if you want to preserve purity it's tough to compile without laziness. -Jan-Willem Maessen ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Robert Harper on monads and laziness
Tony Morris: Interesting how I have been authoring and subsequently using monads in scala for several years and it is strictness that gets in the way more than anything. Just to make sure that I understand you correctly. You are saying that when you use monads in Scala, then strictness makes that more awkward than necessary. (I assume that you are *not* saying that strictness is the most awkward language feature of Scala.) Why is that? Manuel ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Robert Harper on monads and laziness
For a historical perspective, I highly recommend The Definitive Account of the History of Haskell: http://research.microsoft.com/en-us/um/people/simonpj/papers/history-of-haskell/index.htm Section 7 clearly and directly cites the desire to have pure I/O as the motivation for adopting monads. As you are saying that doesn't directly contradict the statement of Bob that you cite. In fact, Section 3.2 of the above paper supports the opinion that purity is a consequence of choosing to be lazy, but it also claims that the combination of power and beauty of a pure language motivated the language designers. Interestingly, today (at least the academic fraction of) the Haskell community appears to hold the purity of the language in higher regard than its laziness. Manuel Ketil Malde: I'm following Harper's blog, Existential Type¹, which I find to be an enjoyable and entertainingly written tirade about the advantages of teaching functional programming - specifically ML - to students. Of course, he tends to be critical of Haskell, but it's nice to get some thought provoking opinion from somebody who knows a bit about the business. Recently, he had a piece on monads, and how to do them in ML, and one statement puzzled me: There is a particular reason why monads had to arise in Haskell, though, which is to defeat the scourge of laziness. My own view is/was that monads were so successful in Haskell since it allowed writing flexible programs with imperative features, without sacrificing referential transparency. Although people are quick (and rightly so) to point out that this flexibility goes way beyond IO, I think IO was in many ways the killer application for monads. Before IO, we had very limited functionality (like 'interact' taking a 'String - String' function and converting it into an exectuable program) to build real programs from. Laziness does require referential transparency (or at least, it is easier to get away with the lack of RT in a strict language), so I can see that he is indirectly correct, but RT is a goal in itself. Thus, I wonder if there are any other rationale for a statement like that? -k ¹ http://existentialtype.wordpress.com/ -- If I haven't seen further, it is by standing in the footprints of giants ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] DPH and GHC 7.0.1
Andrew Coppin: On 19/11/2010 11:39 PM, David Peixotto wrote: There were some problems getting DPH to work well with the changes in GHC 7. There is more info in this mail: http://www.haskell.org/pipermail/cvs-ghc/2010-November/057574.html The short summary is that there will be a patch level release of GHC (7.0.2) that works well with DPH and the DPH packages will then be available for installation from Hackage. If you want to play with DPH now you can do so on GHC HEAD. -David I was wondering about this myself, actually. I'm especially surprised since I thought the DPH implementation was hard-wired into the compilter itself (in which case, how can you distribute it seperately?) Then again, I've never yet even tried using DPH. (The wiki page looks very out of date, so I don't know how much to trust its information.) As David said, we will release the DPH libraries separately, but at the same time as GHC 7.0.2. DPH consists essentially of two components (a) the vectoriser, a program transformer hardwired into GHC and (b) the DPH libraries. At the request of the Haskell Platform people we separated the DPH library packages from the standard GHC distribution and will distribute them via Hackage. The wiki page will be updated in time for that release. Manuel PS: We didn't release DPH with GHC 7.0.1 as we still had bugs to fix from recent major changes at the time of the 7.0.1 release and didn't want to hold up the GHC release.___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: [Haskell] Proposal: Form a haskell.org committee
Ian Lynagh: To fix this problem, we propose that we create a haskell.org committee, which is responsible for answering these sorts of questions, although for some questions they may choose to poll the community at large if they think appropriate. [..] Unfortunately, this gives us a bootstrapping problem, so we suggest that the initial committee be chosen from open nominations by some of the people who currently de-facto end up making the decisions currently: Duncan Coutts, Isaac Jones, Ian Lynagh, Don Stewart and Malcolm Wallace. These 5 would still be elligible to nominate themselves. Two of the initial members will stand down after one year, and two after two years, in order to bootstrap rolling membership turnover. Good plan! Manuel ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Multidimensional Matrices in Haskell
Hi Mihai, A friend of mine wanted to do some Cellular Automata experiments in Haskell and was asking me what packages/libraries are there for multidimensional matrices. I'm interested in both immutable and mutable ones but I don't want them to be trapped inside a monad of any kind. You may like to have a look at the recently released Repa library: http://hackage.haskell.org/package/repa There is a draft paper about it: http://www.cse.unsw.edu.au/~chak/papers/KCLPL10.html Manuel ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Proposal: Australian Hackathon
1) Who's interested Interest, yes, but time is a very scarce resource these days... 2) What dates are good Midyear break is 29 Jun to 18 Jul at UNSW, but I'm away for a week in that time period. 3) What projects people want to work on To be honest, I'd probably be in and out and, on a weekend, have one or two kids running around me. So, working with and maybe coaching some people on code I'm familiar with is probably the most realistic. That could be Accelerate, GHC, or DPH. 4) Where we can host this As Ben said, we should be able to organise a room at UNSW. Exactly how we get people on the network here (esp on a weekend), I'm less sure, but we could try to organise some guest accounts on the wireless or wired net — unless people want to bring 3G dongles or iPhones to tether. OK, so we have a fair number of people indicating interest... so which weekend would be preferred? [..] Or should we take this to the wiki rather than the mailing list? I'd suggest to do the planning of details on a wiki page. Manuel ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] How many Haskell Engineer I/II/IIIs are there?
John Van Enk: consider presenting at CUFP this year Any word on when this will be? It'll be before or after (I suspect the later) ICFP http://www.icfpconference.org/icfp2010/, which is September 27-29 in Baltimore, Maryland. Manuel ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] OpenCL target for DPH?
Marcus Daniels wrote, I'm wondering if anyone has looked at OpenCL as target for Data Parallel Haskell? Specifically, having Haskell generate CL kernels, i.e. SIMD vector type aware C language backend, as opposed to just a Haskell language binding. The short answer is that there is currently no plan to directly target OpenCL from DPH. (That is the DPH team doesn't have any such plans, but if anybody else wants to give it a shot, the latest, bleeding edge DPH code is always available in the GHC HEAD repository.) The long answer is that we are currently working on two separate data-parallel extensions for Haskell. Data Parallel Haskell http://haskell.org/haskellwiki/GHC/Data_Parallel_Haskell ~ Here the focus is *expressiveness*. In particular, we support arbitrarily deep, dynamic nesting of dataparallel computations with full support of higher-order functions (ie, parallel arrays of functions are fine). However, to keep the work manageable, we only target multicore CPUs for the moment (using the multi-threading support in GHC's RTS). Data.Array.Accelerate http://www.cse.unsw.edu.au/~chak/project/accelerate/ ~ Here the focus is on targeting *exotic, high-performance hardware*. We are currently working on a CUDA backend targeting CUDA-capable NVIDIA GPUs, but it shouldn't be too hard to re-target that to OpenCL. Support for the Cell BE and FPGAs appears feasible, too (but we lack local expertise and hardware to write such backends ourselves). However, to keep the work manageable, we only consider regular, multi-dimensional array codes encoded in an embedded DSL where functions are not first-class (ie, we use Haskell's first-class functions to implement the EDSL, but the embedded language is first-order). Longer term future ~~ At some point, we would of course like to bring the above two projects together, but at the moment, each is already rather challenging just by itself. Manuel ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] university courses on type families/GADTs?
Tom Schrijvers wrote, I was wondering whether there are any universities that teach about Haskell type families or GADTs? I do in my course Language-based Software Safety (both TFs and GADTs). It's an advanced, research-oriented course for 4th year undergraduate and for postgraduate students. (It wasn't offered last year and this year, but will be again offered next year.) Manuel ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Bulding a library for C users on OS X
Chris Eidhof: I'm trying to call a Haskell function from C, on OS X. There's an excellent post [1] by Tomáš Janoušek that explains how to do this on Linux. However, on OS X, it's different. First of all, it looks like the -no-hs-main flag is ignored, because I get the following error: ghc -O2 --make -no-hs-main -optl '-shared' -optc '- DMODULE=Test' -o Test.so Test.hs module_init.c [1 of 1] Compiling Main ( Test.hs, Test.o ) Test.hs:1:0: The function `main' is not defined in module `Main''' The flag -no-hs-main is a link-time flag that allows you to link without a main function, but you are getting a compile time error. It's as if you try to export main, but don't define it. Have you had a look at http://www.haskell.org/ghc/docs/latest/html/users_guide/ffi-ghc.html#foreign-export-ghc ? Manuel ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Type-level naturals multiplication
Reid Barton: On Sat, Oct 10, 2009 at 02:59:37PM -0400, Brad Larsen wrote: Suppose we implement type-level naturals as so: data Zero data Succ a Then, we can reflect the type-level naturals into a GADT as so (not sure if ``reflect'' is the right terminology here): data Nat :: * - * where Zero :: Nat Zero Succ :: Nat a - Nat (Succ a) Using type families, we can then proceed to define type-level addition: type family Add a b :: * type instance Add Zero b = b type instance Add (Succ a) b = Succ (Add a b) Is there any way to define type-level multiplication without requiring undecidable instances? I hesitate to contradict Manuel Chakravarty on this subject... but I posted a type-level multiplication program without undecidable instances on this list in June: http://www.haskell.org/pipermail/haskell-cafe/2009-June/062452.html If you prefer to use EmptyDataDecls, you can replace the first four lines by data Z data S n data Id :: * - * data (:.) :: (* - *) - (* - *) - (* - *) And I still don't understand why that definition works while the obvious one doesn't :) Ok, I should have been more precise. It's not that anything about multiplication as such is a problem. However, when you look at the standard definitions for addition type family Add a b :: * type instance Add Zero b = b type instance Add (Succ a) b = Succ (Add a b) and multiplication type family Mul a b :: * type instance Mul Zero b = Zero type instance Mul (Succ a) b = Add (Mul a b) b then the difference is that multiplication uses nested applications of type families (namely, Add (Mul a b) b). It is this nested application of type families that can be abused to construct programs that lead to non-termination of type checking (by exploiting the openness of type families in combination with local equalities introduced either by equality constraints in type signatures or GADT pattern matches). Unfortunately, there doesn't seem to be a simple syntactic criterion that would let GHC decide between harmless and problematic uses of nested *open* family applications in family instances. Hence, we need to rule them all out. You circumvent that problem cleverly by the use of higher-kinded types. Manuel ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Graph Library Using Associated Types
Lajos Nagy: I understand that one of the original motivations for introducing associated types to Haskell was the survey of support for generic programming done by Garcia et al. where they compared the implementation of the Boost Graph Library in various languages (C++, Java, Haskell, ML, C#, Eiffel). Haskell got full marks in all categories, except for associated types which made the resulting implementations more verbose than necessary (and exposed implementation details). Since then GHC added support for associated types but I was wondering if anybody re-did the experiment with the new features enabled (the original code is available at: http://www.osl.iu.edu/research/comparing/). No, we actually didn't do that. It would be interesting, though. Manuel ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Type-level naturals multiplication
Brad Larsen: Suppose we implement type-level naturals as so: data Zero data Succ a Then, we can reflect the type-level naturals into a GADT as so (not sure if ``reflect'' is the right terminology here): data Nat :: * - * where Zero :: Nat Zero Succ :: Nat a - Nat (Succ a) Using type families, we can then proceed to define type-level addition: type family Add a b :: * type instance Add Zero b = b type instance Add (Succ a) b = Succ (Add a b) Is there any way to define type-level multiplication without requiring undecidable instances? No, not at the moment. The reasons are explained in the paper Type Checking with Open Type Functions (ICFP'08): http://www.cse.unsw.edu.au/~chak/papers/tc-tfs.pdf We want to eventually add closed *type families* to the system (ie, families where you can't add new instances in other modules). For such closed families, we should be able to admit more complex instances without requiring undecidable instances. Manuel ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Type families in export lists
Lee Duhem: On Sat, May 30, 2009 at 7:35 PM, Maurí cio briqueabra...@yahoo.com wrote: Hi, How do I include type families (used as associated types) in a module export list? E.g.: class MyClass a where type T a :: * coolFunction :: Ta - a (...) If I just include MyClass and its functions in the list, instances in other modules complain they don't know T, but I wasn't able to find how (where) to include T in the list. In export list, you can treat 'type T a' as normal type declaration, ie, write T(..) in export list. There is also special syntax to export associated types. You can write MyClass (type T) in the export list; cf, http://haskell.org/haskellwiki/GHC/Type_families#Import_and_export Manuel ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] haskell cuda?
Dan: Doesn't look like there's code out there - will try e-mailing the authors of the various papers/presentations. We haven't made any code available yet, but we are planning to do so before ICFP this year. This e-mail also counts as an open plea to those compiler wizards working on this stuff: feel free to put beta buggy versions of your code online :) It's not so much the beta bugginess as the several times completely ripping apart and putting together in different ways that prevented us from putting code out. Once we put something out, it becomes harder to change the API, too, and we are still changing the design of that around. Anyway, thanks for the interest. Manuel Scott A. Waterman wrote: Try reaching Manuel Chakravarty, http://justtesting.org/ and his colleague Sean Lee at Galois. Slides from his talk on GPU.gen : Just gave my talk on Data Parallelism in Haskell at PSU; here the slides: http://bit.ly/17EQcl and slides from an earlier Galois talk: http://www.galois.com/blog/2008/08/29/gpugen-bringing-the-power-of-gpus-into-the-haskell-world/ --ts On May 12, 2009, at 9:18 AM, Dan wrote: Hi, Does anyone know if there's a compiler from Data-Parallel Haskell to GPU code? I saw a paper on it a while back, but Google hasn't turned up any code. Cheers, - Dan ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Generating Haskell with associated types (and kind annotations)
Hi Dan, I was wondering whether anyone had any suggestions on a good way to generate repetitive code with associated types and kind annotations. I'd like to use TH but as far as I understand, it doesn't support this yet (I think associated types are in HEAD but not kinds), I implemented type families (including associated types) and kinds for TH in the HEAD. If there is anything missing that prevents you from using it, please let me know and I'll have a look at it. Manuel ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Strange type error with associated type synonyms
Matt Morrow: On Mon, Apr 6, 2009 at 7:39 PM, Manuel M T Chakravarty c...@cse.unsw.edu.au wrote: Peter Berry: 3) we apply appl to x, so Memo d1 a = Memo d a. unify d = d1 But for some reason, step 3 fails. Step 3 is invalid - cf, http://www.haskell.org/pipermail/haskell-cafe/2009-April/059196.html . More generally, the signature of memo_fmap is ambiguous, and hence, correctly rejected. We need to improve the error message, though. Here is a previous discussion of the subject: http://www.mail-archive.com/haskell-cafe@haskell.org/msg39673.html Manuel The thing that confuses me about this case is how, if the type sig on memo_fmap is omitted, ghci has no problem with it, and even gives it the type that it rejected: Basically, type checking proceeds in one of two modes: inferring or checking. The former is when there is no signature is given; the latter, if there is a user-supplied signature. GHC can infer ambiguous signatures, but it cannot check them. This is of course very confusing and we need to fix this (by preventing GHC from inferring ambiguous signatures). The issue is also discussed in the mailing list thread I cited in my previous reply. Manuel PS: I do realise that ambiguous signatures are the single most confusing issue concerning type families (at least judging from the amount of mailing list traffic generated). We'll do our best to improve the situation before 6.12 comes out.___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Strange type error with associated type synonyms
Peter Berry:
{-# LANGUAGE TypeFamilies, TypeSynonymInstances,
ScopedTypeVariables #-}
The following is a class of memo tries indexed by d:
class Fun d where
type Memo d :: * - *
abst :: (d - a) - Memo d a
appl :: Memo d a - (d - a)
-- Law: abst . appl = id
-- Law: appl . abst = id (denotationally)
Any such type Memo d is naturally a functor:
memo_fmap f x = abst (f . appl x)
The type of memo_fmap (as given by ghci) is (Fun d) = (a - c) -
Memo d a - Memo d c. (Obviously this would also be the type of fmap
for Memo d, so we could declare a Functor instance in principle.) If
we add this signature:
memo_fmap' :: Fun d = (a - b) - Memo d a - Memo d b
memo_fmap' f x = abst (f . appl x)
it doesn't type check:
TypeSynonymTest.hs:14:17:
Couldn't match expected type `Memo d1 b'
against inferred type `Memo d b'
In the expression: abst (f . appl x)
In the definition of `memo_fmap'':
memo_fmap' f x = abst (f . appl x)
TypeSynonymTest.hs:14:32:
Couldn't match expected type `Memo d a'
against inferred type `Memo d1 a'
In the first argument of `appl', namely `x'
In the second argument of `(.)', namely `appl x'
In the first argument of `abst', namely `(f . appl x)'
Failed, modules loaded: none.
As I understand it, the type checker's thought process should be along
these lines:
1) the type signature dictates that x has type Memo d a.
2) appl has type Memo d1 a - d1 - a for some d1.
3) we apply appl to x, so Memo d1 a = Memo d a. unify d = d1
But for some reason, step 3 fails.
Step 3 is invalid - cf, http://www.haskell.org/pipermail/haskell-cafe/2009-April/059196.html
.
More generally, the signature of memo_fmap is ambiguous, and hence,
correctly rejected. We need to improve the error message, though.
Here is a previous discussion of the subject:
http://www.mail-archive.com/haskell-cafe@haskell.org/msg39673.html
Manuel
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Type families and kind signatures
Louis Wasserman: Mkay. I get it now. I was under the impression that, essentially, a data family was precisely equivalent to a type family aliasing to a separately declared datatype. No, they are not equivalent. You can see that as follows. Assume, data family T a type family S a Now, given `T a ~ T b', we know that `a ~ b'. (We call this implication decomposition.) In contrast, given `S a ~ S b' we do *not* know whether `a ~ b'. Why not? Consider the instances type instance S Int = Bool type instance S Float = Bool Clearly, `S Int ~ S Float', but surely not `Int ~ Float'. So, decomposition does not hold for type synonym families, but it does hold for data families. This is actually, not really a property of type *families* alone. It already distinguishes vanilla data types from vanilla type synonyms. We know, say, that if `Maybe a ~ Maybe b', then `a ~ b'. However, given type Const a = Int we have `Const Int ~ Const Float' (and still not `Int ~ Float'). Definitions, such as that of `Const', are rarely used, which is why this issue doesn't come up much until you use type families. One more question: is there any way to get the low overhead of newtypes for particular instances of a data family? Is this impossible? That is, is there any way to do something like data family Foo a data instance Foo Int = Bar Int -- Bar is actually a newtype You can use newtype instance Foo Int = MkFoo Int So, the instances of a data family can be data or newtype instances., and you can freely mix them. Manuel On Thu, Apr 2, 2009 at 12:47 PM, David Menendez d...@zednenem.com wrote: 2009/4/2 Louis Wasserman wasserman.lo...@gmail.com: Mkay. One more quick thing -- the wiki demonstrates a place where the original attempt worked, with a data family instead. (That is, replacing 'type' with 'data' and adjusting the instance makes this program compile immediately.) a) Is there a type-hackery reason this is different from data families? It's not type hackery. Data families are different from type families, and the syntax for declaring instances of higher-kinded families is a consequence of those differences. An instance of a data family is a new type constructor, so you have to provide the additional arguments in order to declare the data constructors. data family Foo a :: * - * data instance Foo Bool a = FB a a -- Foo Bool has kind * - *, like [], so I could make it a Functor Instance of type families are always pre-existing type constructors. type family Bar a :: * - * -- Bar a must equal something of kind * - * type instance Bar () = Maybe b) Is there a reason this isn't made a lot clearer in the documentation? GHC's docs say that higher-order type families can be declared with kind signatures, but never gives any examples -- which would make it a lot clearer that the below program doesn't work. Here's a higher-kinded type family I've used. type family Sig t :: * - * class (Traversable (Sig t)) = Recursive t where roll :: Sig t t - t unroll :: t - Sig t t The Traversable context wouldn't be valid if I had declared Sig t a :: *, because type families must always be fully applied. The difference is analogous to the difference between type M0 a = StateT Int IO a type M1 = StateT Int IO Since type synonyms (like type and data families) must always be fully applied, you can use M1 in places where you can't use M0, even though they're effectively the same thing. foo :: ErrorT String M1 a -- valid bar :: ErrorT String M0 a -- not valid -- Dave Menendez d...@zednenem.com http://www.eyrie.org/~zednenem/ ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] ANNOUNCE: vacuum-cairo: a cairo frontend to vacuum for live Haskell data visualization
Don Stewart: Is there a Mac OSX packaging team? Unfortunately, it's not just a packaging problem. (Well, packing of Haskell libraries, that is.) There are two version of GTK+ Mac OS X: (1) the MacPorts version and (2) a native GTK+ framework. Unfortunately, both are not satisfactory. The MacPorts version is based on X windows, which is supported on Macs right out of the box, but to be honest, X programs on the Mac are ugly and annoying. Moreover, whether the MacPorts version builds at all seems to be a matter of luck - I have been out of luck more than once. MacPorts is also pretty useless once you want to distribute your GTK-GUI programs to other Mac users. The native GTK+ framework is a port of GTK+ to the native Mac GUI and dead easy to install (it has a binary installer). Unfortunately, it lacks many of GTK+'s optional components (most notably libglade). It is however in beta right now, so we can only hope that there will be more of the optional components in the final version. Manuel sebf: On Mar 31, 2009, at 7:40 AM, Don Stewart wrote: I am pleased to announce the release of vacuum-cairo, a Haskell library for interactive rendering and display of values on the GHC heap using Matt Morrow's vacuum library. Awesome! I want to try this. I have problems though installing it on an Intel MacBook running $ ghc --version The Glorious Glasgow Haskell Compilation System, version 6.10.1 $ cabal --version cabal-install version 0.6.2 using version 1.6.0.2 of the Cabal library $ ghc-pkg list gtk /Library/Frameworks/GHC.framework/Versions/610/usr/lib/ghc-6.10.1/./ package.conf: gtk-0.10.0 I have installed gtk2hs using the instructions at http://www.haskell.org/haskellwiki/Gtk2Hs#Using_the_GTK.2B_OS_X_Framework A simple cabal update; cabal install vacuum-cairo gives me: $ cabal install vacuum-cairo Resolving dependencies... cabal: cannot configure vacuum-cairo-0.3.1. It requires svgcairo -any There is no available version of svgcairo that satisfies -any I have installed libsvg-cairo using MacPorts and it seems installed in /opt/local/lib: $ ls /opt/local/lib/libsvg-cairo.* /opt/local/lib/libsvg-cairo.1.0.1.dylib /opt/local/lib/libsvg-cairo.1.dylib /opt/local/lib/libsvg-cairo.a /opt/local/lib/libsvg-cairo.dylib /opt/local/lib/libsvg-cairo.la But cabal-install still gives the same error. Even with --extra-lib- dirs set: $ cabal install --extra-lib-dirs=/opt/local/lib/ vacuum-cairo Resolving dependencies... cabal: cannot configure vacuum-cairo-0.3.1. It requires svgcairo -any There is no available version of svgcairo that satisfies -any Hence, I downloaded the tarball and tried to use this instead to install vacuum-cairo, which lead to another problem: I cannot install the vacuum package because of a dependencies conflict due to the package ghc-6.10.1 requiring two different versions of process: $ cabal install vacuum Resolving dependencies... cabal: dependencies conflict: ghc-6.10.1 requires process ==1.0.1.1 however process-1.0.1.1 was excluded because ghc-6.10.1 requires process ==1.0.1.0 Funny. Any ideas on how to get this cool package installed? Thanks! Sebastian ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Status of Haskell under OsX
Ross Mellgren: I use this configuration exclusively... it wasn't actually that hard to set up once I found out that the .pc files are shipped in a strange directory buried in the frameworks. I posted how I got it working back in December: http://sourceforge.net/mailarchive/message.php?msg_name=3E883695-30D3-4CBE-AD14-B08C24D343EF%40z.odi.ac That does work nicely. Thanks for the pointer. I added a paragraph on the Haskell wiki for easy reference: http://www.haskell.org/haskellwiki/Gtk2Hs#Using_the_GTK.2B_OS_X_Framework Manuel On Mar 2, 2009, at 6:39 PM, Manuel M T Chakravarty wrote: BTW, there is a nice native version of GTK for Mac OS X as a proper framework: http://www.gtk-osx.org/ Unfortunately, it seems rather difficult to build gtk2hs with the GTK+ framework as the framework doesn't support pkg-config and gtk2hs knows nothing about Mac frameworks. However, GHC has support for frameworks; so, it should be possible to get this to work. Manuel Arne Dehli Halvorsen: Manuel M T Chakravarty wrote: I'm planning to purchase a MacBookPro so I'm wondering how well Haskell is supported under this platform. At least two of the regular contributors to GHC work on Macs. That should ensure that Mac OS X is well supported. Installation is trivial with the Mac OS X installer package: http://haskell.org/ghc/download_ghc_6_10_1.html#macosxintel Hi, following on from this point: How does one get gtk2hs running on a mac? I have a MacBook Pro, and I've had ghc installed for some time now. (first in 6.8.2 (packaged), then 6.10.1 (packaged), then 6.8.2 via macports 1.6 then 6.10.1 via macports 1.7) I tried to install gtk2hs via macports, but it didn't work. (0.9.12? on 6.8.2, then on 6.10.1) Is there a recipe one could follow? Can I get the preconditions via macports, and then use cabal to install gtk2hs 0.10? Grateful for assistance, Arne D H Manuel ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Status of Haskell under OsX
BTW, there is a nice native version of GTK for Mac OS X as a proper framework: http://www.gtk-osx.org/ Unfortunately, it seems rather difficult to build gtk2hs with the GTK+ framework as the framework doesn't support pkg-config and gtk2hs knows nothing about Mac frameworks. However, GHC has support for frameworks; so, it should be possible to get this to work. Manuel Arne Dehli Halvorsen: Manuel M T Chakravarty wrote: I'm planning to purchase a MacBookPro so I'm wondering how well Haskell is supported under this platform. At least two of the regular contributors to GHC work on Macs. That should ensure that Mac OS X is well supported. Installation is trivial with the Mac OS X installer package: http://haskell.org/ghc/download_ghc_6_10_1.html#macosxintel Hi, following on from this point: How does one get gtk2hs running on a mac? I have a MacBook Pro, and I've had ghc installed for some time now. (first in 6.8.2 (packaged), then 6.10.1 (packaged), then 6.8.2 via macports 1.6 then 6.10.1 via macports 1.7) I tried to install gtk2hs via macports, but it didn't work. (0.9.12? on 6.8.2, then on 6.10.1) Is there a recipe one could follow? Can I get the preconditions via macports, and then use cabal to install gtk2hs 0.10? Grateful for assistance, Arne D H Manuel ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Status of Haskell under OsX
I'm planning to purchase a MacBookPro so I'm wondering how well Haskell is supported under this platform. At least two of the regular contributors to GHC work on Macs. That should ensure that Mac OS X is well supported. Installation is trivial with the Mac OS X installer package: http://haskell.org/ghc/download_ghc_6_10_1.html#macosxintel Manuel ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Comparison of functional dependencies and type families [was: Re: Type families not as useful over functions]
Just for the record, here a few clarifications. Expressiveness ~~ From a theoretical point of view, type families (TFs) and functional dependencies (FDs) are equivalent in expressiveness. There is nothing that you can do in one and that's fundamentally impossible in the other. See also Related Work in http://www.cse.unsw.edu.au/~chak/papers/SPCS08.html . In fact, you could give a translation from one into the other. Haskell ~~~ This simple equivalence starts to break down when you look at the use of the two language features in Haskell. This is mainly because there are some syntactic contexts in Haskell, where you can have types, but no class contexts. An example, are newtype definitions. Implementation in GHC ~ The situation becomes quite a bit more tricky once you look at the interaction with other type system features and GHC's particular implementation of FDs and TFs. Here the highlights: * GADTs: - GADTs and FDs generally can't be mixed (well, you can mix them, and when a program compiles, it is type correct, but a lot of type correct programs will not compile) - GADTs and TFs work together just fine * Existential types: - Don't work properly with FDs; here is an example: class F a r | a - r instance F Bool Int data T a = forall b. F a b = MkT b add :: T Bool - T Bool - T Bool add (MkT x) (MkT y) = MkT (x + y) -- TYPE ERROR - Work fine with TFs; here the same example with TFs type family F a type instance F Bool = Int data T a = MkT (F a) add :: T Bool - T Bool - T Bool add (MkT x) (MkT y) = MkT (x + y) (Well, strictly speaking, we don't even need an existential here, but more complicated examples are fine, too.) * Type signatures: - GHC will not do any FD improvement in type signatures; here an example that's rejected as a result (I assume Hugs rejects that, too): class F a r | a - r instance F Bool Int same :: F Bool a = a - Int same = id -- TYPE ERROR (You may think that this is a rather artificial example, but firstly, this idiom is useful when defining abstract data types that have a type dependent representation type defined via FDs. And secondly, the same situation occurs, eg, when you define an instance of a type class where one method has a class context that contains a type class with an FD.) - TFs will be normalised (ie, improved) in type signatures; the same example as above, but with a TF: type family F a type instance F Bool = Int same :: F Bool - Int same = id * Overlapping instances: - Type classes with FDs may use overlapping instances (I conjecture that this is only possible, because GHC does not improve FDs in type signatures.) - Type instances of TFs cannot use overlapping instances (this is important to ensure type safety) It's a consequence of this difference that closed TFs are a features that is requested more often than closed classes with FDs. Manuel PS: Associated types are just syntactic sugar for TFs, there is nothing that you can do with them that you cannot do with TFs. Moreover, it is easy to use type families for bijective type functions; cf. http://www.haskell.org/pipermail/haskell-cafe/2009-January/053696.html . (This follows of course from the equivalence of expressiveness of TFs and FDs.) Ahn, Ki Yung: My thoughts on type families: 1) Type families are often too open. I causes rigid variable type error messages because when I start writing open type functions, I often realize that what I really intend is not truly open type functions. It happens a lot that I had some assumptions on the arguments or the range of the type function. Then, we need help of type classes to constrain the result of open type functions. For example, try to define HList library using type families instead of type classes with functional dependencies. One will soon need some class constraints. Sometimes, we can use associated type families, but many times it may become tedious when there are multiple arguments and result have certain constraints so that we might end up associating/splitting them over multiple type classes. In such cases, it may be more simple working with functional dependencies alone, rather than using both type classes and type families. I wish we had closed kinds so that we can define closed type functions as well as open type functions. 2) Type families are not good when we need to match types back and forth (e.g. bijective functions), or even multiple ways. We need the help of functional dependencies for these relational definitions. I know that several people are working on the unified implementation for both type families and functional dependencies. Once GHC have common background implementation, type families will truly be syntactic
Re: [Haskell-cafe] (Off-topic) CUDA
Malcolm Wallace: (Also... Haskell on the GPU. It's been talked about for years, but will it ever actually happen?) gpu is just set of simd-like instructions. so the reason why you will never see haskell on gpu is the same as why you will never see it implemented via simd instructions :D Because SIMD/GPU deals only with numbers, not pointers, you will not see much _symbolic_ computation being offloaded to these arithmetic units. But there are still great opportunities to improve Haskell's speed at numerics using them. And some symbolic problems can be encoded using integers. There are at least two current (but incomplete) projects in this area: Sean Lee at UNSW has targetted Data Parallel Haskell for an Nvidia GPGPU, and Joel Svensson at Chalmers is developing a Haskell- embedded language for GPU programming called Obsidian. We have a paper about the UNSW project now. It is rather high-level, but has some performance figures of preliminary benchmarks: http://www.cse.unsw.edu.au/~chak/papers/LCGK09.html BTW, this is currently independent of Data Parallel Haskell. It is a flat data-parallel array language embedded in Haskell. The language is restricted in a manner that we can generate GPU code (CUDA to be precise) from it. In the longer run, we want to turn this into a backend of Data Parallel Haskell, but that will require quite a bit more work. Manuel ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Problems running vectorised dph program
Hi Fabian,
I've just begun to play with Data Parallel Haskell but instantly ran
into a
problem. My very stupid but very simple example ought to sum the
values of
all Nodes in a Tree. The non-vectorised code behaves like I
expected, the
vectorised code doesn't terminate. I compiled and ran it the same
way as the
example in the tutorial:
ghc -c -O -fdph-par Main.hs
ghc -c -Odph -fcpr-off -fdph-par MinimalParTree.hs
ghc -o MinimalParTree -fdph-par -threaded MinimalParTree.o Main.o
./MinimalParTree
My question is: Is this a bug or is something wrong with the program?
This appears to be a bug in the DPH libraries. Can you please file a
bug report at http://hackage.haskell.org/trac/ghc?
For the time being, you can change sumTree as follows to get your
program working:
sumTree :: Tree Int - Int
sumTree (Node x ns)
| lengthP ns == 0 = x
| otherwise = x + sumP (mapP sumTree ns)
Thanks for the report,
Manuel
module Main where
import MinimalParTree
main = do
print $ sumTreeWrapper 20
{-# LANGUAGE PArr, ParallelListComp #-}
{-# OPTIONS -fvectorise #-}
module MinimalParTree (sumTreeWrapper) where
import qualified Prelude
import Data.Array.Parallel.Prelude
import Data.Array.Parallel.Prelude.Int
data Tree a = Node a [: Tree a :]
testTree :: Int - Tree Int
testTree elem = Node elem emptyP
sumTree :: Tree Int - Int
sumTree (Node x ns) = x + sumP (mapP sumTree ns)
{-# NOINLINE sumTreeWrapper #-}
sumTreeWrapper :: Int - Int
sumTreeWrapper elem =
sumTree (testTree elem)
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Type family problem
Gleb Alexeyev: Sjoerd Visscher wrote: When I try this bit of code: class C1 a where type F a :: * x :: F a y :: F a x = y I get this error: Couldn't match expected type `F a1' against inferred type `F a' In the expression: y In the definition of `x': x = y I can't figure out what is going on or how I should fix this. The discussion [1] seems to be related. [1] http://hackage.haskell.org/trac/ghc-test/ticket/2855 Exactly. See also the related ticket http://hackage.haskell.org/trac/ghc-test/ticket/1897 In short, the signature F a is ambiguous (as `a' only occurs as a parameter of a synonym family in the signature). Functions with an ambiguous signature are generally unusable (even if the compiler accepts the definition initially). Manuel ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Comments from OCaml Hacker Brian Hurt
I have to say, I agree with Lennart here. Terms like monoid have had a precise definition for a very long time. Replacing an ill-defined term by a vaguely defined term only serves to avoid facing ones ignorance - IMHO an unwise move for a technical expert. Learning Haskell has often been described as a perspective changing, deeply enlightening process. I believe this is because the language and the community favours drilling down to the core of a problem and exposing its essence in the bright light of mathematical precision. It would be a mistake to give up on that. We could call lambda abstraction, name binder, and we could call the lambda calculus, rule system to manipulate name bindings. That would avoid some scary greek. Would it make functional programming any easier? In contrast, even the planned new C++0x standard uses our terminology: http://en.wikipedia.org/wiki/C%2B%2B0x#Lambda_functions_and_expressions Ok, ok, they do mutilate the whole idea quite brutally, but the point is, we got in their heads. That counts. I am all for helping beginners to learn, but I am strongly against diluting what is being learnt. If some of our terminology is a problem, we need to explain it better. Manuel Lennart Augustsson: Most people don't understand pure functional programming either. Does that mean we should introduce unrestricted side effects in Haskell? -- Lennart On Thu, Jan 15, 2009 at 4:22 PM, Thomas DuBuisson thomas.dubuis...@gmail.com wrote: On Thu, Jan 15, 2009 at 4:12 PM, Sittampalam, Ganesh ganesh.sittampa...@credit-suisse.com wrote: Lennart Augustsson wrote: I have replied on his blog, but I'll repeat the gist of it here. Why is there a fear of using existing terminology that is exact? Why do people want to invent new words when there are already existing ones with the exact meaning that you want? If I see Monoid I know what it is, if I didn't know I could just look on Wikipedia. If I see Appendable I can guess what it might be, but exactly what does it mean? I would suggest that having to look things up slows people down and might distract them from learning other, perhaps more useful, things about the language. Exactly. For example, the entry for monoid on Wikipedia starts: In abstract algebra, a branch of mathematics, a monoid is an algebraic structure with a single, associative binary operation and an identity element. I've had some set theory, but most programmers I know have not. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Type Family Relations
Thomas DuBuisson: Cafe, I am wondering if there is a way to enforce compile time checking of an axiom relating two separate type families. Mandatory contrived example: type family AddressOf h type family HeaderOf a -- I'm looking for something to the effect of: type axiom HeaderOf (AddressOf x) ~ x -- Valid: type instance AddressOf IPv4Header = IPv4 type instance HeaderOf IPv4 = IPv4Header -- Invalid type instance AddressOf AppHeader = AppAddress type instance HeaderOf AppAddress = [AppHeader] So this is a universally enforced type equivalence. The stipulation could be arbitrarily complex, checked at compile time, and must hold for all instances of either type family. Am I making this too hard? Is there already a solution I'm missing? There are no type-level invariants, like your type axiom, at the moment, although there is active work in this area http://www.cs.kuleuven.be/~toms/Research/papers/plpv2009_draft.pdf -- Type Invariants for Haskell, T. Schrijvers, L.-J. Guillemette, S. Monnier. Accepted at PLPV 2009. However, there is a simple solution to your problem. To enforce a side condition on the type instances of two separate families, you need to bundle the families as associated types into a class. Then, you can impose side conditions by way of super class constraints. In your example, that *should* work as follows -- GHC currently doesn't accept this, due to superclass equalities not being fully implemented, but we'll solve this in a second step: class (HeaderOf a ~ h, AddressOf h ~ a) = Protocol h a where type AddressOf h type HeaderOf a -- Valid: instance Protocol IPv4Header IPv4 where type AddressOf IPv4Header = IPv4 type HeaderOf IPv4 = IPv4Header -- Invalid instance Protocol AppHeader AppAddress where type AddressOf AppHeader = AppAddress type HeaderOf AppAddress = [AppHeader] Superclass equalities are currently only partially implemented and GHC rejects them for this reason. However, your application doesn't require the full power of superclass equalities and can be realised with normal type classes: class EQ a b instance EQ a a class (EQ (HeaderOf a) h, EQ (AddressOf h) a) = Protocol h a where type AddressOf h type HeaderOf a -- Valid: instance Protocol IPv4Header IPv4 where type AddressOf IPv4Header = IPv4 type HeaderOf IPv4 = IPv4Header -- Invalid instance Protocol AppHeader AppAddress where type AddressOf AppHeader = AppAddress type HeaderOf AppAddress = [AppHeader] With this definition, the invalid definition is rejected with the message /Users/chak/Code/haskell/main.hs:34:9: No instance for (EQ [AppHeader] AppHeader) arising from the superclasses of an instance declaration at /Users/chak/Code/haskell/main.hs:34:9-37 Possible fix: add an instance declaration for (EQ [AppHeader] AppHeader) In the instance declaration for `Protocol AppHeader AppAddress' Manuel ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Could FDs help usurp an ATs syntactic restriction?
Nicolas Frisby:
From the error below, I'm inferring that the RHS of the associated
type definition can only contain type variables from the instance
head, not the instance context. I didn't explicitly see this
restriction when reading the GHC/Type_families entry.
Could perhaps the a b - bn functional dependency of the TypeEq
class lift this restriction for bn? This isn't my ball park, but that
idea has my hopes up :).
haskell
{-# LANGUAGE TypeFamilies #-}
import TypeEq
-- Attempting to encapsulate TypeEq behind an associated type.
class EQ a b where
type BN a b
instance TypeEq a b bn = EQ a b where
type BN a b = bn
/haskell
results in an error
ghci
/tmp/Test.hs:9:16: Not in scope: type variable `bn'
Failed, modules loaded: none.
/ghci
GHC is right, you cannot use 'bn' in the definition of the type family
instance. I agree that the documentation needs to make this clearer.
Generally,
class EQ a b where
type BN a b
instance TypeEq a b bn = EQ a b where
type BN a b = bn
is really just syntactic sugar for
type family BN a b
class EQ a b
type instance BN a b = bn
instance TypeEq a b bn = EQ a b
where it is clear that 'bn' is not in scope in the rhs of the type
instance.
Unfortunately, you cannot wrap a type class constraint into a type
synonym family (independent of whether it is associated or not).
Incidentally, type equalities (which are part of the type family
implementation) enable a much more compact definition of the type
equality predicate:
data True; data False;
class EqTyP a b result
instance (result ~ True) = EqTyP a a result
instance (result ~ False) = EqTyP a b result
Manuel
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Go Haskell!
Claus Reinke: What do those folks working on parallel Haskell arrays think about the sequential Haskell array baseline performance? You won't like the answer. We are not happy with the existing array infrastructure and hence have our own. Roman recently extracted some of it as a standalone package: http://hackage.haskell.org/cgi-bin/hackage-scripts/package/vector In the longer run, we would like to factor our library into DPH- specific code and general-purpose array library that you can use independent of DPH. Manuel ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] ANNOUNCE: Salsa: A .NET Bridge for Haskell
Great! Thanks for putting the code out! Manuel ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Simplifying a IsFunction type class using type equality constraints
Corey O'Connor: I recently had a need to use the IsFunction typeclass described by Oleg here: http://okmij.org/ftp/Haskell/isFunction.lhs and am wondering if the use of the TypeCast class can be correctly replaced by a type equality constraint. The IsFunction and TypeCast classes were defined as: data HTrue data HFalse class IsFunction a b | a - b instance TypeCast f HTrue = IsFunction (x-y) f instance TypeCast f HFalse = IsFunction a f -- literally lifted from the HList library class TypeCast a b | a - b, b-a where typeCast :: a - b class TypeCast' t a b | t a - b, t b - a where typeCast' :: t- a-b class TypeCast'' t a b | t a - b, t b - a where typeCast'' :: t- a-b instance TypeCast' () a b = TypeCast a b where typeCast x = typeCast' () x instance TypeCast'' t a b = TypeCast' t a b where typeCast' = typeCast'' instance TypeCast'' () a a where typeCast'' _ x = x I found the use of TypeCast in the IsFunction could be replaced by a type family: class IsFunction a b | a - b instance (f ~ TTrue) = IsFunction (x-y) f instance (f ~ TFalse) = IsFunction a f Yes, that's a fine way of simplifying the definition. In fact, you should also be able to drop the functional dependency in the IsFunction class. Manuel ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Type family oddity
Claus Reinke wrote:
Btw, is there a list of common TF pitfalls somewhere? Some example
items so far seem to be:
1 'C a = TF a', where 'a' isn't determinable
2 'TF a' is not fully polymorphic
3 'TF a' is not a decomposable type constructor, it stands only
for itself, or for its result (in that way it is more like a defined
function application)
For 1/2, it is helpful to flatten type family applications:
- 'C a = TF a' becomes: '(C a,TF a~tfa) = tfa'
- 'TF a' becomes: 'TF a~tfa = tfa'
For 3, it is helpful to imagine the arity of type families being
marked
by braces, to distinguish type family parameters from any
constructor parameters, in case the type family reduces to a type
constructor:
- Given 'type family TF2 a :: * - *','TF2 a b' becomes: '{TF2
a} ~ tfa = tfa b'
It should rather be a type-level programming FAQ:
Re 1: Ambiguous signatures are a general problem. However, they are
syntactically harder to recognise with TFs.
Re 2: Applies to GADTs as well.
Re 3: I have always been wondering whether we want special syntax for
the application of synonym families. That would make it syntactically
easier to recognise ambiguous signatures and indicarte syntactically
were decomposition is admisible.
BTW, part of the problem is that H98 is not entirely consistent with
its use of upper and lower case identifiers. Strictly speaking,
already vanilla type synonyms should have been lower case as they are
a simple form of functions on types (you cannot use decomposition on
them!) Then, synonym families could be lower-case, too.
Manuel
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Type family oddity
Florian Weimer: I can't figure out why the following code doesn't compile with the October 2n GHC 6.10 beta (-XTypeFamilies -XFlexibleContexts) when the type declaration is not commented out. It's a bug that the code is accepted *without* the signature, as the signature is ambiguous: http://hackage.haskell.org/trac/ghc/ticket/1897 This is not because the code fails to be type-safe, but because (a) you can't use the function erase_range anyway and (b) that it is accepted without a signature, but not with the signature leads to confusion, as you experienced. BTW, the method 'erase' in your code has the same problem. Manuel module T where type family RangeTrait c class InputRange r where remaining :: r - Bool advance :: r - r class (InputRange (RangeTrait s)) = Sequence s where erase :: RangeTrait s - IO (RangeTrait s) -- erase_range :: (Sequence s) = RangeTrait s - IO (RangeTrait s) erase_range r = if remaining r then do r' - erase r erase_range r' else return r GHCi says the type is precisely as specified in the comment. However, when I activate the type declaration, GHC complains: T.hs:16:22: Couldn't match expected type `RangeTrait s' against inferred type `RangeTrait s2' In the first argument of `erase', namely `r' In a stmt of a 'do' expression: r' - erase r In the expression: do r' - erase r erase_range r' T.hs:17:22: Couldn't match expected type `RangeTrait s1' against inferred type `RangeTrait s2' In the first argument of `erase_range', namely `r'' In the expression: erase_range r' In the expression: do r' - erase r erase_range r' Any suggestions? Is this a bug in GHC? ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Distributing Haskell binaries as OSX App Bundles
I wrote a command-line program recently for a friend in haskell. However, he's far away and not particularly computer literate. I sent him the raw binaries, but they came up with errors about not being able to find libgmp stuff. So then I thought I should probably be able to somehow distribute all the stuff together in a .app bundle. However, the only experience I have of doing this sort of stuff before is via xcode. What's the best way to go about this? It just occurred to me now that maybe cmake is the way to go? If you use the installer package version of GHC http://haskell.org/ghc/dist/6.8.3/chakravarty/GHC-6.8.3-i386.pkg GMP will automatically be linked statically. As far as creating app bundles, one way is to use xcode to to create the bundle structure and then have it call a conventional makefile based build system to do the actual build and install the binaries into the bundle structure. That's what I did to create the GHC.pkg. It might require some fiddling, though. Manuel ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] GHC trouble on Leopard
Miguel, I tried to compile some code on Mac Os X (Intel) Leopard. I have GHC 6.8.3 installed - the installer from GHC webpage (GHC-6.8.3-i386.pkg). But when I run make I get this error ghc-6.8.3: could not execute: /Library/Frameworks/GHC.framework/ Versions/608/usr/lib/ghc-6.8.3/ghc-asm This is not a common problem. I suspect that either your installation somehow got corrupt or you somehow changed your Perl installation. (The file in question is a Perl script.) Manuel ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Research language vs. professional language
Ryan Ingram: On Sun, Aug 31, 2008 at 7:27 PM, Jonathan Cast [EMAIL PROTECTED] wrote: This concept of `day-to-day work' is a curious one. Haskell is not a mature language, and probably shouldn't ever be one. I see where you are coming from here, but I think that train has already started and can't be stopped. I find Haskell interesting as a professional programmer for these four reasons: it's pure, it's functional, it's lazy, and it's got a great compiler. [..] There will always be new discoveries in purely functional programming, and as the art advances, features like this ad-hoc overloading hack (and ACIO) will become obsolete and have to be thrown over-board. This is a good point. However, it seems to me that the pure programming language research is moving towards dependently typed languages, and that progress in Haskell has been more application-side; transactional memory and data-parallel, along with research on various fusion techniques, for example. Let me quote from the Preface of the Haskell report: It was decided that a committee should be formed to design such a language, providing faster communication of new ideas, a stable foundation for real applications development, and a vehicle through which others would be encouraged to use functional languages. and It should be suitable for teaching, research, and applications, including building large systems. From the outset, the Haskell vision included being a stable foundation for real applications development (I read this as aiming at industrial use) and research. This leads to tension, but, for better or worse, I believe that the Haskell community -in its current form- is pretty much committed to meet both goals. You can see it in GHC. It implements the static Haskell 98 and at the same time many experimental, researchy features (which you use at your own risk). More generally, I think that this is one of the killer features of functional languages, they provide a fast path from innovative, even highly theoretical research to practical applications. This may not work forever -maybe all interesting research that can be done in Haskell without radical changes will have been done at some point- but for the moment, I think we are in pretty good shape. Manuel ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Haskell Xcode Plugin
Dennis Buchmann: during my search for an acceptable development environment under Mac OS X I found this Plugin for Xcode: http://hoovy.org/HaskellXcodePlugin/ Unfortunately, I'm not able to get it to run in Xcode v3.0 and the developer seems to be not contactable at the moment. So, has anyone installed this plugin successfully (with problems in the beginning)? I have a student working on a plugin for Xcode 3.0. Hopefully, he'll be able to release something in about two month. Manuel ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] xmonad on the openmoko mobile phone
Don Stewart: Haskell fans might be impressed by the good work of Joachim Breitner, who got xmonad running on his openmoko phone, http://www.joachim-breitner.de/blog/archives/300-Xmonad-on-my-mobile-phone.html You can see a photo here, http://galois.com/~dons/images/openmoko-nomeata.jpg Yay! Haskell on the iphone next? The iPhone SDK includes a version of gcc to generate code for the iPhone. Be cool if anybody try to use that with GHC. Manuel ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Building NDP with latest GHC
Austin Seipp: After my last issue with GHC's HEAD, I tried checking it out again and getting the patches for the libraries and lo and behold, it worked. So now I'm up to date with the latest libraries and the compiler, but it appears that building NDP itself is proving to be troublesome. The NDP libraries are in a state of complete upheaval. Instead of the one package ndp, there will be a set of dph packages with different backends to choose from (initially, there will be two backends, one for sequential code and one for multicore parallel code). If I'm just doing everything wrong, I'd really appreciate knowing and I'd be *more* than happy to update the wiki pages so that more people can try it and have it build successfuly, because as it stands I'm coming to the conclusion that basically all the information in [1] is just old and flat-out wrong, and I'm completely of ideas on how to go about this. [..] [1] http://haskell.org/haskellwiki/Data_Parallel_Haskell/PackageNDP Due to the completely different new set up, there was no point in trying to track incremental changes on the wiki page. Once, the individual pieces fit together again, we'll update the documentation. Due to a sequence of problems with GHC's build system and its increasing Cabal'isation, the library re-arrangement has taken much longer than originally anticipated. Sorry about that. Manuel ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Type families versus functional dependencies question
Alexey Rodriguez: On Fri, Jul 4, 2008 at 5:03 AM, Manuel M T Chakravarty [EMAIL PROTECTED] wrote: The problem is that blah's type is ambiguous, as f does only occur as an argument to the type family. If you'd define class Blah f a where blah :: a - f - T f f a (and change the rest of the program accordingly) then all will be fine. See this thread for a more in-depth discussion of the problem: http://www.haskell.org/pipermail/haskell-cafe/2008-April/041385.html Yes, I was afraid that this was the case. However, the question remains on whether my functional dependencies encoding is correct. A correct encoding would help me understand this typing problem a bit more. Especially, now that Claus showed that adding an equality constraint makes this program work! For this particular program, you could argue that the signature is not ambiguous as T is unary; hence, in (T f f a) only the (T f) is really a type family application and so the second occurrence of 'f' should make the signature unambiguous. This is the reason why Claus' encoding works and why your FD translation works. I will have a look at whether I can improve the implementation in GHC to be smarter about handling such higher kinded TFs. Thanks for the example program! Manuel ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Type families versus functional dependencies question
Alexey Rodriguez: We are having trouble with the following program that uses type families: class Blah f a where blah :: a - T f f a class A f where type T f :: (* - *) - * - * the following function does not type: wrapper :: forall a f . Blah f a = a - T f f a wrapper x = blah x GHC gives the error: Couldn't match expected type `T f1 f1 a' against inferred type `T f f a' In the expression: blah x In the definition of `wrapper': wrapper x = blah x Maybe it is a problem with ambiguous types, namely f appears only in applications of T. But that is not the case, there is a naked f appearing as the argument of T f. But perhaps the type checker does not want to unify those two f's precisely because they are the arguments of T f. The problem is that blah's type is ambiguous, as f does only occur as an argument to the type family. If you'd define class Blah f a where blah :: a - f - T f f a (and change the rest of the program accordingly) then all will be fine. See this thread for a more in-depth discussion of the problem: http://www.haskell.org/pipermail/haskell-cafe/2008-April/041385.html Manuel ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] type-level integers using type families
Peter Gavin: Has anyone else tried implementing type-level integers using type families? I tried using a couple of other type level arithmetic libraries (including type-level on Hackage) and they felt a bit clumsy to use. I started looking at type families and realized I could pretty much build an entire Scheme-like language based on them. In short, I've got addition, subtraction, multiplication working after just a days worth of hacking. I'm going to post the darcs archive sometime, sooner if anyone's interested. I really like the type-families based approach to this, it's a lot easier to understand, and you can think about things functionally instead of relationally. (Switching back and forth between Prolog- ish thinking and Haskell gets old quick.) Plus you can do type arithmetic directly in place, instead of using type classes everywhere. I am glad to hear that type families work for you. One thing that I'd like to be able to do is lazy unification on type instances, so that things like data True data False type family Cond x y z type instance Cond True y z = y type instance Cond False y z = z will work if the non-taken branch can't be unified with anything. Is this planned? Is it even feasible? I don't think i entirely understand the question. Do you mean that from an equality like Cond b Int Bool ~ Int you want the type checker to infer that (b ~ True)? This is generally not correct reasoning as type families are open; ie, subsequent modules might add data Bogus type instance Bogus y z = Int and now there are two solutions to (Cond b Int Bool ~ Int). Manuel ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Type families and GADTs in 6.9
Dan, I've been playing around with type families off and on in 6.8, but, what with the implementation therein being reportedly incomplete, it's hard to know what I'm getting right and wrong, or what should work but doesn't and so on. So, I finally decided to take the plunge and install 6.9 (which, perhaps, isn't yet safe in that regard either, but, such is life :)). But, when I loaded up one of my programs, I got a type error. The subject is inductively defined tuples: [..] However, proj results in a type error: Occurs check: cannot construct the infinite type: t = Lookup (t ::: ts) fn In the pattern: v ::: vs In the definition of `proj': proj FZ (v ::: vs) = v Sorry, but looks like a bug in 6.9 to me. Could you add it to the GHC bug tracker? Thanks, Manuel ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] type families and type signatures
Lennart Augustsson: On Thu, Apr 10, 2008 at 4:20 AM, Manuel M T Chakravarty [EMAIL PROTECTED] wrote: the five signatures forall a. S a forall b. S b forall a b. S (a, b) Int S Int By alpha-convertible I mean the usual thing from lambda calculus, they are identical modulo the names of bound variables. So only the first two are alpha-convertible to each other. If you involve any kind of reduction the equivalence test is no longer trivial. All I'm asking for really, is to be able to paste in the type that was inferred as the signature, without the compiler complaining. I think a trivial, purely syntactic test, such as the one proposed, would generate at least as much puzzlement as the current situation does. It would mean, you could not have String in your signature if the inferred signature has [Char]. I don't think that this is a solution at all. Manuel ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] type families and type signatures
Lennart Augustsson:
In the current GHC there are even definitions that are perfecty
usable, that cannot be given the type signature that that was
inferred.
That's bad, I agree.
At work we have the warning for missing signatures enabled, and we
turn warnings into errors. We have to disbale this for certain
definitions, because you cannot give them a signature. I find that
broken.
Definitely. Can you give an example?
Manuel
On Thu, Apr 10, 2008 at 5:52 AM, Manuel M T Chakravarty [EMAIL PROTECTED]
wrote:
Lennart Augustsson:
Let's look at this example from a higher level.
Haskell is a language which allows you to write type signatures for
functions, and even encourages you to do it.
Sometimes you even have to do it. Any language feature that stops
me from writing a type signature is in my opinion broken.
TFs as implemented in currently implemented ghc stops me from
writing type signatures. They are thus, in my opinion, broken.
The problem of ambiguity is not at all restricted to TFs. In fact,
you need neither TFs nor FDs to get the exact same behaviour. You
don't even need MPTCs:
{-# LANGUAGE FlexibleContexts #-}
module Ambiguity where
class C a
bar :: C (a, b) = b - b
bar = id
bar' :: C (a, b) = b - b
bar' = bar
This gives us
/Users/chak/Code/haskell/Ambiguity.hs:10:7:
Could not deduce (C (a, b)) from the context (C (a1, b))
arising from a use of `bar'
at /Users/chak/Code/haskell/Ambiguity.hs:10:7-9
Possible fix:
add (C (a, b)) to the context of the type signature for `bar''
or add an instance declaration for (C (a, b))
In the expression: bar
In the definition of `bar'': bar' = bar
So, we have this problem as soon as we have flexible contexts and/or
MPTCs, independent of TFs and FDs.
Manuel
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] type families and type signatures
Lennart Augustsson: On Thu, Apr 10, 2008 at 4:20 AM, Manuel M T Chakravarty [EMAIL PROTECTED] wrote: Lennart Augustsson: On Wed, Apr 9, 2008 at 8:53 AM, Martin Sulzmann [EMAIL PROTECTED] wrote: Lennart, you said (It's also pretty easy to fix the problem.) What do you mean? Easy to fix the type checker, or easy to fix the program by inserting annotations to guide the type checker? Martin I'm referring to the situation where the type inferred by the type checker is illegal for me to put into the program. In our example we can fix this in two ways, by making foo' illegal even when it has no signature, or making foo' legal even when it has a signature. To make it illegal: If foo' has no type signature, infer a type for foo', insert this type as a signature and type check again. If this fails, foo' is illegal. That would be possible, but it means we have to do this for all bindings in a program (also all lets bindings etc). Of course, but I'd rather the compiler did it than I. It's not that hard, btw. If the whole module type checks, insert all signatures and type check again. Sure. I did not argue against this. I think it would be a reasonable way forward. Manuel ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] type families and type signatures
Claus Reinke: type family Id a type instance Id Int = Int foo :: Id a - Id a foo = id n foo' :: Id a - Id a foo' = foo type function notation is slightly misleading, as it presents qualified polymorphic types in a form usually reserved for unqualified polymorphic types. rewriting foo's type helped me to see the ambiguity that others have pointed out: foo :: r ~ Id a = r - r there's nowhere to get the 'a' from. so unless 'Id' itself is fully polymorphic in 'a' (Id a = a, Id a = Int, ..), 'foo' can't really be used. for each type variable, there needs to be at least one position where it is not used as a type family parameter. Yes. It is generally so that the introduction of indexed types (ie, all of GADTs, data type families, or synonym families) means that a type with a parameter is not necessarily parametric. it might be useful to issue an ambiguity warning for such types? The problem is that testing for ambiguity is, in general, difficult. Whether a context is ambiguous depends for example on the currently visible class instances. As a result, a signature that is ambiguous in a module M, may be fine in a module N that imports M. However, I think what should be easier is to improve the error messages given when a function with an ambiguous signature is used. For example, if the error message in the definition of foo' would have included a hint saying that the definition is illegal because its right hand side contains the use of a function with an ambiguous signature, then Ganesh may have had an easier time seeing what's happening. ps. i find these examples and discussions helpful, if often initially puzzling - they help to clear up weak spots in the practice of type family use, understanding, and implementation, thereby improving all while making families more familiar!-) Absolutely! Manuel ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] type families and type signatures
Lennart Augustsson: On Wed, Apr 9, 2008 at 8:53 AM, Martin Sulzmann [EMAIL PROTECTED] wrote: Lennart, you said (It's also pretty easy to fix the problem.) What do you mean? Easy to fix the type checker, or easy to fix the program by inserting annotations to guide the type checker? Martin I'm referring to the situation where the type inferred by the type checker is illegal for me to put into the program. In our example we can fix this in two ways, by making foo' illegal even when it has no signature, or making foo' legal even when it has a signature. To make it illegal: If foo' has no type signature, infer a type for foo', insert this type as a signature and type check again. If this fails, foo' is illegal. That would be possible, but it means we have to do this for all bindings in a program (also all lets bindings etc). To make it legal: If foo' with a type signature doesn't type check, try to infer a type without a signature. If this succeeds then check that the type that was inferred is alpha-convertible to the original signature. If it is, accept foo'; the signature doesn't add any information. This harder, if not impossible. What does it mean for two signatures to be alpha-convertible? I assume, you intend that given type S a = Int the five signatures forall a. S a forall b. S b forall a b. S (a, b) Int S Int are all the alpha-convertible. Now, given type family F a b type instance F Int c = Int what about forall a. F a Int forall a. F Int Int forall a. F Int a forall a b. (a ~ Int) = F a b and so on So, I guess, you don't really mean alpha-convertible in its original syntactic sense. We should accept the definition if the inferred and the given signature are in some sense equivalent. For this equivalence to be robust, I am sure we need to define it as follows, where = is standard type subsumption: t1 equivalent t2 iff t1 = t2 and t2 = t1 However, the fact that we cannot decide type subsumption for ambiguous types is exactly what led us to the original problem. So, nothing has been won. Summary ~~~ Trying to make those definitions that are currently only legal *without* a signature also legal when the inferred signature is added (foo' in Ganesh's example) doesn't seem workable. However, to generally reject the same definitions, even if they are presented without a signature, seems workable. It does require the compiler to compute type annotations, and then, check that it can still accept the annotated program. This makes the process of type checking together with annotating the checked program idempotent, which is nice. Manuel ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: type families and type signatures
apfelmus: Manuel M T Chakravarty wrote: apfelmus: Manuel M T Chakravarty wrote: Let's alpha-rename the signatures and use explicit foralls for clarity: foo :: forall a. Id a - Id a foo' :: forall b. Id b - Id b GHC will try to match (Id a) against (Id b). As Id is a type synonym family, it would *not* be valid to derive (a ~ b) from this. After all, Id could have the same result for different argument types. (That's not the case for your one instance, but maybe in another module, there are additional instances for Id, where that is the case.) While in general (Id a ~ Id b) -/- (a ~ b) , parametricity makes it true in the case of foo . For instance, let Id a ~ Int . Then, the signature specializes to foo :: Int - Int . But due to parametricity, foo does not care at all what a is and will be the very same function for every a with Id a ~ Int . In other words, it's as if the type variable a is not in scope in the definition of foo . Be careful, Id is a type-indexed type family and *not* a parametric type. Parametricity does not apply. For more details about the situation with GADTs alone, see Foundations for Structured Programming with GADTs. Patricia Johann and Neil Ghani. Proceedings, Principles of Programming Languages 2008 (POPL'08). Yes and no. In the GADT case, a function like bar :: forall a . GADT a - String is clearly not parametric in a, in the sense that pattern matching on the GADT can specialize a which means that we have some form of pattern matching on the type a . The resulting String may depend on the type a . So, by parametricity, I mean type arguments may not be inspected. [..] However, I have this feeling that bar :: forall a . Id a - String with a type family Id *is* parametric in the sense that no matter what a is, the result always has to be the same. Intuitively, that's because we may not pattern match on the branch of a definition like type instance Id String = .. type instance Id Int= .. .. So, in the special case of foo and foo' , solving Id b ~ Id a by guessing a ~ b is safe since foo is parametric in a . We don't know that. We could have type instance Id [a] = GADT a Just looking at the signature, we don't know. Manuel ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] type families and type signatures
Lennart Augustsson:
Let's look at this example from a higher level.
Haskell is a language which allows you to write type signatures for
functions, and even encourages you to do it.
Sometimes you even have to do it. Any language feature that stops
me from writing a type signature is in my opinion broken.
TFs as implemented in currently implemented ghc stops me from
writing type signatures. They are thus, in my opinion, broken.
The problem of ambiguity is not at all restricted to TFs. In fact,
you need neither TFs nor FDs to get the exact same behaviour. You
don't even need MPTCs:
{-# LANGUAGE FlexibleContexts #-}
module Ambiguity where
class C a
bar :: C (a, b) = b - b
bar = id
bar' :: C (a, b) = b - b
bar' = bar
This gives us
/Users/chak/Code/haskell/Ambiguity.hs:10:7:
Could not deduce (C (a, b)) from the context (C (a1, b))
arising from a use of `bar'
at /Users/chak/Code/haskell/Ambiguity.hs:10:7-9
Possible fix:
add (C (a, b)) to the context of the type signature for `bar''
or add an instance declaration for (C (a, b))
In the expression: bar
In the definition of `bar'': bar' = bar
So, we have this problem as soon as we have flexible contexts and/or
MPTCs, independent of TFs and FDs.
Manuel
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] type families and type signatures
Ganesh Sittampalam: On Mon, 7 Apr 2008, Manuel M T Chakravarty wrote: Ganesh Sittampalam: The following program doesn't compile in latest GHC HEAD, although it does if I remove the signature on foo'. Is this expected? Yes, unfortunately, this is expected, although it is very unintuitive. This is for the following reason. Let's alpha-rename the signatures and use explicit foralls for clarity: foo :: forall a. Id a - Id a foo' :: forall b. Id b - Id b GHC will try to match (Id a) against (Id b). As Id is a type synonym family, it would *not* be valid to derive (a ~ b) from this. After all, Id could have the same result for different argument types. (That's not the case for your one instance, but maybe in another module, there are additional instances for Id, where that is the case.) Can't it derive (Id a ~ Id b), though? That's what it does derive as a proof obligation and finds it can't prove. The error message you are seeing is GHC's way of saying, I cannot assert that (Id a ~ Id b) holds. Now, as GHC cannot show that a and b are the same, it can also not show that (Id a) and (Id b) are the same. It does look odd when you use the same type variable in both signatures, especially as Haskell allows you to leave out the quantifiers, but the 'a' in the signature of foo and the 'a' in the signatures of foo' are not the same thing; they just happen to have the same name. Sure, but forall a . Id a ~ Id a is the same thing as forall b . Id b ~ Id b. Thanks for the explanation, anyway. I'll need to have another think about what I'm actually trying to do (which roughly speaking is to specialise a general function over type families using a signature which I think I need for other reasons). Generally speaking, is there any way to give a signature to foo'? Sorry, but in the heat of explaining what GHC does, I missed the probably crucial point. Your function foo is useless, as is foo'. Not only can't you rename foo (to foo'), but you generally can't use it. It's signature is ambiguous. Try evaluating (foo (1::Int)). The problem is related to the infamous (show . read). Manuel ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] type families and type signatures
Sittampalam, Ganesh: Manuel Chakravarty wrote: Ganesh Sittampalam: On Mon, 7 Apr 2008, Manuel M T Chakravarty wrote: Ganesh Sittampalam: The following program doesn't compile in latest GHC HEAD, although it does if I remove the signature on foo'. Is this expected? Yes, unfortunately, this is expected, although it is very unintuitive. This is for the following reason. Let's alpha-rename the signatures and use explicit foralls for clarity: foo :: forall a. Id a - Id a foo' :: forall b. Id b - Id b GHC will try to match (Id a) against (Id b). As Id is a type synonym family, it would *not* be valid to derive (a ~ b) from this. After all, Id could have the same result for different argument types. (That's not the case for your one instance, but maybe in another module, there are additional instances for Id, where that is the case.) Can't it derive (Id a ~ Id b), though? That's what it does derive as a proof obligation and finds it can't prove. The error message you are seeing is GHC's way of saying, I cannot assert that (Id a ~ Id b) holds. No, I meant can't it derive that equality when matching (Id a) against (Id b)? As you say, it can't derive (a ~ b) at that point, but (Id a ~ Id b) is known, surely? No, it is not know. Why do you think it is? Generally speaking, is there any way to give a signature to foo'? Sorry, but in the heat of explaining what GHC does, I missed the probably crucial point. Your function foo is useless, as is foo'. Not only can't you rename foo (to foo'), but you generally can't use it. It's signature is ambiguous. Try evaluating (foo (1::Int)). The problem is related to the infamous (show . read). My real code is somewhat analogous to (foo :: (Id Int - Id Int)) (1::Int). Isn't that unambiguous in the same way as (show.read) is if I give show or read a signature? No. The problem with a functions that has an ambiguous signature is that it contains type variables that are impossible to constrain by applying the function. Providing a type signature at the application site makes this no easier. Why? Consider what a type annotation means. By writing e :: t, you express your intent to use e at type t, but you also force the compiler to check that whatever type it derives for e is more general than t. It is this check for type subsumption that is the tricky bit when typing TFs (or FDs). See http://www.cse.unsw.edu.au/~chak/papers/SPCS08.html for more detail on why this is a hard problem. The problem with an ambiguous signature is that the subsumption check always fails, because the ambiguous signature contains some type variables for which the type checker cannot deduce a type instance. (You as a human reader may be able to *guess* an instance, but HM- based inference does generally not guess. It's a deterministic process.) The problem is really with foo and its signature, not with any use of foo. The function foo is (due to its type) unusable. Can't you change foo? Manuel ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] translating from fundeps into type families
Chaddaï Fouché: 2008/4/8, Manuel M T Chakravarty [EMAIL PROTECTED]: You need to write the instance as instance (b ~ TheFoo a, Foo a) = Bar (Either a b) where bar (Left a) = foo' a bar (Right b) = foo' (foo b :: a) If you do that, the program compile, but res still raise a panic in GHC6.8.2 . Before you sent your solution, I also tried to do class (TheFoo a ~ b) = Foo a b where ... instance (Foo a b) = Bar (Either a b) where ... But it didn't compile, it seems to me both versions should have the same behaviour ? 6.8.2 has many bugs concerning type families that have been removed in the development version of GHC. Manuel ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] translating from fundeps into type families
Ganesh Sittampalam: Can I have some advice on translating the attached Test1.hs into type families? My attempt at doing so is in Test1a.hs, but firstly it requires FlexibleInstances where Test1.hs didn't, and secondly it fails because it can't infer the instance for Bar (Either Int Int) whereas the fundeps version had no problems there. You need to write the instance as instance (b ~ TheFoo a, Foo a) = Bar (Either a b) where bar (Left a) = foo' a bar (Right b) = foo' (foo b :: a) Generally, you can't have type synonym families in instance heads. GHC should have complained about this despite your use of FlexibleInstances. (I'll fix that.) Unfortunately, the above will currently only go through if you specify UndecidableInstances. Nothing about it is undecidable, though, so the flag should not be required. Part of the trouble here is that, although we just completed a formal statement about the decidability of type checking for type families *without* taking context simplification into account http://www.cse.unsw.edu.au/~chak/papers/SPCS08.html , we are still lacking a formal statement about type checking for type families *with* context simplification. My conjecture at the moment is that equalities of the form tv ~ F tv1 .. tvn where tv and tvi are distinct type variables should always be fine in class instance contexts and correspond to what is permitted for FDs. (However, previous experience with FDs and TFs clearly shows that any statements about decidability and completeness in this space are to be regarded with caution until they have been formalised rigorously.) I'll create a trac ticket with your example. Cheers, Manuel ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: type families and type signatures
Hi Mark, I don't know if you have defined/studied corresponding notions of ambiguity/coherence in your framework. Instead, I was referring to what Manuel described as the equivalent problem using FDs: class IdC a b | a - b instance IdC Int Int bar :: IdC a b = b - b bar = id bar' :: IdC a b = b - b bar' = bar In this program, both bar and bar' have ambiguous types (the variable 'a' in each of the contexts is not uniquely determined by the variable 'b' appearing on the right), and so *neither* one of these definitions is valid. This behavior differs from what has been described for your approach, so perhaps Manuel's example isn't really equivalent after all. Technically, one could ignore the ambiguous type signature for bar, because the *principal* type of bar (as opposed to the *declared type*) is not ambiguous. However, in practice, there is little reason to allow the definition of a function with an ambiguous type because such functions cannot be used in practice: the ambiguity that is introduced in the type of bar will propagate to any other function that calls it, either directly or indirectly. For this reason, it makes sense to report the ambiguity at the point where bar is defined, instead of deferring that error to places where it is used, like the definition of bar'. (The latter is what I mean by delayed ambiguity checking.) You are of course spot on, but this is a difference in how GHC handles functional dependencies compared to Hugs. Hugs does reject bar as being ambiguous, but GHC does not! In other words, it also uses delayed ambiguity checking for the FD version, and so raises an error only when seeing bar'. The implementation of type families just mirrors GHC's behaviour for FDs. (This is why I presented the FD example, but I should have mentioned that the equivalence is restricted to GHC.) The rational for the decision to use delayed ambiguity checking in GHC is that it is, in general, not possible to spot and report all ambiguous signatures and *only* those. So, there are three possible choices: (1) Reject all signatures that *may* be ambiguous (and hence reject some perfectly good programs). (2) Reject all signatures that are *guaranteed* to be ambiguous (and accept some programs with functions that can never be applied). (3) Don't check for ambiguity (or delayed ambiguity checking). As you wrote, all three choices are perfectly safe - we will never accept a type-incorrect program, but they vary in terms of the range of accepted programs and quality of error messages. Please correct me if I am wrong, but as I understand the situation, Hugs uses Choice (1) and GHC uses Choice (3). As an example, consider this contrived program: class F a b | a - b where f1 :: a - b f2 :: b - a instance F Int Int where f1 = id f2 = id class G x a b where g :: x - a - b instance F a b = G Bool a b where g c v = f1 v instance F b a = G Int a b where g c v = f2 v foo1 :: (G Int a b) = a - a foo1 v = v foo2 :: (G Bool a b) = a - a foo2 v = v bar = foo2 (42::Int) Here foo1 is actually ambiguous, but foo2 is fine due to the FD in the instance context of the (G Bool a b) instance. GHC accepts this program (not checking for ambiguity) and allows you to evaluate bar. In contrast, Hugs rejects both the signature of foo1 and of foo2, arguably being overly restrictive with foo2. Cheers, Manuel ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: type families and type signatures
apfelmus: Manuel M T Chakravarty wrote: Ganesh Sittampalam: Let's alpha-rename the signatures and use explicit foralls for clarity: foo :: forall a. Id a - Id a foo' :: forall b. Id b - Id b GHC will try to match (Id a) against (Id b). As Id is a type synonym family, it would *not* be valid to derive (a ~ b) from this. After all, Id could have the same result for different argument types. (That's not the case for your one instance, but maybe in another module, there are additional instances for Id, where that is the case.) While in general (Id a ~ Id b) -/- (a ~ b) , parametricity makes it true in the case of foo . For instance, let Id a ~ Int . Then, the signature specializes to foo :: Int - Int . But due to parametricity, foo does not care at all what a is and will be the very same function for every a with Id a ~ Int . In other words, it's as if the type variable a is not in scope in the definition of foo . Be careful, Id is a type-indexed type family and *not* a parametric type. Parametricity does not apply. For more details about the situation with GADTs alone, see Foundations for Structured Programming with GADTs. Patricia Johann and Neil Ghani. Proceedings, Principles of Programming Languages 2008 (POPL'08). In full System F , neither definition would be a problem since the type a is an explicit parameter. You can't generally translate type family/GADT programs into System F. We proposed an extension of System F called System F_C(X); see our TLDI'07 paper: http://www.cse.unsw.edu.au/~chak/papers/SCPD07.html Manuel ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] type families and type signatures
Ganesh Sittampalam:
The following program doesn't compile in latest GHC HEAD, although
it does if I remove the signature on foo'. Is this expected?
Yes, unfortunately, this is expected, although it is very
unintuitive. This is for the following reason.
Let's alpha-rename the signatures and use explicit foralls for clarity:
foo :: forall a. Id a - Id a
foo' :: forall b. Id b - Id b
GHC will try to match (Id a) against (Id b). As Id is a type synonym
family, it would *not* be valid to derive (a ~ b) from this. After
all, Id could have the same result for different argument types.
(That's not the case for your one instance, but maybe in another
module, there are additional instances for Id, where that is the case.)
Now, as GHC cannot show that a and b are the same, it can also not
show that (Id a) and (Id b) are the same. It does look odd when you
use the same type variable in both signatures, especially as Haskell
allows you to leave out the quantifiers, but the 'a' in the signature
of foo and the 'a' in the signatures of foo' are not the same thing;
they just happen to have the same name.
BTW, here is the equivalent problem using FDs:
class IdC a b | a - b
instance IdC Int Int
bar :: IdC a b = b - b
bar = id
bar' :: IdC a b = b - b
bar' = bar
Given that this is a confusing issue, I am wondering whether we could
improve matters by giving a better error message, or an additional
hint in the message. Do you have any suggestion regarding what sort
of message might have helped you?
Manuel
{-# LANGUAGE TypeFamilies #-}
module Test7 where
type family Id a
type instance Id Int = Int
foo :: Id a - Id a
foo = id
foo' :: Id a - Id a
foo' = foo
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Equality constraints in type families
Hugo Pacheco: Yes, but doesn't the confluence problem only occur for type synonyms that ignore one or more of the parameters? If so, this could be checked... You can't check this easily (for the general case). Given type family G a b type FList a x = G a x type instance F [a] = FList a Does FList ignore its second argument? Depends on the type instances of G. Manuel On Fri, Mar 28, 2008 at 12:04 AM, Manuel M T Chakravarty [EMAIL PROTECTED] wrote: Hugo Pacheco: Sorry, I meant type FList a x = Either One (a,x) type instance F [a] = FList a We should not allow such programs. Manuel On Thu, Mar 27, 2008 at 4:45 PM, Hugo Pacheco [EMAIL PROTECTED] wrote: The current implementation is wrong, as it permits type S a b = a type family F a :: * - * type instance F a = S a Why do we need to forbid this type instance? Because it breaks the confluence of equality constraint normalisation. Here are two diverging normalisations: (1) F Int Bool ~ F Int Char == DECOMP F Int ~ F Int, Bool ~ Char == FAIL (2) F Int Bool ~ F Int Char == TOP S Int Bool ~ S Int Char == (expand type synonym) Int ~ Int == TRIVIAL This does mean that a program such as type FList a = Either One ((,) a) type instance F [a] = FList a will be disallowed in further versions? Doesn't this problem occur only for type synonyms that ignore one or more of the parameters? If so, this could be checked... hugo ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Functional dependencies with Type Classes
Henning Günther: suppose there are two (identical) classes: class Res a b | a - b where getRes :: a - b and class Res2 t where type Member t getRes2 :: t - Member t It is easy to automatically make every instance of Res2 an instance of res: instance Res2 a = Res a (Member a) where getRes x = getRes2 x However, declaring every instance of Res an instance of Res2 seems impossible, as the following doesn't compile instance Res a b = Res2 a where type Member a = b getRes2 x = getRes x Question is: How to do this? The reason I need it is because I use a library which uses functional dependencies, but my classes shall be type families. The last definition is invalid as the right-hand side of a type family instance can only depend on its parameters. However, in type Member a = b you pull 'b' out of thin air. Remember that associated types (ie, type families as part of classes) are only syntactic sugar for sparate type family and class declarations. Obviously, it would be imposible to pull the type instance out of the class in your definition. (The mismatch between FDs and TFs here really is due to FDs being tied to classes and TFs being separable - in that sense TFs are more general than FDs, and hence, you cannot always simulate TFs with FDs.) However, you can wrap an FD library into a TF interface with some additional effort. Using your example for illustration, define the type family and class separately: type family Member a class Res2 a where getRes2 :: a - Member a Then, implement the catch all class instance as follows: instance Res a (Member a) = Res2 a where getRes2 x = getRes x (This needs -fundecidable-instances. It is perfectly decidable if your FD class is, but GHC doesn't know that.) Now, the additional overhead is that you need to define the type family instances separately; ie, for every class instance of the FD class, such as instance Res Int Bool where getRes x = x == 0 you need to repeat the type mapping: type instance Member Int = Bool I hope this is not too much of a burden in your application. Manuel PS: Hmm, maybe this should go onto the wiki...___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Equality constraints in type families
Hugo Pacheco: Anyway, do you think it is feasible to have a flag such as -fallow- unsafe-type-families for users to use at their own risk? (supposing we know how to guarantee these constraints). Sorry, but it doesn't seem like a good idea to enable an unsound type system even by an explicit option. Manuel ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Equality constraints in type families
Hugo Pacheco: Sorry, I meant type FList a x = Either One (a,x) type instance F [a] = FList a We should not allow such programs. Manuel On Thu, Mar 27, 2008 at 4:45 PM, Hugo Pacheco [EMAIL PROTECTED] wrote: The current implementation is wrong, as it permits type S a b = a type family F a :: * - * type instance F a = S a Why do we need to forbid this type instance? Because it breaks the confluence of equality constraint normalisation. Here are two diverging normalisations: (1) F Int Bool ~ F Int Char == DECOMP F Int ~ F Int, Bool ~ Char == FAIL (2) F Int Bool ~ F Int Char == TOP S Int Bool ~ S Int Char == (expand type synonym) Int ~ Int == TRIVIAL This does mean that a program such as type FList a = Either One ((,) a) type instance F [a] = FList a will be disallowed in further versions? Doesn't this problem occur only for type synonyms that ignore one or more of the parameters? If so, this could be checked... hugo ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Equality constraints in type families
Hugo Pacheco: Since I was the one to start this thread, I have managed to implement what I initially wanted as F a :: *-* with F a x::*, and the cost of not having partially applied type synonyms was not much apart from some more equality coercions that I wasn't expecting. [..] Generally, I love type-indexed types. Glad to hear that! Manuel ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Equality constraints in type families
Simon Peyton-Jones: | * GHC says that these constraints must be obeyed only | *after* the programmer-written type has been normalised | by expanding saturated type synonyms | ... | I regard this as a kind of pre-pass, before serious type checking | takes place, so I don't think it should interact with type checking | at all. | | I don't think this normalisation should include type families, | although H98 type synonyms are a kind of degenerate case of type | families. | | Would that design resolve this particular issue? | | Not quite, but it refines my proposal of requiring that type synonyms | in the rhs of type instances need to be saturated. Let me elaborate. Why not quite? Maybe I was thinking too much in terms of GHC's implementation, but due to the lazy expansion type synonyms, the expansion is interleaved with all the rest of type checking. But I think I now know what you meant: the outcome should be *as if* type synonym expansion was done as a pre-pass. | So, the crucial point is that, as you wrote, | | I don't think this normalisation should include type families, | although H98 type synonyms are a kind of degenerate case of type | families. Exactly! Just to state it more clearly again: Any programmer-written type (i.e one forming part of the source text of the program) must obey the following rules: - well-kinded - type synonyms saturated - arguments of type applications are monotypes (but - is special) However these rules are checked ONLY AFTER EXPANDING SATURATE TYPE SYNONYMS (but doing no reduction on type families) I agree. The above checks are performed by checkValidType in TcMType. In particular, the check for saturated synonyms is in check_type (line 1134 or thereabouts). I'm not sure why these checks are not firing for the RHS of a type family declaration. Maybe we aren't calling checkValidType on it. I'll check that. Might be an oversight. So I think we are agreed. I think the above statement of validity should probably appear in the user manual. Yes, I'll take care of that. Manuel ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Equality constraints in type families
Manuel M T Chakravarty: again, i gave a concrete example of how ghc behaves as i would expect, not as that decomposition rule would suggest. Maybe you can explain why you think so. I didn't understand why you think the example is not following the decomposition rule. Actually, see http://hackage.haskell.org/trac/ghc/ticket/2157#comment:10 Manuel ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Equality constraints in type families
Simon Peyton-Jones: | | However, I think I now understand what you are worried about. It is the | | interaction of type families and GHC's generalised type synonyms (i.e., | | type synonyms that may be partially applied). I agree that it does lead | | to an odd interaction, because the outcome may depend on the order in | | which the type checker performs various operations. In particular, | | whether it first applies a type instance declaration to reduce a type | | family application or whether it first performs decomposition. | | yes, indeed, thanks! that was the central point of example one. Aha. Just to clarify, then, GHC's 'generalised type synonyms' behave like this. * H98 says that programmer-written types must obey certain constraints: - type synonym applications saturated - arguments of type applications are monotypes (apart from -) * GHC says that these constraints must be obeyed only *after* the programmer-written type has been normalised by expanding saturated type synonyms http://www.haskell.org/ghc/docs/latest/html/users_guide/data-type-extensions.html#type-synonyms I regard this as a kind of pre-pass, before serious type checking takes place, so I don't think it should interact with type checking at all. I don't think this normalisation should include type families, although H98 type synonyms are a kind of degenerate case of type families. Would that design resolve this particular issue? Not quite, but it refines my proposal of requiring that type synonyms in the rhs of type instances need to be saturated. Let me elaborate. The current implementation is wrong, as it permits type S a b = a type family F a :: * - * type instance F a = S a Why do we need to forbid this type instance? Because it breaks the confluence of equality constraint normalisation. Here are two diverging normalisations: (1) F Int Bool ~ F Int Char == DECOMP F Int ~ F Int, Bool ~ Char == FAIL (2) F Int Bool ~ F Int Char == TOP S Int Bool ~ S Int Char == (expand type synonym) Int ~ Int == TRIVIAL However, here is a (somewhat silly) program that does have partially applied type synonyms in a type instances' rhs and that is perfectly ok: type S a b = a type family F (a :: * - *) b :: * - * type instance F a b = S (S a) b b This is ok, because we can expand the type synonyms in the rhs of the type instance S (S a) b b = S a b = a and get a valid type. So, the crucial point is that, as you wrote, I don't think this normalisation should include type families, although H98 type synonyms are a kind of degenerate case of type families. The only way to stratify the normalisation of type synonyms and type families such that all type synonyms are expanded before any family applications are normalised is by requiring that after normalising the rhs of a type instance declaration *by itself*, we get a type that only contains saturated applications of type synonyms. (As Claus wrote, this is after all what we do for class instance heads.) Manuel ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Equality constraints in type families
Claus Reinke: one might say that the central point of example two were two partially applied type synonym families in the same position (rhs of a type synonym family instance definition). usually, when reduction meets typing, there is a subject reduction theorem, stating that types do not change during reduction. since, in this case, reduction and constraint generation happen at the same (type) level, the equivalent would be a proof of confluence, so that it doesn't matter which type rules are applied in which order (in this case, decomposition and reduction). Well, we still need normal subject reduction (i.e., types don't change under value term reduction), and we have established that for System FC (in the TLDI paper). In addition, type term normalisation (much like value term normalisation) needs to be confluent; otherwise, you won't get a complete type inference/checking algorithm. as far as i could determine, the TLDI paper does not deal with the full generality of ghc's type extensions, so it doesn't stumble over this issue, and might need elaboration. System FC as described in the paper is GHC's current Core language. What are you missing? | The most clean solution may indeed be to outlaw partial applications of | vanilla type synonyms in the rhes of type instances. (Which is what I | will implement unless anybody has a better idea.) i always dislike losing expressiveness, and ghc does almost seem to behave as i would expect in those examples, so perhaps there is a way to fit the partial applications into the theory of your TLDI paper. I don't think we can avoid losing that expressiveness, as you demonstrated that it leads to non-confluence of type term normalisation - see also my reply to SimonPJ's message in this thread. and i still don't like the decomposition rule, and i still don't even understand that first part about comparing partially applied type constructors!-) Haskell always had the decomposition rule. Maybe we confused the matter, by always showing a particular instance of the decomposition rule, rather than the general rule. Here it is in all it's glory: t1 t2 ~ t1' t2' == t1 ~ t1', t2 ~ t2' No mention of a type family. However, the rule obviously still needs to be correct if we allow any of the type terms (including t1 and t1') to include *saturated* applications of type families. Manuel ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Equality constraints in type families
Claus Reinke wrote,
given that type families are never meant to be partially applied,
perhaps a different notation, avoiding confusion
with type constructor applications in favour of something
resembling products, could make that clearer?
something simple, like braces to group families and indices:
type family {F a} :: * - *
{F x} y ~ {F u} v = {F x} ~ {F u} y ~ v
would avoid confusion about which parameters need
to be present (no partial application possible) and are
subject to family instance rules, and which parameters are subject
to the decomposition rule.
and David Menendez wrote,
erhaps type families could use a different kind constructor to
distinguish type indexes from type parameters.
Currently, Haskell kinds are generated by this grammar:
kind ::= * | kind - kind
We create a new production for family kinds,
fkind ::= kind | kind -| fkind
Now, we can easily distinguish F and G,
F :: * -| * - *
G :: * -| * -| *
The grammar allows higher-kinded indexes, like (* - *) -| *, but
requires all indexes to precede the regular parameters. (That is, you
can't abstract over a family.)
Yes, this is something that we thought about, too. In the System FC
paper, we subscript all type families with their arity to achieve a
weak form of this; ie, we'd write
F_1 Int Bool
to make clear that (F_1 Int) is a non-decomposable family application,
where the outermost application in ((F_1 Int) Bool) is decomposable.
The extra syntax has its advantages (more local information) and
disadvantages (more clutter). We weren't convinced that we need the
extra syntax, so left it out for the moment. However, this is
something that can always be changed if experience shows that programs
are easier to understand with extra syntax. It doesn't affect the
type theory and is really a pure language design question. I'd be
glad to hear some more opinions about this matter.
Manuel
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Equality constraints in type families
Dan Doel: On Tuesday 11 March 2008, Tom Schrijvers wrote: I think you've uncovered a bug in the type checker. We made the design choice that type functions with a higher-kinded result type must be injective with respect to the additional paramters. I.e. in your case: F x y ~ F u v = F x ~ F u /\ y ~ v So if we apply that to F d c ~ F a (c,a) we get: F d ~ F a /\ c ~ (c,a) where the latter clearly is an occurs-check error, i.e. there's no finite type c such that c = (c,a). So the error in the second version is justified. There should have been one in the latter, but the type checker failed to do the decomposition: a bug. While I think I understand why this is (due to the difference between index and non-index types), does this mean the following won't type check (it does in 6.8, but I gather its type family implementation wasn't exactly complete)? type family D a :: * type family E a :: * type instance D Int = Char type instance D Char = Int type instance E Char = Char type instance E Int = Int type family F a :: * - * type instance F Int = D type instance F Char = E foo :: F Int Int ~ F Char Char = a foo = undefined Clearly, both F Int Int ~ Char and F Char Char ~ Char, but neither Int ~ Char nor F Int ~ F Char. Then again, looking at that code, I guess it's an error to have D and E partially applied like that? Exactly. And one can't write, say: type instance F Int a = D a correct? I suppose that clears up situations where one might be able to construct a specific F X Y ~ F U V, but F X /~ F U \/ Y /~ V (at least, I can't thing of any others off the top of my head). Yes, this type instance is invalid. However, early version of the type family implementation erroneously accepted such instances. Manuel ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Equality constraints in type families
Claus Reinke: type family F a :: * - * F x y ~ F u v = F x ~ F u /\ y ~ v words, in a type term like (F Int Bool), the two parameters Int and Bool are treated differently. Int is treated like a parameter to a function (which is what you where expecting), whereas Bool is treated like a parameter to a vanilla data constructor (the part you did not expect). To highlight this distinction, we call only Int a type index. Generally, if a type family F has arity n, it's first n parameters are type indicies, the rest are treated like the parameters of any other type constructor. i'm not sure haskell offers the kind of distinction that we need to talk about this: 'data constructor' is value-level, 'type constructor' doesn't distinguish between type- vs data-defined type constructors. i think i know what you mean, but it confuses me that you use 'data constructor' (should be data/newtype-defined type constructor?) Yes, I meant to write data type constructor. and 'type constructor' (don't you want to exclude type-defined type constructors here). It may have been clearer if I had written data type constructor, but then the Haskell 98 report doesn't bother with that either (so I tend to be slack about it, too). data ConstD x y = ConstD x type ConstT x y = x 'ConstD x' and 'ConstT x' have the same kind, that of type constructors: * - *. but: ConstD x y1 ~ ConstD x y2 = y1 ~ y2 whereas forall y1, y2: ConstT x y1 ~ ConstT x y2 But note that ConstT x ~ ConstT x is malformed. and i thought 'type family' was meant to suggest type synonym families, in contrast to 'data family'? My nomenclature is as follows. The keywords 'type family' introduces a type synonym family and 'data family' introduces a data type family (or just data family). The term type family includes both. This follows Haskell's common use of type constructor, type synonym constructor, and data type constructor. you did notice that i gave an example of how ghc does not seem to follow that decomposition rule, didn't you? Yes, but I didn't see why you think GHC does the wrong thing. Manuel ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Equality constraints in type families
Claus Reinke: type family F a :: * - * F x y ~ F u v = F x ~ F u /\ y ~ v why would F x and F u have to be the same functions? shouldn't it be sufficient for them to have the same result, when applied to y and v, respectively? Oh, yes, that is sufficient and exactly what is meant by F x ~ F u. It means, the two can be unified modulo any type instances and local given equalities. sorry, i don't understand how that could be meant by 'F x ~ F u'; that equality doesn't even refer to any specific point on which these two need to be equal, so it can only be a point-free higher-order equality, can't it? the right-to-left implication is obvious, but the left-to-right implication seems to say that, for 'F x' and 'F u' to be equal on any concrete pair of types 'y' and 'u', they have to be equal on all possible types and 'y' and 'u' themselves have to be equal. You write 'y' and 'u'. Do you mean 'x' and 'u'? If so, why do you think the implication indicates that x and u need to be the same? again, i gave a concrete example of how ghc behaves as i would expect, not as that decomposition rule would suggest. Maybe you can explain why you think so. I didn't understand why you think the example is not following the decomposition rule. Manuel ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Equality constraints in type families
Claus Reinke: type family F a :: * - * .. We made the design choice that type functions with a higher-kinded result type must be injective with respect to the additional paramters. I.e. in your case: F x y ~ F u v = F x ~ F u /\ y ~ v i'm still trying to understand this remark: - if we are talking about type functions, i should be allowed to replace a function application with its result, and if that result doesn't mention some parameters, they shouldn't play a role at any stage, right? - if anything other than the function result matters, isn't it somewhat misleading to speak of type functions? You will notice that I avoid calling them type functions. In fact, the official term is type families. That is what they are called in the spec http://haskell.org/haskellwiki/GHC/Type_families and GHC's option is -XTypeFamilies, too. More precisely, they are type-indexed type families. One difference between type families and (value-level) functions is that not all parameters of a type family are treated the same. A type family has a fixed number of type indicies. We call the number of type indicies the type family's arity and by convention, the type indicies come always before other type parameters. In the example type family F a :: * - * F has arity 1, whereas type family G a b :: * has arity 2. So, the number of named parameters given is the arity. (The overall kind is still F :: * - * - *; ie, the arity is not obvious from the kind, which I am somewhat unhappy about.) In other words, in a type term like (F Int Bool), the two parameters Int and Bool are treated differently. Int is treated like a parameter to a function (which is what you where expecting), whereas Bool is treated like a parameter to a vanilla data constructor (the part you did not expect). To highlight this distinction, we call only Int a type index. Generally, if a type family F has arity n, it's first n parameters are type indicies, the rest are treated like the parameters of any other type constructor. Moreover, a type family of arity n, must always be applied to at least n parameters - ie, applications to type indicies cannot be partial. This is not just an arbitrary design decision, it is necessary to stay compatible with Haskell's existing notion of higher-kinded unification (see, Mark Jones' paper about constructor classes), while keeping the type system sound. To see why, consider that Haskell's higher-kinded type system, allows type terms, such as (c a), here c may be instantiated to be (F Int) or Maybe. This is only sound if F treats parameters beyond its arity like any other type constructor. A more formal discussion is in our TLDI paper about System F_C(X). Manuel ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Equality constraints in type families
Tom Schrijvers: could you please help me to clear up this confusion?-) Let me summarize :-) The current design for type functions with result kinds other than * (e.g. * - *) has not gotten very far yet. We are currently stabilizing the ordinary * type functions, and writing the story up. When that's done we can properly focus on this issue and consider different design choices. I don't quite agree. The current story was pretty much settled in the paper on associated type synonyms already and further clarified in the FC paper. Manuel ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Equality constraints in type families
Claus Reinke: type family F a :: * - * .. We made the design choice that type functions with a higher-kinded result type must be injective with respect to the additional paramters. I.e. in your case: F x y ~ F u v = F x ~ F u /\ y ~ v actually, i don't even understand the first part of that:-( why would F x and F u have to be the same functions? shouldn't it be sufficient for them to have the same result, when applied to y and v, respectively? Oh, yes, that is sufficient and exactly what is meant by F x ~ F u. It means, the two can be unified modulo any type instances and local given equalities. Manuel ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Type parameters in type families
Ryan Ingram: On 3/17/08, Hugo Pacheco [EMAIL PROTECTED] wrote: On the other side, it fails to compile when this signature is explicit: fff :: forall d x. (FunctorF d) = d - F d x - F d x fff a = fmapF a id Interestingly, this works when you also give a type signature to id: fff :: forall d x. (FunctorF d) = d - F d x - F d x fff a = fmapF a (id :: x - x) compiles for me (ghc6.8.2). There's probably a bug in the type checker; inference is working with no type signatures, but checking fails. The type checker is alright. It is an issue that we need to explain better in the documentation, though. As a simple example consider, class C a where type F a :: * foo :: F a The only occurrence of 'a' here is as an argument of the type family F. However, as discussed in this thread, decomposition does not hold for the type-indicies of a type family. In other words, from F a ~ F b, we can *not* deduce a ~ b. You have got the same situation for the 'x' in type type of fff. BTW, the same applies if you code the example with FDs. class C a ca | a - ca where foo :: ca which means, we have foo :: C a ca = ca Here 'a' only appears in the context and as 'a' appears on the lhs of the FD arrow, that leads to ambiguities. In summary, a type variable in a signature that appears *only* as part of type-indicies of type families leads to the same sort of ambiguities as a type variable that appears only in the context of a type signature. Manuel ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] problem with type equality constraints
Ganesh Sittampalam: On Mon, 17 Mar 2008, Manuel M T Chakravarty wrote: Your are completely right. Unfortunately, superclass equalities (ie, the Id a ~ ida in the class declaration of Foo) aren't fully implemented yet. OK, thanks. Is there any rough idea of when they will be? That's a bit difficult to say. The main problem is that the current handling of evidence for classes and access to superclass evidence doesn't mix well with the fact that the evidence for equalities are coercions (ie, type-level things, rather than value level things). It's high up on the list, but some other things like the interaction between GADTs and type families (basically done now) were higher up. If its important to you, I'd try to get to it earlier than if nobody is really waiting for it. Manuel ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] type families, fun deps, lattices imposed on/by types
Isto Aho:
Please, consider the example 03 of Understanding functional
dependencies
via Constraint Handling rules by Sulzmann, Duck, Peyton-Jones and
Stuckey.
There we are defining a multiplication over different numeric types:
class Mul a b c | a b - c where
(*) :: a - b - c
instance Mul Int Int Int where ...
instance Mul Int Float Float where ...
Ok, we could add
instance Mul Float Int Float where ...
but if we want to make everything work nicely together, Integer,
Complex,
Rational etc, there will be a lot of instances, especially if we
have to give
both Float Int and Int Float instances.
And now the question on lattices of types (didn't know any better
name
to refer to the following):
Is the following possible? Or can something similar achieved with
type families (easily)?
type lattice T a b
-- Each of the following gives a -relation between types,
-- upper gives a method, how we get the larger (2nd) from
-- the smaller (1st).
lattice instance T Int Integer where upper = fromIntegral
lattice instance T Int Float where upper = fromIntegral
lattice instance T Integer (Ratio Integer) where upper = ...
lattice instance T (Ratio Integer) Double where ...
lattice instance T Float Double ...
lattice instance T Double (Complex Double) ...
-- e.g. Now the compiler can check that the top type is
-- unique and that there is a path from every type to the top type.
-- If the compiler founds this not to be the case, an error is output.
-- But otherwise there can be types that are not comparable but
-- the common top is quaranteed to exist.
class Mul a b c where
lattice T
(*) :: a - b - c
(*) x y = (upper x y x) * (upper x y y)
-- Now there is no need for the instances like.
instance Mul Int Float Float where ...
instance Mul Float (Ratio Integer) Double where ...
In the definition, the upper function only has one argument...
The compiler can generate those instances, because we have given
the upper-methods. There is always the top available.
Function
(*) x y = (upper x y x) * (upper x y y)
might could be replaced with
(*) x y = x * y
because of the presence of lattice T and thus, the upper-function.
If this were possible, the benefits would be:
- No need to state Int Float and Float Int instances on cases
where the operands do commute.
- No need to write a large number of instances if you have several
types on lattice (e.g. some more or less well defined relation).
- If the relation between types is not clear, we could define another
lattice T2 to our Mul2 class for the other uses.
Continuing the idea: we could override the default instances generated
by the compiler with our own instances when needed.
Ok, so, is it possible to write something like that already? (I just
wouldn't like write a lot of instances...) If not, would it be
possible to extend, say ghc, to work that way or are there too much
inconsistencies in the above presentation?
Using your idea of separating the lattice and conversion from the
definition of multiplication, you can at least save yourself the class
instances:
{-# LANGUAGE TypeFamilies, MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleContexts, FlexibleInstances,
UndecidableInstances #-}
type family Join a b :: *
type instance Join Int Int = Int
type instance Join Float Float = Float
type instance Join Int Float = Float
type instance Join Float Int = Float
class Conv a b where
conv :: a - b
instance Conv Int Float where
conv = fromIntegral
instance Conv Int Int where
conv = id
instance Conv Float Float where
conv = id
class Mul a b where
mul :: a - b - Join a b
instance (Conv a (Join a b), Conv b (Join a b), Num (Join a b))
= Mul a b where
mul x y = conv x * conv y
You will have to write quite a lot of type instances of Join.
However, the rest of the code is as concise as you seem to want it.
You could even do better with Join by using more sophisticated type-
level data structures; i.e., you could define type-level association
lists and define Join as a type-level lookup function, including rules
for reflexivity and symmetry, on those lists. In other words, instead
of hard-coding the laws of lattices into the compiler, you'd just
programatically define them as part of your type-level program. This
is more flexible, as I am sure there are other applications, where we
don't want a lattice, but some other structure.
See also Andrew Appleyard's recent BSc thesis on how a similar
approach can be used to embed the type structure of a different
programming language in Haskell. In his case, this was the subtyping
relation of C#:
http://www.cse.unsw.edu.au/~pls/thesis/aja-thesis.pdf
Manuel
PS: The use of UndecidableInstances in the above code is a bit
unfortunate, but it is forced on us by the rather complicated instance
context of Mul (even if the above set of family and class instances is
of course perfectly
Re: [Haskell-cafe] problem with type equality constraints
Ganesh Sittampalam: When I try to compile this code with ghc-6.9.20080310: module Test2 where type family Id a type instance Id Int = Int type instance Id (a, b) = (Id a, Id b) class Id a ~ ida = Foo a ida instance Foo Int Int instance (Foo a ida, Foo b idb) = Foo (a, b) (ida, idb) I get these errors: Test2.hs:12:0: Couldn't match expected type `ida' against inferred type `Id a' `ida' is a rigid type variable bound by the instance declaration at Test2.hs:12:16 When checking the super-classes of an instance declaration In the instance declaration for `Foo (a, b) (ida, idb)' Test2.hs:12:0: Couldn't match expected type `idb' against inferred type `Id b' `idb' is a rigid type variable bound by the instance declaration at Test2.hs:12:27 When checking the super-classes of an instance declaration In the instance declaration for `Foo (a, b) (ida, idb)' It seems to me that since Foo a ida and Foo b idb are superclassess, Id a ~ ida and Id b ~ idb should be known and so this should have worked - am I missing something? Your are completely right. Unfortunately, superclass equalities (ie, the Id a ~ ida in the class declaration of Foo) aren't fully implemented yet. If I am not mistaken, superclass equalities, class defaults for associated type families, and GADT data instances are the three major features of type families/equality constraint saga that aren't fully implemented yet. Manuel ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Bug with GADT in function Patterns?
Hi Hugo,
I have found a bug on the compiler (at least ghc 6.8.2). For some
module (yes, the example does nothing at all):
module Test where
data Type a where
Func :: Type a - Type b - Type (a - b)
PF :: Type a - Type (PF a)
data PF a where
ID :: PF (a - a)
test :: Type a - a - a
test (PF (Func _ _)) ID = ID
I get the impossible:
$ ghci Test.hs -fglasgow-exts
GHCi, version 6.9.20080303: http://www.haskell.org/ghc/ :? for help
Loading package base ... linking ... done.
[1 of 1] Compiling Test ( Test.hs, interpreted )
ghc-6.9.20080303: panic! (the 'impossible' happened)
(GHC version 6.9.20080303 for i386-apple-darwin):
Coercion.splitCoercionKindOf
$co${tc aog} [tv]
predt_ao8{tv} [tau] ~ a{tv aob} [sk] - a{tv aob} [sk]
Please report this as a GHC bug: http://www.haskell.org/ghc/
reportabug
However, the following implementations of test compile ok:
test :: Type a - a - a
test (PF _) ID = ID
test :: Type a - a - a
test (PF (Func _ _)) x = x
It has something to do with mixing different GADTs contructors.
Should this be submitted as a bug as it is?
The implementation of type checking of GADTs was completely redone in
6.9. Could you please check whether you have the same problem with
the current version of 6.9 in the darcs repo. If yes, then please
submit it as a bug.
Thanks,
Manuel
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
