Re: [Haskell-cafe] Propositions in Haskell
I do understand the difference between theorem provers and Haskell programs.Logic can be used to reason 'about' Haskell programs and logic can be used 'within' Haskell programs.I am trying to clarify the difference between 'about' and 'within'Is approach 1 concerned with |= (model based 'within'), whereas approach 2 is concerned with |- (proof based 'about')?Thanks,PatOn 15/05/13, Alberto G. Corona agocor...@gmail.com wrote:Not exactly what you ask, but it is noteworthy that the mind has different logic processors. The fastest one work with IF THEN ELSE rules applied specifically to deals. This is why your example (and most examples of logic) involves a kind of deal expressed in the first person. This trigger a fast mental evaluation, while an equivalent but more general case is harder to process and need some paper work. (That special treatment of first person deals logic respond to the need to detect breaks of deals as fast as possible) http://en.wikipedia.org/wiki/Wason_selection_taskThat's why higher level languages have redundant logical structures and do not follow a general abstract and short mathematical notation. Therefore higher level, in programming languages, does not mean higher mathematical abstraction, but to be closer to the way the mind works. 2013/5/15 Patrick Browne patrick.bro...@dit.ie patrick.bro...@dit.ie -- Hi-- I am trying to show that a set of propositions and a conclusion the form a valid argument.-- I used two approaches; 1) using if-then-else, 2) using pattern matching. -- The version using if-then-else seems to be consistent with my knowledge of Haskell and logic (either of which could be wrong).-- Can the second approach be improved to better reflect the propositions and conclusion? Maybe type level reasoning could be used? -- -- Valid argument?-- 1. I work hard or I play piano-- 2. If I work hard then I will get a bonus-- 3. But I did not get a bonus-- Therefore I played piano-- Variables: p = Piano, w = worked hard, b = got a bonus -- (w \/ p) /\ (w = b) /\ ¬(b)-- --- -- p -- First approach using language control structure if-then-elsew, p, b::Bool-- Two equivalences for (w \/ p) as an implication. -- 1. (w \/ p) =equivalent-to= (not p) = w-- 2. (w \/ p) =equivalent-to= (not w) = p-- Picked 2p = if (not w) then True else False -- Contrapositive: (w = b) =equivalent-to= ~b = ~w w = if (not b) then False else Trueb = False -- gives p is true and w is false-- Second approach using pattern matching -- I think the rewriting goes from left to right but the logical inference goes in the opposite direction. w1, p1, b1::Boolp1 = (not w1) w1 = b1 -- Not consistent with statements, but I do not know how to write ~b1 = ~w1 in Haskellb1 = False-- Again gives p1 is true and w1 is false Tá an teachtaireacht seo scanta ó thaobh ábhar agus víreas ag Seirbhís Scanta Ríomhphost de chuid Seirbhísí Faisnéise, ITBÁC agus meastar í a bheith slán. http://www.dit.ie This message has been scanned for content and viruses by the DIT Information Services E-Mail Scanning Service, and is believed to be clean. http://www.dit.ie ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe -- Alberto. Tá an teachtaireacht seo scanta ó thaobh ábhar agus víreas ag Seirbhís Scanta Ríomhphost de chuid Seirbhísí Faisnéise, ITBÁC agus meastar í a bheith slán. http://www.dit.ie This message has been scanned for content and viruses by the DIT Information Services E-Mail Scanning Service, and is believed to be clean. http://www.dit.ie ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Propositions in Haskell
maybe this will help? Haskell code in and of itself isn't special. proofs can happen with the type system, but typically you'd want to define a target language and do assertions about it, similar to how a compiler inspects it's input programs. Haskell is not homoiconic nor is it like coq or prolog. But it is really really good at defining an ast and doing operations on it. On Thu, May 16, 2013 at 5:27 AM, Patrick Browne patrick.bro...@dit.iewrote: I do understand the difference between theorem provers and Haskell programs. Logic can be used to reason 'about' Haskell programs and logic can be used 'within' Haskell programs. I am trying to clarify the difference between 'about' and 'within' Is approach 1 concerned with |= (model based 'within'), whereas approach 2 is concerned with |- (proof based 'about')? Thanks, Pat On 15/05/13, *Alberto G. Corona * agocor...@gmail.com wrote: Not exactly what you ask, but it is noteworthy that the mind has different logic processors. The fastest one work with IF THEN ELSE rules applied specifically to deals. This is why your example (and most examples of logic) involves a kind of deal expressed in the first person. This trigger a fast mental evaluation, while an equivalent but more general case is harder to process and need some paper work. (That special treatment of first person deals logic respond to the need to detect breaks of deals as fast as possible) http://en.wikipedia.org/wiki/Wason_selection_task That's why higher level languages have redundant logical structures and do not follow a general abstract and short mathematical notation. Therefore higher level, in programming languages, does not mean higher mathematical abstraction, but to be closer to the way the mind works. 2013/5/15 Patrick Browne patrick.bro...@dit.ie patrick.bro...@dit.ie -- Hi -- I am trying to show that a set of propositions and a conclusion the form a valid argument. -- I used two approaches; 1) using if-then-else, 2) using pattern matching. -- The version using if-then-else seems to be consistent with my knowledge of Haskell and logic (either of which could be wrong). -- Can the second approach be improved to better reflect the propositions and conclusion? Maybe type level reasoning could be used? -- -- Valid argument? -- 1. I work hard or I play piano -- 2. If I work hard then I will get a bonus -- 3. But I did not get a bonus -- Therefore I played piano -- Variables: p = Piano, w = worked hard, b = got a bonus --(w \/ p) /\ (w = b) /\ ¬(b) -- --- --p -- First approach using language control structure if-then-else w, p, b::Bool -- Two equivalences for (w \/ p) as an implication. -- 1. (w \/ p) =equivalent-to= (not p) = w -- 2. (w \/ p) =equivalent-to= (not w) = p -- Picked 2 p = if (not w) then True else False -- Contrapositive: (w = b) =equivalent-to= ~b = ~w w = if (not b) then False else True b = False -- gives p is true and w is false -- Second approach using pattern matching -- I think the rewriting goes from left to right but the logical inference goes in the opposite direction. w1, p1, b1::Bool p1 = (not w1) w1 = b1 -- Not consistent with statements, but I do not know how to write ~b1 = ~w1 in Haskell b1 = False -- Again gives p1 is true and w1 is false Tá an teachtaireacht seo scanta ó thaobh ábhar agus víreas ag Seirbhís Scanta Ríomhphost de chuid Seirbhísí Faisnéise, ITBÁC agus meastar í a bheith slán. http://www.dit.ie This message has been scanned for content and viruses by the DIT Information Services E-Mail Scanning Service, and is believed to be clean. http://www.dit.ie ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe -- Alberto. Tá an teachtaireacht seo scanta ó thaobh ábhar agus víreas ag Seirbhís Scanta Ríomhphost de chuid Seirbhísí Faisnéise, ITBÁC agus meastar í a bheith slán. http://www.dit.ie This message has been scanned for content and viruses by the DIT Information Services E-Mail Scanning Service, and is believed to be clean. http://www.dit.ie ___ 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] Infrastructure for testing the impact of a Functor/Applicative/Monad hierarchy
Reading the other thread (Adding Applicative/Functor instances to all Monads in GHC) I was wondering if there was infrastructure for testing what effect making the often-discussed Functor/Monad change would have: How many packages on hackage would break etc. I have read a few times that people have compiled all of hackage to see the impact of whatever. How do you do that? Do you just run a loop around cabal install or have you built some more advanced tools to visualize the results better or compile the packages from ground up, in order of their dependencies? I'm interested in anything in this direction. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Infrastructure for testing the impact of a Functor/Applicative/Monad hierarchy
Has anyone surveyed the in-print textbooks, tutorials, or tried to assess how much Haskell (H98, H2010, Glasgow Haskell?) is used in teaching? Having the wrong hierarchy is a minor annoyance to us members of the cognoscenti, but a change outside a revision of the language standard could leave a lot of beginners and the teaching material they rely on stranded. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Infrastructure for testing the impact of a Functor/Applicative/Monad hierarchy
There is a chicken and the egg problem with this argument. Historically Haskell' has only considered changes that have been actually implemented. I would encourage the language standard to follow suit, but we survived a similar autocratic minor change to Num with very little ecosystem disruption. -Edward On Thu, May 16, 2013 at 12:28 PM, Stephen Tetley stephen.tet...@gmail.comwrote: Has anyone surveyed the in-print textbooks, tutorials, or tried to assess how much Haskell (H98, H2010, Glasgow Haskell?) is used in teaching? Having the wrong hierarchy is a minor annoyance to us members of the cognoscenti, but a change outside a revision of the language standard could leave a lot of beginners and the teaching material they rely on stranded. ___ 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] Library for drawing simple user interface
Hi, Which library should I use for simple user interface? Should I use opengl directly (through HOpenGL)? Or Gloss? Or something else? I want to create small ui library from scratch in haskell. Emanuel ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] List comprehensions with Word8
Hello everyone, I was playing with Word8 and list comprehensions and the following examples came up. I have to admit the behavior looks quite strange because it does not seem to be consistent. Can someone shed some light on reason behind some of these outputs? By the way, I have abbreviated some outputs with ellipsis ... [1..10] :: [Word8] [1,2,3,4,5,6,7,8,9,10] [1..100] :: [Word8] [1,2,3,4,5,6,7,8,9,10,...,100] [1..1000] :: [Word8] [1,2,3,4,5,6,7,8,9,10,...,232] [1..1] :: [Word8] [1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16] [1..10] :: [Word8] [1,2,3,4,5,6,7,8,9,10,...,160] [1..100] :: [Word8] [1,2,3,4,5,6,7,8,9,10,...,64] [1..1000] :: [Word8] [1,2,3,4,5,6,7,8,9,10,...,128] [1..1] :: [Word8] [] [1..10] :: [Word8] [] Thank you, Jose -- José António Branquinho de Oliveira Lopes Instituto Superior Técnico Technical University of Lisbon ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] List comprehensions with Word8
Prelude 10 `mod` 256 0 So [1..10] == [1..0]. Cheers, On Thu, May 16, 2013 at 6:15 PM, Jose A. Lopes jose.lo...@ist.utl.pt wrote: Hello everyone, I was playing with Word8 and list comprehensions and the following examples came up. I have to admit the behavior looks quite strange because it does not seem to be consistent. Can someone shed some light on reason behind some of these outputs? By the way, I have abbreviated some outputs with ellipsis ... [1..10] :: [Word8] [1,2,3,4,5,6,7,8,9,10] [1..100] :: [Word8] [1,2,3,4,5,6,7,8,9,10,...,100] [1..1000] :: [Word8] [1,2,3,4,5,6,7,8,9,10,...,232] [1..1] :: [Word8] [1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16] [1..10] :: [Word8] [1,2,3,4,5,6,7,8,9,10,...,160] [1..100] :: [Word8] [1,2,3,4,5,6,7,8,9,10,...,64] [1..1000] :: [Word8] [1,2,3,4,5,6,7,8,9,10,...,128] [1..1] :: [Word8] [] [1..10] :: [Word8] [] Thank you, Jose -- José António Branquinho de Oliveira Lopes Instituto Superior Técnico Technical University of Lisbon ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe -- Felipe. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] List comprehensions with Word8
This happens because of how fromInteger is defined for Word8. It maps integers to integers mod 256. Also remember that 10 is actually fromInteger 10, in all of your examples. So your example is actually equivalent to [0..1 `mod` 256]. On May 16, 2013 2:19 PM, Jose A. Lopes jose.lo...@ist.utl.pt wrote: Hello everyone, I was playing with Word8 and list comprehensions and the following examples came up. I have to admit the behavior looks quite strange because it does not seem to be consistent. Can someone shed some light on reason behind some of these outputs? By the way, I have abbreviated some outputs with ellipsis ... [1..10] :: [Word8] [1,2,3,4,5,6,7,8,9,10] [1..100] :: [Word8] [1,2,3,4,5,6,7,8,9,10,...,100] [1..1000] :: [Word8] [1,2,3,4,5,6,7,8,9,10,...,232] [1..1] :: [Word8] [1,2,3,4,5,6,7,8,9,10,11,12,**13,14,15,16] [1..10] :: [Word8] [1,2,3,4,5,6,7,8,9,10,...,160] [1..100] :: [Word8] [1,2,3,4,5,6,7,8,9,10,...,64] [1..1000] :: [Word8] [1,2,3,4,5,6,7,8,9,10,...,128] [1..1] :: [Word8] [] [1..10] :: [Word8] [] Thank you, Jose -- José António Branquinho de Oliveira Lopes Instituto Superior Técnico Technical University of Lisbon __**_ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/**mailman/listinfo/haskell-cafehttp://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] List comprehensions with Word8
On Thu, 16 May 2013 23:15:33 +0200, you wrote: Hello everyone, I was playing with Word8 and list comprehensions and the following examples came up. I have to admit the behavior looks quite strange because it does not seem to be consistent. Can someone shed some light on reason behind some of these outputs? When you say some positive integer :: [Word8] what you're effectively saying is some positive integer `mod` 256 because that's what fits into a slot that's 8 bits wide. So: 1000 `mod` 256 = 232 1 `mod` 256 = 16 and so on. -Steve Schafer ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] List comprehensions with Word8
At risk of belaboring the now-obvious, note that the empty lists begin at 1, which is 10^8, and thus the first power of 10 evenly divisible by 2^8. The largest value in the list for each 10^n is likewise 0 modulo 2^n. (Figuring out why the sequence has those particular multiples of 2^n is left as an exercise for the reader.) - C. On Thu, May 16, 2013 at 5:15 PM, Jose A. Lopes jose.lo...@ist.utl.pt wrote: Hello everyone, I was playing with Word8 and list comprehensions and the following examples came up. I have to admit the behavior looks quite strange because it does not seem to be consistent. Can someone shed some light on reason behind some of these outputs? By the way, I have abbreviated some outputs with ellipsis ... [1..10] :: [Word8] [1,2,3,4,5,6,7,8,9,10] [1..100] :: [Word8] [1,2,3,4,5,6,7,8,9,10,...,100] [1..1000] :: [Word8] [1,2,3,4,5,6,7,8,9,10,...,232] [1..1] :: [Word8] [1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16] [1..10] :: [Word8] [1,2,3,4,5,6,7,8,9,10,...,160] [1..100] :: [Word8] [1,2,3,4,5,6,7,8,9,10,...,64] [1..1000] :: [Word8] [1,2,3,4,5,6,7,8,9,10,...,128] [1..1] :: [Word8] [] [1..10] :: [Word8] [] Thank you, Jose -- José António Branquinho de Oliveira Lopes Instituto Superior Técnico Technical University of Lisbon ___ 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] A use case for *real* existential types
* o...@okmij.org o...@okmij.org [2013-05-11 05:26:55-] I must say though that I'd rather prefer Adres solution because his init init :: (forall a. Inotify a - IO b) - IO b ensures that Inotify does not leak, and so can be disposed of at the end. So his init enforces the region discipline and could, after a trivial modification to the code, automatically do a clean-up of notify descriptors -- something you'd probably want to do. Well, it is still possible to escape if one wants, using an existential type: data Escape = forall a . Escape (Inotify a) (Watch a) main = do Escape inotify watch - init $ \inotify - do watch - addWatch inotify foo return $ Escape inotify watch rmWatch inotify watch This is because here, unlike in the ST case, the monad itself (IO) is not tagged. It's probably not easy to do this by accident, but I think ensures is too strong a word here. Roman ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Lambda expressions (core) to categorical form
I want to convert lambda expressions into a vocabulary of monoidal categories, so that they can be given multiple interpretations, including circuit generation and timing analysis, and hopefully some other far-out alternatives (3D visualization, animated evaluation, etc). More specifically, I want a GHC plugin that makes this transformation on GHC's Core language. If you know of related work, have suggestions, and/or are interested in collaborating/consulting, I'd love to hear. Thanks, - Conal ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
