# News aggregator

### I want to build an Android app, but I'm an amatuer programmer is haskell barking up the wrong tree?

I see a lot of old information around, ajhc, jhc, ghc-backend for android, most over a year old.

Hints of *soon* like GHC now has a proper portable backend, OpenGL apps running under SDL.

But If I want to make something using for example Material Elements from android 5.

For anyone wondering, I want to make a 3rd party chat app for a site that chat (similar fashion to facebook) only works in desktop mode.

Just to be annoying I also only use Windows at the moment maintaining another OS is a hassle.

If this is out of reach, is there another language with similar philosophy I could use?

submitted by YellowOnion[link] [28 comments]

### Let's update our versioning policy to bind closer to Semver.org

An easily spottable plague of an absolute majority of Haskell packages is that they get stuck in the 0.x.x version space, thus forever retaining that "beta" feeling even if the package's API remains stable for years and has dependencies counted by thousands. Simple example: "containers".

My take on the issue is that our current versioning policy basically makes no distinction between the A and the B in A.B.C thus rendering them both as the major version. Besides the mentioned issue this leaves us only the C for both non-breaking updates and bug-fixes, the last being the reason why some authors introduce the 4th variable D for bug-fixes.

Turns out, our policy does not accomodate to the increasingly popular language-agnostic Semver convention, in which our both A and B are united under A', thus producing A'.C.D. I.e., A' is the major version, used for API-changing updates, C is the minor version, used for API-non-changing updates, D is for bugfixes.

The aforementioned incompatibility forms another issue: it is a potential reason of confusion for the newcomers, who've previously applied Semver in other languages.

What I propose is to begin the process of updating our versioning policy to accomodate to the Semver convention.

Let's discuss this.

submitted by nikita-volkov[link] [89 comments]

### Incoherent Instances: Why does GHC not produce a warning when picking an instance arbitrarily?

For GHC 7.8.4, according to the users guide picking an instance with overlapping instances follows this procedure:

Find all instances I that match the target constraint; that is, the target constraint is a substitution instance of I. These instance declarations are the candidates.

Find all non-candidate instances that unify with the target constraint. Such non-candidates instances might match when the target constraint is further instantiated. If all of them were compiled with -XIncoherentInstances, proceed; if not, the search fails.

Eliminate any candidate IX for which both of the following hold:

- There is another candidate IY that is strictly more specific; that is, IY is a substitution instance of IX but not vice versa.
- Either IX or IY was compiled with -XOverlappingInstances.

If only one candidate remains, pick it. Otherwise if all remaining candidates were compiled with -XInccoherentInstances, pick an arbitrary candidate.

So IncoherentInstanecs is doing two things:

- Allow code to compile when there are non-candidate instances that might match.
- If there are multiple remaining candidates, pick one arbitrarily.

Since #1 can occur without #2, why does GHC not produce a warning in case 2? Such a warning would be useful since it would probably indicate an error with your program. If your program is correct, then a warning would be a useful reminder to check that all the candidate instances have the same behavior.

Note: 7.10 adds per instance pragmas, but the users guide does not suggest it adds any warnings.

submitted by llyy6[link] [7 comments]

### Ken T Takusagawa: [cssohavu] Enabling arbitrary static verification

As the complexity of programs increase, static verification features of a programming language become relatively more important, compared to say code conciseness or code execution speed (at least, constant factors of code execution speed). It becomes relatively more important for a machine verifier to be able to "understand" the program and verify correctness properties about it. That computer verifier might become the only entity that understands the entirety of a large program written over a long period of time by many authors.

Rich type systems such as in Haskell are an example of static verification. For example, it is useful to be able to annotate which code is stateful and what state it is modifying. Haskell monads accomplish such annotation, and the type checker checks that the annotations are correct.

However, Haskell types are not the be-all-end-all of static verification. In more complicated code, it is easy to want to express and verify properties which cannot be expressed in its type system.

Design a language whose static verification features are user definable and may be arbitrarily complex, keeping pace with the complexity of the program.

(We will probably eventually want to express static verification of the static verification, and so on. The difficulty of creating a correct program inherently grows faster than linearly with size of the executable part of the program. Perhaps this will prevent the technological singularity.)

Language features such as polymorphic types or other type extensions would not be hardcoded into the compiler but imported as one of many possible static verification libraries that a program can invoke in the static verification phase of its compilation. Theorem provers will also likely be useful as libraries.

Lisp syntax looks nice, with its arbitrary extensibility and ability to treat code as data, which is what the static verification code will be doing.

### Easy HTTP/2 web servers from Haskell.

### immortal profiling

### Spock tutorial and website launch

### Conal Elliott » Early inspirations and new directions in functional reactive programming

### Obfuscated haskell attempt

[link] [10 comments]

### Haskell-programming sysadmin opportunity at SFLC

### What is {-# ... #-} in the beginning of most haskell programs?

I am new to Haskell (and programming in general). I have seen many haskell programs that begin with {-# LANGUAGE (something here) #-}. What is this? What does it accomplish? Is it Haskell's version of shebang?

submitted by srivkrani[link] [55 comments]

### Type and function naming conventions

A substantial program has many names. What conventions do you use to name them? I'm asking about function names and type names that are exported from a module, including data constructors.

I see many random StackOverflow questions on this topic and scattered other blog posts and such, but most of these are about object-oriented languages. Does anyone have good conventions for a functional language?

Also, what suggestions exist for how heavily to rely on the module system to disambiguate names, and how much to use typeclasses purely for naming purposes? I tried the one data type per module style, but I did not find it to be clearly superior and the fact that it breaks too many tools and conventions (makes default Haddocks worthless) led me to abandon that idea.

Sometimes I have to name something so nebulous that I resort to random short, but memorable words. When I saw a package with Biff, Tannen, Joker, and Clown as names, I knew I am not alone in this problem.

I used to routinely name fields using record syntax, but this results in an explosion of mostly useless names so now I tend to avoid records for small types whose data constructors are exported.

*what I'm not talking about*:

short vs long variable names for local bindings that aren't exported from a module

whether things like Monoid should not be given allegedly scary-sounding names

whether type variables should have long names or use a single letter

[link] [10 comments]

### Curry arguments on a structure of functions, then fold with composition

**Motivation/Pattern**

**Definition**

**Some more toy examples**

It seems to me that <-> is applying functions to arguments in a way that is "perpendicular" to function composition.

**Operator Label**

Apparently, then Lens library contains a function ?? that is defined identically (thanks, zxamt, for pointing this out). In the use-case that I described above, I think that labeling the operator as ?? conveys very little information about what it does. In contrast, something like <-> is more readable because it looks like a function being applied to arguments.

**Discussion**

Any comments on this pattern/style?

**UPDATE: Bifunctors!**

It is easy to generalize the operator to Bifunctors (or indeed multi-functors):

(<-->) :: (Bifunctor f) => f (a -> b) (a -> c) -> a -> f b c fab <--> a = bimap ($a) ($a) fabExample:

split :: Integral a => a -> a -> (a,a) unsplit :: Integral a => a -> (a,a) -> a split k i = (div, mod) <--> i <--> k unsplit k (d, m) = k * d + m -- (split, unsplit) <--> k :: Integral a => (a -> (a,a), (a,a) -> a) composeTuple :: (b -> c, a -> b) -> a -> c composeTuple (f,g) = f . g -- For all k: composeTuple $ (split, unsplit) <--> k = id -- For all k: composeTuple $ (unsplit, split) <--> k = id**UPDATE**

Apparently, this is an operation that works on any "representable functor". There is a whole post on it in Comonad.Reader. From the article:

distributeReader :: Functor f => f (r -> a) -> (r -> f a) distributeReader fra = \r -> fmap ($r) fraAs you can see, distributeReader is the same as <->. The article is the third in a series on applicatives. There is also a memoization library based on this idea.

submitted by newestHaskeller[link] [8 comments]

### wren gayle romano: An introduction to recursive types

The past couple weeks I've been teaching about recursive types and their encodings in B522. Here's a short annotated bibliography for followup reading:

- For a basic intro to recursive types, and for the set-theoretic metatheory: see section IV, chapters 20 and 21.
- Benjamin C. Pierce (2002)
*Types and Programming Languages.*MIT Press.

- Benjamin C. Pierce (2002)
- The proof of logical inconsistency and non-termination is "well-known". For every type τ we can define a fixed-point combinator and use that to exhibit an inhabitant of the type:
- fixτ = λf:(τ→τ). let e = λx:(μα.α→τ). f (x (unroll x)) in e (roll(μα.α→τ) e)
- ⊥τ = fixτ (λx:τ. x)

- A category-theoretic proof that having fixed-points causes inconsistency
- Hagen Huwig and Axel Poigné (1990)
*A note on inconsistencies caused by fixpoints in a Cartesian Closed Category.*Theoretical Computer Science, 73:101–112.

- Hagen Huwig and Axel Poigné (1990)
- The proof of Turing-completeness is "well-known". Here's a translation from the untyped λ-calculus to STLC with fixed-points:
- (x)* = x
- (λx. e)* = roll(μα.α→α) (λx:(μα.α→α). e*)
- (f e)* = unroll (f*) (e*)

- Knaster–Tarski (1955): For any monotone function, f, (a) the least fixed-point of f is the intersection of all f-closed sets, and (b) the greatest fixed-point of f is the union of all f-consistent sets.
- Alfred Tarski (1955)
*A lattice-theoretical fixpoint theorem and its applications.*Pacific Journal of Mathematics 5(2):285–309. - Bronisław Knaster (1928)
*Un théorème sur les fonctions d'ensembles.*Annales de la Société Polonaise de Mathématique, 6:133–134.

- Alfred Tarski (1955)
- For a quick introduction to category theory, a good place to start is:
- Benjamin C. Pierce (1991)
*Basic Category Theory for Computer Scientists.*MIT Press.

- Benjamin C. Pierce (1991)
- For a more thorough introduction to category theory, consider:
- Jiří Adámek, Horst Herrlich, and George Strecker (1990)
*Abstract and Concrete Categories: The Joy of Cats.*John Wiley and Sons.

- Jiří Adámek, Horst Herrlich, and George Strecker (1990)
- The Boehm–Berarducci encoding
- Oleg Kiselyov (2012)
*Beyond Church encoding: Boehm–Berarducci isomorphism of algebraic data types and polymorphic lambda-terms* - Corrado Boehm and Alessandro Berarducci (1985)
*Automatic Synthesis of Typed Lambda-Programs on Term Algebras.*Theoretical Computer Science, v39:135–154

- Oleg Kiselyov (2012)
- Church/Boehm–Berarducci encodings are not canonical
- [citation needed]

- Surjective pairing cannot be encoded in STLC (i.e., the implicational fragment of intuitionistic propositional logic): see p.155
- Morten H. Sørensen and Paweł Urzyczyn (2006)
*Lectures on the Curry–Howard isomorphism.*Studies in Logic and the Foundations of Mathematics, v.149.

- Morten H. Sørensen and Paweł Urzyczyn (2006)
- However, adding it is a conservative extension
- Roel de Vrijer (1987)
*Surjective Pairing and Strong Normalization: Two themes in lambda calculus.*dissertation, University of Amsterdam. - Roel de Vrijer (1989)
*Extending the lambda calculus with surjective pairing is conservative.*4th LICS, pp.204–215. - Kristian Støvring (2005)
*Extending the Extensional Lambda Calculus with Surjective Pairing is Conservative.*BRICS.

- Roel de Vrijer (1987)
- Compiling data types with Scott encodings
- Jan Martin Jansen, Pieter Koopman, and Rinus Plasmeijer (200X)
*Data Types and Pattern Matching by Function Application.* - Jan Martin Jansen, Pieter Koopman, and Rinus Plasmeijer (2006)
*Efficient Interpretation by Transforming Data Types and Patterns to Functions.*Trends in Functional Programming. - Jan Martin Jansen, Rinus Plasmeijer, and Pieter Koopman (2010)
*Comprehensive Encoding of Data Types and Algorithms in the λ-Calculus.*J. Functional Programming. - Pieter Koopman, Rinus Plasmeijer, and Jan Martin Jansen (2014)
*Church encoding of data types considered harmful for implementations.*IFL submission

- Jan Martin Jansen, Pieter Koopman, and Rinus Plasmeijer (200X)
- For more on the difference between Scott and Mogensten–Scott encodings:
- Aaron Stump (2009)
*Directly Reflective Meta-Programming.*J. Higher Order and Symbolic Computation, 22(2):115–144.

- Aaron Stump (2009)
- Parigot encodings
- M. Parigot (1988)
*Programming with proofs: A second-order type theory.*ESOP, LNCS 300, pp.145–159. Springer.

- M. Parigot (1988)
- For more on catamorphisms, anamorphisms, paramorphisms, and apomorphisms
- Varmo Vene and Tarmo Uustalu (1998)
*Functional programming with apomorphisms (corecursion).*In Proc. Estonian Acad. Sci. Phys. Math., 47:147–161 - Erik Meijer, Maarten Fokkinga, and Ross Paterson (1991)
*Functional Programming with Bananas, Lenses, Envelopes, and Barbed Wire.*In Proc. 5th ACM conference on Functional programming languages and computer architecture, pp.124–144

- Varmo Vene and Tarmo Uustalu (1998)
- build/foldr list fusion
- Andy Gill, John Launchbury, and Simon Peyton Jones (1993)
*A short cut to deforestation.*In Proc. Functional Programming Languages and Computer Architecture, pp.223–232. - Many more links at the bottom of this page

- Andy Gill, John Launchbury, and Simon Peyton Jones (1993)
- For another general introduction along the lines of what we covered in class
- Philip Wadler (1990)
*Recursive types for free!*

- Philip Wadler (1990)
- "Iterators" vs "recursors" in Heyting arithmetic and Gödel's System T: see ch.10:
- Morten H. Sørensen and Paweł Urzyczyn (2006)
*Lectures on the Curry–Howard isomorphism*Studies in Logic and the Foundations of Mathematics, v.149.

- Morten H. Sørensen and Paweł Urzyczyn (2006)
- There are a great many more papers by Tarmo Uustalu, Varmo Vene, Ralf Hinze, and Jeremy Gibbons on all this stuff; just google for it.

comments