News aggregator

Danny Gratzer: Some Useful Agda

Planet Haskell - Fri, 06/27/2014 - 6:00pm
Posted on June 28, 2014

I’ve been using Agda for a few months now. I’ve always meant to figure out how it handles IO but never have.

Today I decided to change that! So off I went to the related Agda wiki page. So hello world in Agda apparently looks like this

open import IO main = run (putStrLn "test")

The first time I tried running this I got an error about an IO.FFI, if you get this you need to go into your standard library and run cabal install in the ffi folder.

Now, on to what this actually does. Like Haskell, Agda has an IO monad. In fact, near as I can tell this isn’t a coincidence at all, Agda’s primitive IO seems to be a direct call to Haskell’s IO.

Unlike Haskell, Agda has two IO monads, a “raw” primitive one and a higher level pure one found in IO.agda. What few docs there are make it clear that you are not intended to write the “primitive IO”.

Instead, one writes in this higher level IO monad and then uses a function called run which converts everything to the primitive IO.

So one might ask: what exactly is this strange IO monad and how does it actually provide return and >>=? Well the docs don’t actually seem to exist so poking about the source reveals

data IO {a} (A : Set a) : Set (suc a) where lift : (m : Prim.IO A) → IO A return : (x : A) → IO A _>>=_ : {B : Set a} (m : ∞ (IO B)) (f : (x : B) → ∞ (IO A)) → IO A _>>_ : {B : Set a} (m₁ : ∞ (IO B)) (m₂ : ∞ (IO A)) → IO A

Wow.. I don’t know about you, but this was a bit different than I was expecting.

So this actually just forms a syntax tree! There’s something quite special about this tree though, those ∞ annotations mean that it’s a “coinductive” tree. So we can construct infinite IO tree. Otherwise it’s just a normal tree.

Right below that in the source is the definition of run

{-# NO_TERMINATION_CHECK #-} run : ∀ {a} {A : Set a} → IO A → Prim.IO A run (lift m) = m run (return x) = Prim.return x run (m >>= f) = Prim._>>=_ (run (♭ m )) λ x → run (♭ (f x)) run (m₁ >> m₂) = Prim._>>=_ (run (♭ m₁)) λ _ → run (♭ m₂)

So here’s where the evilness comes in! We can loop forever transforming our IO into a Prim.IO.

Now I had never used Agda’s coinductive features before and if you haven’t either than they’re not terribly complicated.

∞ is a prefix operator that stands for a “coinductive computation” which is roughly a thunk. ♯ is a prefix operator that delays a computation and ♭ forces it.

There are reasonably complex rules that govern what qualifies as a “safe” way to force things. Guarded recursion seems to always work though. So we can write something like

open import Coinduction open import Data.Unit data Cothingy (A : Set) : Set where conil : Cothingy A coCons : A → ∞ (Cothingy A) → Cothingy A lotsa-units : Cothingy ⊤ lotsa-units = coCons tt (♯ lotsa-units)

Now using ♯ we can actually construct programs with infinite output.

forever : IO ⊤ forever = ♯ putStrLn "Hi" >> ♯ forever main = run forever

This when run will output “Hi” forever. This is actually quite pleasant when you think about it! You can view you’re resulting computation as a normal, first class data structure and then reify it to actual computations with run.

So with all of this figured out, I wanted to write a simple program in Agda just to make sure that I got it all.

FizzBuzz

I decided to write the fizz-buzz program. For those unfamiliar, the specification of the program is

For each of the numbers 0 to 100, if the number is divisible by 3 print fizz, if it’s divisible by 5 print buzz, if it’s divisible by both print fizzbuzz. Otherwise just print the number.

This program is pretty straightforward. First, the laundry list of imports

module fizzbuzz where import Data.Nat as N import Data.Nat.DivMod as N import Data.Nat.Show as N import Data.Bool as B import Data.Fin as F import Data.Unit as U import Data.String as S open import Data.Product using (_,_ ; _×_) open import IO open import Coinduction open import Relation.Nullary open import Function

This seems to be the downside of finely grained modules.. Tons and tons of imports.

Now we need a function which takes to ℕs and returns true if the first mod the second is zero.

congruent : N.ℕ → N.ℕ → B.Bool congruent n N.zero = B.false congruent n (N.suc m) with N._≟_ 0 $ F.toℕ (N._mod_ n (N.suc m) {U.tt}) ... | yes _ = B.true ... | no _ = B.false

Now from here we can combine this into the actual worker for the program

_and_ : {A B : Set} → A → B → A × B _and_ = _,_ fizzbuzz : N.ℕ → S.String fizzbuzz N.zero = "fizzbuzz" fizzbuzz n with congruent n 3 and congruent n 5 ... | B.true , B.true = "fizzbuzz" ... | B.true , B.false = "fizz" ... | B.false , B.true = "buzz" ... | B.false , B.false = N.show n

Now all that’s left is the IO glue

worker : N.ℕ → IO U.⊤ worker N.zero = putStrLn $ fizzbuzz N.zero worker (N.suc n) = ♯ worker n >> ♯ putStrLn (fizzbuzz $ N.suc n) main = run $ worker 100

There. A somewhat real, IO based program written in Agda. It only took me 8 months to figure out how to write it :)

<script type="text/javascript"> /* * * CONFIGURATION VARIABLES: EDIT BEFORE PASTING INTO YOUR WEBPAGE * * */ var disqus_shortname = 'codeco'; // required: replace example with your forum shortname /* * * DON'T EDIT BELOW THIS LINE * * */ (function() { var dsq = document.createElement('script'); dsq.type = 'text/javascript'; dsq.async = true; dsq.src = '//' + disqus_shortname + '.disqus.com/embed.js'; (document.getElementsByTagName('head')[0] || document.getElementsByTagName('body')[0]).appendChild(dsq); })(); </script> <noscript>Please enable JavaScript to view the comments powered by Disqus.</noscript> comments powered by Disqus
Categories: Offsite Blogs

"Generating" type synonyms without Template Haskell

haskell-cafe - Fri, 06/27/2014 - 5:52pm
I'd like to know how to conveniently generate specialisations of a product type without resorting to Template Haskell. Concretely, I have a type like data MyProduct a b c = MyProduct { foo :: a , bar :: b , baz :: c } and I use it in type signatures in various different specialisations. Generally the "base" type of each component stays fixed but it is wrapped in zero or more type constructors. For example a. MyProduct Int Bool String b. MyProduct (Maybe Int) (Maybe Bool) (Maybe String) c. MyProduct [IO Int] [IO Bool] [IO String] d. MyProduct (P Int) (P Bool) (P String) for various P that are not always functors in my uses. I thought I might be able to reduce this duplication by parametrisation, that is data MyProduct f a b c = MyProduct { foo :: f a , bar :: f b , baz :: f c } However, I can't always substitute a type const
Categories: Offsite Discussion

Empty case alternative

haskell-cafe - Fri, 06/27/2014 - 5:18pm
Hello cafe, I was looking into Haskell Report 2010 and notice something in the definition of case statement: https://www.haskell.org/onlinereport/haskell2010/haskellch3.html#x8-460003.13 Apparently an empty alternative within case statement is a plausible production. ('alt' production rule, third option). If I get it correctly, following example shows the empty alternative: What I miss is any ratio behind this. What is the empty alternative good for? Any idea? Franta
Categories: Offsite Discussion

Why does this work: 1 < 2.0?

Haskell on Reddit - Fri, 06/27/2014 - 3:12pm

Hi,

I'm not very fluent in Haskell, but from the little I know about type classes I was expecting the comparison in the title, i.e. 1 < 2.0, to fail without and explicit cast like fromIntegral. Why (and how) does it work? I am aware that both 1 and 2.0 have instances for Num, but is that enough? If so, how would such a comparison be handled by the runtime?

Thanks,

Alex

submitted by alex_muscar
[link] [18 comments]
Categories: Incoming News

.hs to .lhs

Haskell on Reddit - Fri, 06/27/2014 - 7:32am
Categories: Incoming News

POSIX capabilities support

haskell-cafe - Fri, 06/27/2014 - 12:31am
Hello Haskellers, I have looked through the various POSIX hack age modules to see if there is capabilities support. ??? Regards, Vasya _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe< at >haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Categories: Offsite Discussion

Bill Atkins: Unit Testing in Swift

Planet Haskell - Thu, 06/26/2014 - 9:24pm
Since Swift was released at the beginning of the month, I've been doing using it for most of my iOS development. It's been a pleasant experience: I've been able to discard huge amounts of boilerplate and take advantage of a few functional programming techniques that were previously unavailable on the iPhone and iPad.

One area where Swift has made huge improvements over Objective-C is unit tests. Objective-C's verbosity made it difficult to create small, focused classes to perform specific tasks. Plus, the language's insistence on keeping only one class to a file and the cumbersome pairing of every implementation file with a header imposed a hefty penalty on programmers who tried to divide their work up into discrete, testable components.

Unit testing in Swift is done with the same XCTest framework introduced back in Xcode 5 for Objective-C. But Swift's concision and its inclusion of modern language features like closures makes XCTest much more pleasant than it was to use under Objective-C. We'll walk through a very simple example of Swift unit testing below.

To get started, create an empty iOS Application project in Xcode called Counter. Xcode will generate a CounterTests folder for you and an associated test target.

First, let's create a simple class to be tested. Create the file "Counter.swift" and add the following code to it:

import Foundation
class Counter {  var count: Int    init(count: Int) {    self.count = count  }    convenience init() {    self.init(count: 0)  }    func increment() {    self.count++  }
}
This is a very simple class, but it will be enough to illustrate how to use XCTest to test your own Swift code.

Create a file called "CounterTest.swift" in the CounterTests folder Xcode generated for you (this simple test will be your "Hello, world" for Swift testing):

import XCTestimport Counter
class CounterTest: XCTestCase {  func testSimpleAddition() {    let counter = Counter()    XCTAssertEqual(0, counter.count)  }
}
NOTE: In the current version of Swift (Beta 2), you have to import your main target into the test target to get your tests to compile and run. This is why we import Counter at the top.

NOTE: I've seen a few Swift tutorials recommend that you use the built-in Swift function assert in your test cases - do not do this! assert will terminate your entire program if it fails. Using the XCTAssert functions provides a number of important benefits:

  • If one test case fails, your other cases can continue running; assert stops the entire program.
  • Because the XCTAssert functions are more explicit about what you're expecting, they can print helpful failure messages (e.g. "2 was not equal to 3") whereas assert can only report that its condition was false. There's a broad variety of assert functions, including XCTAssertLessThan, XCTAssertNil, etc.
  • The Swift language specification explicitly forbids string interpolation in the message passed to assert; the XCTAssert functions don't face this limitation.
To try your test code out, click "Test" on the "Product" menu. Your single test should pass.
We'll add two more test cases to create and exercise several instances of Counter and to ensure that the counter wraps around when it overflows:
import XCTestimport Test
class CounterTest: XCTestCase {  func testInvariants() {    let counter = Counter()    XCTAssertEqual(0, counter.count, "Counter not initialized to 0")        counter.increment()    XCTAssertEqual(1, counter.count, "Increment is broken")
    XCTAssertEqual(1, counter.count, "Count has unwanted side effects!")  }    func testMultipleIncrements() {    let counts = [1, 2, 3, 4, 5, 6]        for count in counts {      let counter = Counter()            for i in 0..count {        counter.increment()      }            XCTAssertEqual(counter.count, count, "Incremented value does not match expected")    }  }    func testWraparound() {    let counter = Counter(count: Int.max)    counter.increment()        XCTAssertEqual(counter.count, Int.min)  }}
These tests should pass as well.

You can find out more about XCTest in the Apple guide "Testing with Xcode." I hope this was helpful - please feel free to comment if anything is unclear.
Categories: Offsite Blogs

A joke in the form of types

Haskell on Reddit - Thu, 06/26/2014 - 8:51pm
data Turtles = Turtle Turtles deriving ( Show ) turtles :: Turtles turtles = Turtle turtles submitted by kwef
[link] [18 comments]
Categories: Incoming News

ICFP 2014 Call for Participation

haskell-cafe - Thu, 06/26/2014 - 7:55pm
[ Please note that much of the block reservation of hotel rooms currently being held for ICFP participants will be released next week. The beginning of September is a very busy conference week in Göteborg, so there is high pressure on hotel rooms in that period. If you plan to attend ICFP 2014, it would be best to make your hotel reservations now before the block reservation expires. ] ===================================================================== Call for Participation ICFP 2014 19th ACM SIGPLAN International Conference on Functional Programming and affiliated events August 31 - September 6, 2013 Gothenburg, Sweden http://icfpconference.org/icfp2014/ ===================================================================== ICFP provides a forum for researchers and developers to hear about the latest work on the design, implementations, principles, and uses of functional programming. The conference covers the e
Categories: Offsite Discussion

ICFP 2014 Call for Participation

General haskell list - Thu, 06/26/2014 - 7:55pm
[ Please note that much of the block reservation of hotel rooms currently being held for ICFP participants will be released next week. The beginning of September is a very busy conference week in Göteborg, so there is high pressure on hotel rooms in that period. If you plan to attend ICFP 2014, it would be best to make your hotel reservations now before the block reservation expires. ] ===================================================================== Call for Participation ICFP 2014 19th ACM SIGPLAN International Conference on Functional Programming and affiliated events August 31 - September 6, 2013 Gothenburg, Sweden http://icfpconference.org/icfp2014/ ===================================================================== ICFP provides a forum for researchers and developers to hear about the latest work on the design, implementations, principles, and uses of functional programming. The conference covers the e
Categories: Incoming News

Philip Wadler: Propositions as Types, updated

Planet Haskell - Thu, 06/26/2014 - 7:42pm
Propositions as Types has been updated. Thanks to all the readers and reviewers who helped me improve the paper.

Propositions as Types
Philip Wadler
Draft, 26 June 2014

The principle of Propositions as Types links logic to computation. At first sight it appears to be a simple coincidence---almost a pun---but it turns out to be remarkably robust, inspiring the design of theorem provers and programming languages, and continuing to influence the forefronts of computing. Propositions as Types has many names and many origins, and is a notion with depth, breadth, and mystery.Comments still solicited!
Categories: Offsite Blogs

New version of vector + discussion

libraries list - Thu, 06/26/2014 - 3:42pm
Hi all, I've prepped a new minor version (0.10.12.0) of the 0.10 branch of vector so that we can release https://github.com/haskell/vector/pull/31, which I cherry-picked from master. Could someone please review this and do the upload? I'm not sure I have the right bit set. Also, in a related topic, an aside: I tried to merge 0.10 into master and got a horrorshow: # Unmerged paths: # (use "git add/rm <file>..." as appropriate to mark resolution) # # both modified: Data/Vector.hs # deleted by them: Data/Vector/Fusion/Bundle/Monadic.hs # both modified: Data/Vector/Fusion/Stream.hs # both modified: Data/Vector/Fusion/Stream/Monadic.hs # both modified: Data/Vector/Fusion/Stream/Size.hs # both modified: Data/Vector/Generic.hs # both modified: Data/Vector/Generic/Mutable.hs # deleted by them: Data/Vector/Generic/Mutable/Base.hs # both modified: Data/Vector/Generic/New.hs # both modified: Data/Vector/Mutable.hs # both modified: Data/Vector/Storable.hs # both mo
Categories: Offsite Discussion

2nd CfP: WFLP 2014 - Workshop on Functional and (Constraint) Logic Programming

General haskell list - Thu, 06/26/2014 - 3:21pm
(note: Deadline extended to July 10th) *********************************************************** 23rd International Workshop on Functional and (Constraint) Logic Programming http://www.imn.htwk-leipzig.de/WFLP2014/ colocated with 28th Workshop on (Constraint) Logic Programming (WLP 2014) September 15 - 17, at Leucorea conference center in Lutherstadt Wittenberg, Germany. *********************************************************** Dates: * submission closes: July 10, 2014 * notification: August 4, 2014 * final version due: September 1, 2014 * workshop: September 15 - 17, 2014 *********************************************************** The international workshops on functional and logic programming aim at bringing together researchers interested in functional programming, logic programming, as well as their integration. The workshops on (constraint) logic programming serve as the scientific forum of the annual meeting of the Society of Logic Programming (GLP e.V.) and bring together researchers int
Categories: Incoming News