[Haskell] Call for Papers IFL 2013
=== VACANCY : 1x Phd Student in domain specific type error diagnosis for Haskell === The activities of the Software Systems division at Utrecht University include research on programming methodologies, compiler construction, and program analysis, validation, and verification. For information about the research group of Software Technology, see: http://www.cs.uu.nl/wiki/Center Financed by the Netherlands Organisation for Scientific Research (NWO), we currently have a job opening for: * 1x PhD researcher (Ph D student) Software Technology Domain-specific languages (DSLs) have the potential both to reduce the effort of programming, and to result in programs that are easier to understand and maintain. For various good reasons, researchers have proposed to embed DSLs (then called EDSLs) into a general purpose host language. An important disadvantage of such an embedding is that it is very hard to make type error diagnosis domain-aware, because inconsistencies are by default explained in terms of the host language. We are currently looking for a highly motivated Ph D student to investigate this problem in the context of the functional language Haskell. The basic approach is to scale the concept of specialized type rules as developed by (Heeren, Hage and Swierstra, ICFP '03, see link below) for Haskell '98 to modern day Haskell with all of its type system extensions. The work is both technically challenging, i.e., how do you ensure that modifications to the type diagnositic process do not inadvertently change the type system, and practically immediately useful: making domain-specific type error diagnosis a reality for a full sized language such as Haskell is likely to have a pervasive influence on the field of domain-specific languages, and the language Haskell. The ICFP '03 paper can be found at http://www.cs.uu.nl/people/jur/scriptingthetypeinferencer.pdf A project paper that describes the context and aims of the current project can be found here: http://www.cs.uu.nl/people/jur/tfp2013_submission_2.pdf At first, the work will be prototyped in our own Utrecht Haskell Compiler. If succesfull, the work will also make its way into the GHC. We expect the candidate to communicate the results academically, to present the work at scientific conferences, to supervise Master students, and to assist in teaching courses at Bachelor or Master level. - What we are looking for - The candidate should have an MSc in Computer Science, be highly motivated, speak and write English very well, and be proficient in producing scientific reports. Knowledge of and experience with at least one of the following two areas is essential: * functional programming, and Haskell in particular * type system concepts Furthermore, we expect the candidate to be able to reason formally. Experience in compiler construction is expected to be useful in this project. - What we offer - You are offered a full-time position for 4 years. The gross salary is in the range between Û 2083,- and maximum Û 2664,- per month. The salary is supplemented with a holiday bonus of 8% and an end-of-year bonus of 8,3% per year. In addition we offer: a pension scheme, a partially paid parental leave, flexible employment conditions. Conditions are based on the Collective Labour Agreement Dutch Universities. We aim to start November 1, 2013 at the latest, but preferably sooner. - In order to apply - To apply please attach a letter of motivation, a curriculum vitae, and (email) addresses of two referees. Make sure to also include a transcript of the courses you have followed (at bachelor and master level), with the grades you obtained, and to include a sample of your scientific writing, e.g., the pdf of your master thesis. It is possible to apply for this position if you are close to obtaining your Master's. In that case include a letter of your supervisor with an estimate of your progress, and do not forget to include at least a sample of your technical writing skills. Application closes on the 20th of June 2013. For application, visit http://www.cs.uu.nl/vacatures/en/583630.html and follow the link to the official job application page at the bottom. --- Contact person --- For further information you can direct your inquiries to: Dr. Jurriaan Hage Phone: (+31) 30 253 3283 e-mail: j.h...@uu.nl. website: http://www.cs.uu.nl/wiki/Hage/WebHome ___ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
[Haskell] Job opening Ph D student in type error diagnosis for domain specific languages in Haskell
Dear Haskellers, Apologies in case you have received multiple copies. best, Jur === VACANCY : 1x Phd Student in domain specific type error diagnosis for Haskell === The activities of the Software Systems division at Utrecht University include research on programming methodologies, compiler construction, and program analysis, validation, and verification. For information about the research group of Software Technology, see: http://www.cs.uu.nl/wiki/Center Financed by the Netherlands Organisation for Scientific Research (NWO), we currently have a job opening for: * 1x PhD researcher (Ph D student) Software Technology Domain-specific languages (DSLs) have the potential both to reduce the effort of programming, and to result in programs that are easier to understand and maintain. For various good reasons, researchers have proposed to embed DSLs (then called EDSLs) into a general purpose host language. An important disadvantage of such an embedding is that it is very hard to make type error diagnosis domain-aware, because inconsistencies are by default explained in terms of the host language. We are currently looking for a highly motivated Ph D student to investigate this problem in the context of the functional language Haskell. The basic approach is to scale the concept of specialized type rules as developed by (Heeren, Hage and Swierstra, ICFP '03, see link below) for Haskell '98 to modern day Haskell with all of its type system extensions. The work is both technically challenging, i.e., how do you ensure that modifications to the type diagnositic process do not inadvertently change the type system, and practically immediately useful: making domain-specific type error diagnosis a reality for a full sized language such as Haskell is likely to have a pervasive influence on the field of domain-specific languages, and the language Haskell. The ICFP '03 paper can be found at http://www.cs.uu.nl/people/jur/scriptingthetypeinferencer.pdf A project paper that describes the context and aims of the current project can be found here: http://www.cs.uu.nl/people/jur/tfp2013_submission_2.pdf At first, the work will be prototyped in our own Utrecht Haskell Compiler. If succesfull, the work will also make its way into the GHC. We expect the candidate to communicate the results academically, to present the work at scientific conferences, to supervise Master students, and to assist in teaching courses at Bachelor or Master level. - What we are looking for - The candidate should have an MSc in Computer Science, be highly motivated, speak and write English very well, and be proficient in producing scientific reports. Knowledge of and experience with at least one of the following two areas is essential: * functional programming, and Haskell in particular * type system concepts Furthermore, we expect the candidate to be able to reason formally. Experience in compiler construction is expected to be useful in this project. - What we offer - You are offered a full-time position for 4 years. The gross salary is in the range between € 2083,- and maximum € 2664,- per month. The salary is supplemented with a holiday bonus of 8% and an end-of-year bonus of 8,3% per year. In addition we offer: a pension scheme, a partially paid parental leave, flexible employment conditions. Conditions are based on the Collective Labour Agreement Dutch Universities. We aim to start November 1, 2013 at the latest, but preferably sooner. - In order to apply - To apply please attach a letter of motivation, a curriculum vitae, and (email) addresses of two referees. Make sure to also include a transcript of the courses you have followed (at bachelor and master level), with the grades you obtained, and to include a sample of your scientific writing, e.g., the pdf of your master thesis. It is possible to apply for this position if you are close to obtaining your Master's. In that case include a letter of your supervisor with an estimate of your progress, and do not forget to include at least a sample of your technical writing skills. Application closes on the 20th of June 2013. For application, visit http://www.cs.uu.nl/vacatures/en/583630.html and follow the link to the official job application page at the bottom. --- Contact person --- For further information you can direct your inquiries to: Dr. Jurriaan Hage Phone: (+31) 30 253 3283 e-mail: j.h...@uu.nl. website: http://www.cs.uu.nl/wiki/Hage/WebHome ___ Haskell mailing list Haskell@haskell.org
Re: [Haskell-cafe] mapFst and mapSnd
class BinaryFunctor f where bimap :: (a - c) - (b - d) - f a b - f c d mapFst = (`bimap id`) mapSnd = bimap id On 31/05/2013 12:16 PM, Shachaf Ben-Kiki shac...@gmail.com wrote: On Thu, May 30, 2013 at 7:12 PM, Shachaf Ben-Kiki shac...@gmail.com wrote: One generalization of them is to lenses. For example `lens` has both, _1, _2, such that mapPair = over both, mapFst = over _1, etc., but you can also get fst = view _1, set _2 = \y' (x,_) - (x,y'), and so on. (Since both refers to two elements, you end up with view both = \(x,y) - mappend x y.) The types you end up with are simple generalizations of mapFoo, with just an extra Functor or Applicative (think mapMFoo): both :: Applicative f = (a - f b) - (a,a) - f (b,b) both f (x,y) = (,) $ f x * g y _2 :: Functor f = (a - f b) - (e,a) - f (e,b) _2 f (x,y) = (,) x $ f y With an appropriate choice of f you can get many useful functions. I spoke too quickly -- your mapPair is something different. Indeed bimap (or (***), if you prefer base) is the place to find it -- lenses don't really fit here. My both is for mapping one function over both elements. Shachaf ___ 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] Projects using Shake
hi frerich, On May 31, 2013, at 2:17 AM, Frerich Raabe wrote: Is anybody aware of open source projects which I could look at, or is there maybe a conventional file extension for… what do you call them, Shakefiles? other than .hs which I could google for? we are using a shake-based build system for our mobile sound engine [1]; see the shakefile here [2] and associated modules [3]. the focus is on cross-compilation of static/shared libraries for mobile platforms (currently ios, android in the works) so it might not be what you're looking for. however, most of it is quite generic (if you're working with c, c++, objc, asm) and we're going to release it as a library as soon the features and the API have settled a bit. cheers, sk [1] http://methc.la [2] https://github.com/samplecount/methcla/blob/develop/engine/shakefile.hs [3] https://github.com/samplecount/methcla/tree/develop/engine/Shakefile ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Call for Papers IFL 2013
=== VACANCY : 1x Phd Student in domain specific type error diagnosis for Haskell === The activities of the Software Systems division at Utrecht University include research on programming methodologies, compiler construction, and program analysis, validation, and verification. For information about the research group of Software Technology, see: http://www.cs.uu.nl/wiki/Center Financed by the Netherlands Organisation for Scientific Research (NWO), we currently have a job opening for: * 1x PhD researcher (Ph D student) Software Technology Domain-specific languages (DSLs) have the potential both to reduce the effort of programming, and to result in programs that are easier to understand and maintain. For various good reasons, researchers have proposed to embed DSLs (then called EDSLs) into a general purpose host language. An important disadvantage of such an embedding is that it is very hard to make type error diagnosis domain-aware, because inconsistencies are by default explained in terms of the host language. We are currently looking for a highly motivated Ph D student to investigate this problem in the context of the functional language Haskell. The basic approach is to scale the concept of specialized type rules as developed by (Heeren, Hage and Swierstra, ICFP '03, see link below) for Haskell '98 to modern day Haskell with all of its type system extensions. The work is both technically challenging, i.e., how do you ensure that modifications to the type diagnositic process do not inadvertently change the type system, and practically immediately useful: making domain-specific type error diagnosis a reality for a full sized language such as Haskell is likely to have a pervasive influence on the field of domain-specific languages, and the language Haskell. The ICFP '03 paper can be found at http://www.cs.uu.nl/people/jur/scriptingthetypeinferencer.pdf A project paper that describes the context and aims of the current project can be found here: http://www.cs.uu.nl/people/jur/tfp2013_submission_2.pdf At first, the work will be prototyped in our own Utrecht Haskell Compiler. If succesfull, the work will also make its way into the GHC. We expect the candidate to communicate the results academically, to present the work at scientific conferences, to supervise Master students, and to assist in teaching courses at Bachelor or Master level. - What we are looking for - The candidate should have an MSc in Computer Science, be highly motivated, speak and write English very well, and be proficient in producing scientific reports. Knowledge of and experience with at least one of the following two areas is essential: * functional programming, and Haskell in particular * type system concepts Furthermore, we expect the candidate to be able to reason formally. Experience in compiler construction is expected to be useful in this project. - What we offer - You are offered a full-time position for 4 years. The gross salary is in the range between Û 2083,- and maximum Û 2664,- per month. The salary is supplemented with a holiday bonus of 8% and an end-of-year bonus of 8,3% per year. In addition we offer: a pension scheme, a partially paid parental leave, flexible employment conditions. Conditions are based on the Collective Labour Agreement Dutch Universities. We aim to start November 1, 2013 at the latest, but preferably sooner. - In order to apply - To apply please attach a letter of motivation, a curriculum vitae, and (email) addresses of two referees. Make sure to also include a transcript of the courses you have followed (at bachelor and master level), with the grades you obtained, and to include a sample of your scientific writing, e.g., the pdf of your master thesis. It is possible to apply for this position if you are close to obtaining your Master's. In that case include a letter of your supervisor with an estimate of your progress, and do not forget to include at least a sample of your technical writing skills. Application closes on the 20th of June 2013. For application, visit http://www.cs.uu.nl/vacatures/en/583630.html and follow the link to the official job application page at the bottom. --- Contact person --- For further information you can direct your inquiries to: Dr. Jurriaan Hage Phone: (+31) 30 253 3283 e-mail: j.h...@uu.nl. website: http://www.cs.uu.nl/wiki/Hage/WebHome ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Call for Papers IFL 2013
Well that's exciting! I really hope uu finds a student. This would be yet another one of Haskell's killer features. - Clark On Friday, May 31, 2013, wrote: === VACANCY : 1x Phd Student in domain specific type error diagnosis for Haskell === The activities of the Software Systems division at Utrecht University include research on programming methodologies, compiler construction, and program analysis, validation, and verification. For information about the research group of Software Technology, see: http://www.cs.uu.nl/wiki/Center Financed by the Netherlands Organisation for Scientific Research (NWO), we currently have a job opening for: * 1x PhD researcher (Ph D student) Software Technology Domain-specific languages (DSLs) have the potential both to reduce the effort of programming, and to result in programs that are easier to understand and maintain. For various good reasons, researchers have proposed to embed DSLs (then called EDSLs) into a general purpose host language. An important disadvantage of such an embedding is that it is very hard to make type error diagnosis domain-aware, because inconsistencies are by default explained in terms of the host language. We are currently looking for a highly motivated Ph D student to investigate this problem in the context of the functional language Haskell. The basic approach is to scale the concept of specialized type rules as developed by (Heeren, Hage and Swierstra, ICFP '03, see link below) for Haskell '98 to modern day Haskell with all of its type system extensions. The work is both technically challenging, i.e., how do you ensure that modifications to the type diagnositic process do not inadvertently change the type system, and practically immediately useful: making domain-specific type error diagnosis a reality for a full sized language such as Haskell is likely to have a pervasive influence on the field of domain-specific languages, and the language Haskell. The ICFP '03 paper can be found at http://www.cs.uu.nl/people/jur/scriptingthetypeinferencer.pdf A project paper that describes the context and aims of the current project can be found here: http://www.cs.uu.nl/people/jur/tfp2013_submission_2.pdf At first, the work will be prototyped in our own Utrecht Haskell Compiler. If succesfull, the work will also make its way into the GHC. We expect the candidate to communicate the results academically, to present the work at scientific conferences, to supervise Master students, and to assist in teaching courses at Bachelor or Master level. - What we are looking for - The candidate should have an MSc in Computer Science, be highly motivated, speak and write English very well, and be proficient in producing scientific reports. Knowledge of and experience with at least one of the following two areas is essential: * functional programming, and Haskell in particular * type system concepts Furthermore, we expect the candidate to be able to reason formally. Experience in compiler construction is expected to be useful in this project. - What we offer - You are offered a full-time position for 4 years. The gross salary is in the range between Û 2083,- and maximum Û 2664,- per month. The salary is supplemented with a holiday bonus of 8% and an end-of-year bonus of 8,3% per year. In addition we offer: a pension scheme, a partially paid parental leave, flexible employment conditions. Conditions are based on the Collective Labour Agreement Dutch Universities. We aim to start November 1, 2013 at the latest, but preferably sooner. - In order to apply - To apply please attach a letter of motivation, a curriculum vitae, and (email) addresses of two referees. Make sure to also include a transcript of the courses you have followed (at bachelor and master level), with the grades you obtained, and to include a sample of your scientific writing, e.g., the pdf of your master thesis. It is possible to apply for this position if you are close to obtaining your Master's. In that case include a letter of your supervisor with an estimate of your progress, and do not forget to include at least a sample of your technical writing skills. Application closes on the 20th of June 2013. For application, visit http://www.cs.uu.nl/vacatures/en/583630.html and follow the link to the official job application page at the bottom. --- Contact person --- For further information you can direct your inquiries to: Dr. Jurriaan Hage Phone: (+31) 30 253 3283 e-mail: j.h...@uu.nl javascript:;.
[Haskell-cafe] question about singletons
Hi all,
Following a discussion on Haskell Cafe some time ago (1), Roman C. wrote:
On the other hand, the type 'Succ 'Zero has kind 'Nat and doesn't have
any inhabitants — only types of kind * do.
Indeed, this is what seems to occur in the following example:
---
{-# LANGUAGE DataKinds #-}
data Nat = Zero | Succ Nat
deriving ( Show, Eq, Ord )
main = do
let one = undefined :: 'Succ 'Zero
print one
---
We obtain an error (ghc 7.6.2):
---
Kind mis-match
Expected kind `OpenKind', but `Succ Zero' has kind `Nat'
In an expression type signature: Succ Zero
In the expression: undefined :: Succ Zero
In an equation for `one': one = undefined :: Succ Zero
---
(note that the error is slightly different in the HEAD version of GHC (2)).
Is it related to the sentence As bottom is an inhabitant of every type
(though with some caveats concerning types of unboxed kind), bottoms can be
used wherever a value of that type would be. found at address (3)? Here we
have a non-* kind, such that bottom would not be an inhabitant of ('Succ
'Zero). Why is this so? This seems to be an assumed choice (4), but I would
like to understand the reason for this design, which makes necessary to use
singletons, as explained at (4).
Now, if I use a singleton to make my example work, I obtain an error when
trying to make the type (Sing a) an instance of Show:
---
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE StandaloneDeriving #-}
data Nat = Zero | Succ Nat
deriving ( Show, Eq, Ord )
data Sing :: a - *
deriving instance Show (Sing a)
main = do
let one = undefined :: Sing ('Succ 'Zero)
print one
---
The error is simply:
---
test_noinhabitant_corrected.hs: Void showsPrec
---
Why?
Thanks,
TP
References:
--
(1):
https://groups.google.com/forum/?fromgroups#!topic/haskell-cafe/AltmX5iCFi8
(2):
---
Expected a type, but ‛Succ Zero’ has kind ‛Nat’
In an expression type signature: Succ Zero
In the expression: undefined :: Succ Zero
In an equation for ‛one’: one = undefined :: Succ Zero
---
(3):
http://www.haskell.org/haskellwiki/Bottom
(4):
http://hackage.haskell.org/trac/ghc/wiki/TypeNats/Basics
Both numeric and symbol literal types are empty---they have no inhabitants.
However, they may be used as parameters to other type constructors, which
makes them useful.
A singleton type is simply a type that has only one interesting inhabitant.
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Two GHC-related GSoC Proposals
[I'll be the mentor for this GSoC project.] I used the MVar approach a while ago and so did Simon Marlow's original solution. Using MVars and Threads for this should scale well enough (1000s of modules) and be relatively straightforward. Error/exception handling could be a bit tricky, but you could use (or copy ideas from) the 'async' package to deal with that. / Thomas On 30 May 2013 18:51, Ryan Newton rrnew...@gmail.com wrote: What's the plan for what control / synchronization structures you'll use in part 2 of the plan to implement a parallel driver? Is the idea just to use an IO thread for each compile and block them on MVars when they encounter dependencies? Or you can use a pool of worker threads and a work queue, and only add modules to the work queue when all their dependencies are met (limits memory use)... many options for executing a task DAG. Fortunately the granularity is coarse. -Ryan On Sun, Apr 21, 2013 at 10:34 PM, Patrick Palka patr...@parcs.ath.cx wrote: Good points. I did not take into account whether proposal #2 may be worth it in light of -fllvm. I suppose that even if the LLVM codegen is able to perform similar optimizations, it would still be beneficial to implement proposal #2 as a core-to-core pass because the transformations it performs would expose new information to subsequent core-to-core passes. Also, Haskell has different overflow rules than C does (whose rules I assume LLVM's optimizations are modeled from): In Haskell, integer overflow is undefined for all integral types, whereas in C it's only undefined for signed integral types. This limits the number of optimizations a C-based optimizer can perform on unsigned arithmetic. I'm not sure how I would break up the parallel compilation proposal into multiple self-contained units of work. I can only think of two units: making GHC thread safe, and writing the new parallel compilation driver. Other incidental units may come up during development (e.g. parallel compilation might exacerbate #4012), but I still feel that three months of full time work is ample time to complete the project, especially with existing familiarity with the code base. Thanks for the feedback. On Sun, Apr 21, 2013 at 5:55 PM, Carter Schonwald carter.schonw...@gmail.com wrote: Hey Patrick, both are excellent ideas for work that would be really valuable for the community! (independent of whether or not they can be made into GSOC sided chunks ) --- I'm actually hoping to invest some time this summer investigating improving the numerics optimization story in ghc. This is in large part because I'm writing LOTs of numeric codes in haskell presently (hopefully on track to make some available to the community ). That said, its not entirely obvious (at least to me) what a tractable focused GSOC sized subset of the numerics optimization improvement would be, and that would have to also be a subset that has real performance impact and doesn't benefit from eg using -fllvm rather than -fasm . - For helping pave the way to better parallel builds, what are some self contained units of work on ghc (or related work on cabal) that might be tractable over a summer? If you can put together a clear roadmap of work chunks that are tractable over the course of the summer, I'd favor choosing that work, especially if you can give a clear outline of the plan per chunk and how to evaluate the success of each unit of work. basically: while both are high value projects, helping improve the parallel build tooling (whether in performance or correctness or both!) has a more obvious scope of community impact, and if you can layout a clear plan of work that GHC folks agree with and seems doable, i'd favor that project :) hope this feedback helps you sort out project ideas cheers -Carter On Sun, Apr 21, 2013 at 12:20 PM, Patrick Palka patr...@parcs.ath.cx wrote: Hi, I'm interested in participating in the GSoC by improving GHC with one of these two features: 1) Implement native support for compiling modules in parallel (see #910). This will involve making the compilation pipeline thread-safe, implementing the logic for building modules in parallel (with an emphasis on keeping compiler output deterministic), and lots of testing and benchmarking. Being able to seamlessly build modules in parallel will shorten the time it takes to recompile a project and will therefore improve the life of every GHC user. 2) Improve existing constant folding, strength reduction and peephole optimizations on arithmetic and logical expressions, and optionally implement a core-to-core pass for optimizing nested comparisons (relevant tickets include #2132,#5615,#4101). GHC currently performs some of these simplifications (via its BuiltinRule framework), but there is a lot of room for improvement. For instance, the core for this snippet is essentially identical to the Haskell source: foo ::
[Haskell-cafe] Performance difference between Linux and Windows?
I've been having a great deal of fun writing a program to solve this year's Code Jam Fair and Squareproblem in Haskell (and learning about Haskell in the process). Having gotten it to work, I've been optimizing it as best I can. I'm not quite in Captain Ahab mode, but before I let it go I would like to find out what's behind a difference I've seen compiling and running the program under Linux and under Windows 7. Profiling it under Linux (compiled with GHC 7.4.1), it had a total allocation of 165,375,112 bytes. I had an opportunity to compile and run on Windows 7, with GHC 7.4.2. I expected it to run faster, since the Windows computer had a 3.1 GHz i7 and my Linux computer has a 2.8 GHz AMD Propus, but what I didn't expect was that the total allocation on the Windows version was 88,438,372 bytes! Thinking it might be due to a compiler improvement, I upgraded my Linux computer to Ubuntu 13.04 so I could get a newer GHC, but it didn't make much difference: total allocation 163,248,688 bytes. So, I'm wondering: what is it about either the Windows implementation or GHC 7.4.2 in particular that would make a factor of two difference in memory allocation? Should anyone wish to compile the program, let me know the best way to make the source available and I will happily do so; I also use Twan van Laarhoven's semilattice search tree code available at http://twanvl.nl/blog/haskell/SemilatticeSearchTree. James Jones ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Job opening Ph D student in type error diagnosis for domain specific languages in Haskell
Dear Haskellers, Apologies in case you have received multiple copies. best, Jur === VACANCY : 1x Phd Student in domain specific type error diagnosis for Haskell === The activities of the Software Systems division at Utrecht University include research on programming methodologies, compiler construction, and program analysis, validation, and verification. For information about the research group of Software Technology, see: http://www.cs.uu.nl/wiki/Center Financed by the Netherlands Organisation for Scientific Research (NWO), we currently have a job opening for: * 1x PhD researcher (Ph D student) Software Technology Domain-specific languages (DSLs) have the potential both to reduce the effort of programming, and to result in programs that are easier to understand and maintain. For various good reasons, researchers have proposed to embed DSLs (then called EDSLs) into a general purpose host language. An important disadvantage of such an embedding is that it is very hard to make type error diagnosis domain-aware, because inconsistencies are by default explained in terms of the host language. We are currently looking for a highly motivated Ph D student to investigate this problem in the context of the functional language Haskell. The basic approach is to scale the concept of specialized type rules as developed by (Heeren, Hage and Swierstra, ICFP '03, see link below) for Haskell '98 to modern day Haskell with all of its type system extensions. The work is both technically challenging, i.e., how do you ensure that modifications to the type diagnositic process do not inadvertently change the type system, and practically immediately useful: making domain-specific type error diagnosis a reality for a full sized language such as Haskell is likely to have a pervasive influence on the field of domain-specific languages, and the language Haskell. The ICFP '03 paper can be found at http://www.cs.uu.nl/people/jur/scriptingthetypeinferencer.pdf A project paper that describes the context and aims of the current project can be found here: http://www.cs.uu.nl/people/jur/tfp2013_submission_2.pdf At first, the work will be prototyped in our own Utrecht Haskell Compiler. If succesfull, the work will also make its way into the GHC. We expect the candidate to communicate the results academically, to present the work at scientific conferences, to supervise Master students, and to assist in teaching courses at Bachelor or Master level. - What we are looking for - The candidate should have an MSc in Computer Science, be highly motivated, speak and write English very well, and be proficient in producing scientific reports. Knowledge of and experience with at least one of the following two areas is essential: * functional programming, and Haskell in particular * type system concepts Furthermore, we expect the candidate to be able to reason formally. Experience in compiler construction is expected to be useful in this project. - What we offer - You are offered a full-time position for 4 years. The gross salary is in the range between € 2083,- and maximum € 2664,- per month. The salary is supplemented with a holiday bonus of 8% and an end-of-year bonus of 8,3% per year. In addition we offer: a pension scheme, a partially paid parental leave, flexible employment conditions. Conditions are based on the Collective Labour Agreement Dutch Universities. We aim to start November 1, 2013 at the latest, but preferably sooner. - In order to apply - To apply please attach a letter of motivation, a curriculum vitae, and (email) addresses of two referees. Make sure to also include a transcript of the courses you have followed (at bachelor and master level), with the grades you obtained, and to include a sample of your scientific writing, e.g., the pdf of your master thesis. It is possible to apply for this position if you are close to obtaining your Master's. In that case include a letter of your supervisor with an estimate of your progress, and do not forget to include at least a sample of your technical writing skills. Application closes on the 20th of June 2013. For application, visit http://www.cs.uu.nl/vacatures/en/583630.html and follow the link to the official job application page at the bottom. --- Contact person --- For further information you can direct your inquiries to: Dr. Jurriaan Hage Phone: (+31) 30 253 3283 e-mail: j.h...@uu.nl. website: http://www.cs.uu.nl/wiki/Hage/WebHome ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org
Re: [Haskell-cafe] question about singletons
Hi TP,
You bring up a few interesting points in your email.
(A note to those who have visited this playground before: to keep things
sane, let's just pretend that the kind # doesn't exist. Of course, if you
don't know about kind #, then you're a step ahead of the rest of us! While
you're at it, forget about the kind `Constraint` also.)
* Types at kind other than * do not have any inhabitants -- in fact, some
people would hesitate to call type-like things at kind other than * types!
(Though, I will call these things types because there's just not another
good moniker. Type-level data? Type indices? Type constructors? All are
somehow lacking.) Let's start with a more familiar example: Maybe. To form
an inhabited type, we must apply Maybe to something. So, we can have values
of type (Maybe Int) and values of type (Maybe Bool), but not values of plain
old type (Maybe). That's because Maybe has kind (* - *), not kind *.
Another way to say this is what I said above: Maybe requires something
(something at kind *, specifically) to become a proper, inhabited type. And,
even though we say `undefined` exists at all types, that's a bit of a
simplification. `undefined` exists at all types _of kind *_. The full type
of `undefined` is `forall (a :: *). a`. Thus, we can't have `undefined` at
Maybe, because Maybe is not of kind *.
This argument extends directly to where we have types derived from promoted
data constructors. The type 'Zero has kind Nat, not *, so 'Zero is
uninhabitable, even by `undefined`.
(When I first wandered down this road, I was confused by this too. Part of
the confusion was somehow deciding that * had some vague association with *
as used on the command line -- a notation that could expand to something
else. This is totally, completely, and in every way False. In at least one
other programming language [Coq], what Haskell spells * is spelled `Type`.
[Well, almost.])
When I am programming with promoted data constructors, I often find the
following definition useful:
data Proxy a = P
With PolyKinds, the type constructor Proxy has kind `forall k. k - *`. So,
if we need to quickly make a value associated with the type 'Zero, we can
just use `Proxy 'Zero`. Because Proxy is kind-polymorphic, this works just
fine.
Why have the restriction that kinds other than * are uninhabited? Well, for
one, (-) would be a strange beast indeed if other types could be inhabited.
What would be the kind of (-)? I don't want to think about it. We also have
the nice maxim that every type that appears to the right of a :: must be of
kind *.
* Singletons are a useful mechanism for type-level programming. But, there
is more to singletons than just defining `Sing` as you have. Instead, you
should import the definitions from GHC.TypeLits, which comes with singleton
definitions for the built-in Nat and Symbol kinds. One drawback of the
built-in Nat and Symbol kinds is that they are not recursively defined; you
can't pattern-match on them. So, if you want your own Nat, you can define a
singleton like this:
data SNat :: Nat - * where
SZero :: SNat 'Zero
SSucc :: SNat n - SNat ('Succ n)
Now, you can have values that are tightly associated with types. Yay!
* Why did you get that error with `show`? Because the `Sing` type you
defined is uninhabited -- not because it has a funny kind, but because it
has no constructors. So, when a `Show` instance is derived, the `show`
method just fails -- GHC knows `show` at type `Sing` cannot be called
because there are no `Sing`s. Then, when you subvert this logic by using
`undefined`, the derived `show` method doesn't quite know what to do with
itself.
I hope this helps! I do have to say I'm impressed, TP, by your intrepid
path of discovery down this road. You're asking all the right questions!
Richard
-Original Message-
From: haskell-cafe-boun...@haskell.org
[mailto:haskell-cafe-boun...@haskell.org] On Behalf Of TP
Sent: 31 May 2013 13:58
To: haskell-cafe@haskell.org
Subject: [Haskell-cafe] question about singletons
Hi all,
Following a discussion on Haskell Cafe some time ago (1), Roman C. wrote:
On the other hand, the type 'Succ 'Zero has kind 'Nat and doesn't have any
inhabitants — only types of kind * do.
Indeed, this is what seems to occur in the following example:
---
{-# LANGUAGE DataKinds #-}
data Nat = Zero | Succ Nat
deriving ( Show, Eq, Ord )
main = do
let one = undefined :: 'Succ 'Zero
print one
---
We obtain an error (ghc 7.6.2):
---
Kind mis-match
Expected kind `OpenKind', but `Succ Zero' has kind `Nat'
In an expression type signature: Succ Zero
In the expression: undefined :: Succ Zero
In an equation for `one': one = undefined :: Succ Zero
---
(note that the error is slightly different in the HEAD version of GHC (2)).
Is it related to the sentence As bottom is an inhabitant of every type
(though with some caveats concerning types of
Re: [Haskell-cafe] Performance difference between Linux and Windows?
The difference is roughly 2x, which suggests difference in Int/pointer sizes: 32bit vs 64bit. Indeed, only since 7.6.1. GHC supports compiling 64 bit executables on Windows ( http://hackage.haskell.org/trac/ghc/wiki/WindowsGhc). That means that in fact you compare 32 bit vs 64 bit programs. I didn't have a look at the code so this is just a wild guess. Best regards, Krzysztof Skrzętnicki On Fri, May 31, 2013 at 3:26 PM, James Jones jejones3...@gmail.com wrote: I've been having a great deal of fun writing a program to solve this year's Code Jam Fair and Squareproblem in Haskell (and learning about Haskell in the process). Having gotten it to work, I've been optimizing it as best I can. I'm not quite in Captain Ahab mode, but before I let it go I would like to find out what's behind a difference I've seen compiling and running the program under Linux and under Windows 7. Profiling it under Linux (compiled with GHC 7.4.1), it had a total allocation of 165,375,112 bytes. I had an opportunity to compile and run on Windows 7, with GHC 7.4.2. I expected it to run faster, since the Windows computer had a 3.1 GHz i7 and my Linux computer has a 2.8 GHz AMD Propus, but what I didn't expect was that the total allocation on the Windows version was 88,438,372 bytes! Thinking it might be due to a compiler improvement, I upgraded my Linux computer to Ubuntu 13.04 so I could get a newer GHC, but it didn't make much difference: total allocation 163,248,688 bytes. So, I'm wondering: what is it about either the Windows implementation or GHC 7.4.2 in particular that would make a factor of two difference in memory allocation? Should anyone wish to compile the program, let me know the best way to make the source available and I will happily do so; I also use Twan van Laarhoven's semilattice search tree code available at http://twanvl.nl/blog/haskell/SemilatticeSearchTree. James Jones ___ 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] lifted-base linking failure with GHC HEAD
-BEGIN PGP SIGNED MESSAGE- Hash: SHA1 Greetings, I'm attempting to build lifted-base (as a dependency for ghc-mod) but cabal-install fails every time during the linking phase. I pasted the full log of `cabal install lifted-base --verbose' to hpaste at [1]. I'm attempting to build it with GHC HEAD. Now, I should note that I have different directories for each ghc version in my ~. So, for ghc 7.6.3 I would have ~/ghc-7.6.3 with appropriate bin, lib etc. in there. I thought that might have made `ld' confused but I just tried to `cabal install lifted-base' with 7.6.3 and it succeeded. Any ideas about what might be wrong? [1] - http://hpaste.org/89046 - -- Mateusz K. -BEGIN PGP SIGNATURE- Version: GnuPG v2.0.19 (GNU/Linux) iQIcBAEBAgAGBQJRqTOjAAoJEM1mucMq2pqXt+QQALM9oWexq5NrWwOmcIj+m+08 DdNpj37KYx+M+3SUZYQ7RVyW7pf7ounsl/1OtGGndhGBeBpeamOMeZxaYvIZr7da IUjd3Vgnl0W44G+T9Wg64g+MIgyy75oLFPNnP0BGbcLzDk5wVgAl/xl+H193lLmu LbBJGAzAE+YHIx1mM+mNGsYgr80dhpGTs5jGdauAEdsnZFdFGj86sxBeFBeKVF78 md0PA1HDwJSVo2FyAAULWhgPDpwBrScjNjTU2etMpegMto1aDaV7rwvJeNeewv15 89o19tpWTvdwxtddOI6YlBKFTL0u80IBlCRQ+NWwu7PB35wR67MbOchXx4qGJSOt TxNelfW+C3h0BW7KLskQjqcEPUKD1hYB5lAnOH2VOaTSFEN9QN66GhC3BHLJCBiu UWZBRyUikAsjRvWL6eQI+vc8fnPSieNa5K2jdPe410uHojr7Eq28WCCXsejaQ3e+ TviDUWLmGfJk97Zmz2NPy4oGqwNYvOQqXKZ4GIpzD1/UHfNUw9wykPuDCapuvXPl OcSlSyjPk70jG32aLEalVZKPYZ1g15VSY6d6WYquZO0mGpwL15Gvc8V7SlZfNpvT 8maX5CQEeNXqfEbl2PwnkfoCwvW7x2p7uD+M2MHxOozkn5vtUonXqFCOVCftE/nL KsYrafRMuMzNRCn4kE/M =OCEQ -END PGP SIGNATURE- ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] mapFst and mapSnd
On Thu, May 30, 2013 at 10:56 PM, Tony Morris tmor...@tmorris.net wrote: class BinaryFunctor f where bimap :: (a - c) - (b - d) - f a b - f c d mapFst = (`bimap id`) mapSnd = bimap id There's a bifunctors package with: class Bifunctor f where bimap :: ... first :: a - b - f a c - f b c second :: b - c - f a b - f a c ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Simplest way to learn FRP through use
I want to learn FRP but am having trouble wading through all the theory about how FRP is implemented and how it /could/ be used for various applications. What is the simplest, easiest-to-learn module or system allowing you to quickly make something interesting (if not very impressive) in an FRP style? Say, a simple simulation of some physical phenomena outputting its state to the terminal; or an object moving on the screen; or some other toy application that I could create and play with. -- frigidcode.com signature.asc Description: OpenPGP digital signature ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Simplest way to learn FRP through use
My favorite mini app is John Conway's game of life. I implemented a version with reactive banana and found it perfect for learning the ideas. I have a simple version of the code up on GitHub if you ever want a nice example to read. I tried to make the code neat rather than worrying about performance or features. On May 31, 2013 8:43 PM, Christopher Howard christopher.how...@frigidcode.com wrote: I want to learn FRP but am having trouble wading through all the theory about how FRP is implemented and how it /could/ be used for various applications. What is the simplest, easiest-to-learn module or system allowing you to quickly make something interesting (if not very impressive) in an FRP style? Say, a simple simulation of some physical phenomena outputting its state to the terminal; or an object moving on the screen; or some other toy application that I could create and play with. -- frigidcode.com ___ 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] Simplest way to learn FRP through use
Unless I am missing something, The Haskell School of Expression has an excellent introduction to it. Tommy On May 31, 2013, at 20:41 , Christopher Howard christopher.how...@frigidcode.com wrote: I want to learn FRP but am having trouble wading through all the theory about how FRP is implemented and how it /could/ be used for various applications. What is the simplest, easiest-to-learn module or system allowing you to quickly make something interesting (if not very impressive) in an FRP style? Say, a simple simulation of some physical phenomena outputting its state to the terminal; or an object moving on the screen; or some other toy application that I could create and play with. -- frigidcode.com ___ 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
