Re: [Haskell-cafe] reifying typeclasses (resend)

[Timon Gehr]

On 09/15/2013 09:38 AM, Evan Laforge wrote:

...

It seems to me like I should be able to replace a typeclass with
arbitrary methods with just two, to reify the type and back.  This
seems to work when the typeclass dispatches on an argument, but not on
a return value.  E.g.:

...

Say m_argument and m_result are the ad-hoc methods  I'd like to get out
of the typeclass.  I can do that well enough for 'argument', but
'result' runs into trouble.  One is the ugly undefined trick with
toTaggedType, but the bigger one is that ghc says 'Could not deduce (a
~ Int) from the context (Taggable a)'.  I wasn't really expecting it
to work, because it would entail a case with multiple types.  As far
as I know, the only way for that to happen is with GADTs.  But I don't
see how they could help me here.



As follows:

{-# LANGUAGE GADTs, StandaloneDeriving #-}

class Taggable a where
toTagged :: a -> Tagged a
toTaggedType :: TaggedType a
fromTagged :: Tagged b -> Maybe a

data Tagged a where -- (example works if this is not a GADT)
  TInt  :: Int -> Tagged Int
  TChar :: Char -> Tagged Char

deriving instance Show (Tagged a)

data TaggedType a where
  TypeInt :: TaggedType Int
  TypeChar :: TaggedType Char

deriving instance Show (TaggedType a)

instance Taggable Int where
toTagged = TInt
toTaggedType = TypeInt
fromTagged (TInt x) = Just x
fromTagged _ = Nothing

instance Taggable Char where
toTagged = TChar
toTaggedType = TypeChar
fromTagged (TChar x) = Just x
fromTagged _ = Nothing

argument :: (Taggable a) => a -> Int
argument a = case toTagged a of
TInt x -> x
TChar c -> fromEnum c

result :: (Taggable a) => Int -> a
result val = go val $ toTaggedType
  where
go :: (Taggable a) => Int -> TaggedType a -> a
go val TypeInt = val
go val TypeChar = toEnum val



So, perhaps my intuition was wrong.  toTagged and fromTagged methods
give you the power to go between value and type level,  but apparently
that's not enough power to express what typeclasses give you.


You do get enough power to write that second function, but the result is 
necessarily uglier than if you use GADTs as there are less invariants 
expressed in the type system.


result :: (Taggable a) => Int -> a
result val = case fromTagged (TInt val) of
  Just a -> a
  Nothing -> case fromTagged (TChar $ toEnum val) of
Just a -> a
Nothing -> case error "matches are non-exhaustive" of
  TInt _ -> undefined
  TChar _ -> undefined

(The last pattern match allows the compiler to warn you if 'result' gets 
out of sync with 'Tagged'.)



___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Proposal: New syntax for Haskell

[Timon Gehr]

On 09/10/2013 09:30 AM, Niklas Hambüchen wrote:

Impressed by the productivity of my Ruby-writing friends, I have
recently come across Cucumber: http://cukes.info


It is a great tool for specifying tests and programs in natural
language, and especially easy to learn for beginners.

I propose that we add a Cucumber syntax for Haskell, with the extension
".chs", next to .hs and .lhs.


Code written in cucumber syntax is concise and easy to read: You can
find some example code in https://gist.github.com/nh2/6505995. Quoting
from that:

   Feature: The Data.List module

 In order to be able to use lists
 As a programmer
 I want a module that defines list functions

 Scenario: Defining the function foldl
   Given I want do define foldl
   Which has the type (in brackets) a to b to a (end of brackets),
  to a, to list of b, to a
   And my arguments are called f, acc, and l
   When l is empty
   Then the result better be acc
   Otherwise l is x cons xs
   Then the result should be foldl f (in brackets) f acc x
 (end of brackets) xs


PS: People even already started a testing framework for Haskell in it:
https://github.com/sol/cucumber-haskell#cucumber-for-haskell



The above hardly is an acceptable state of affairs. While I appreciate 
the effort, clearly Cucumber is a rather limited tool and should be 
replaced by something more sophisticated that actually delivers the 
promises of conciseness and being easy to read.


My first shot (this can probably be made even more concise and/or easier 
to read):


Feature: The Data.List module

In order to be able to use lists more conveniently
As a programmer
I want a module that defines some common operations on lists

Scenario: Defining the function 'foldl'
  Given I want to define 'foldl'
  Which whenever given a thing that whenever given a thing of some 
first kind will give a thing that whenever given a thing of some second 
kind will give a thing of the first kind again, will give something that 
whenever given a thing of the first kind will give something that 
whenever given a list containing things of the second kind will give 
something of the first kind.

  When the list is empty
  Then the result better be the aforementioned thing of the first kind
  Otherwise the list has a first thing in it and the remaining things 
form a list again. Then we get the result by giving to 'foldl' the first 
thing mentioned and to the result we give the result we get by giving 
the first thing in the list to the thing we get by giving the thing of 
the first kind to the thing we already gave to 'foldl' and then give to 
what we get the list of remaining things.





___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Alternative name for return

[Timon Gehr]

On 08/08/2013 01:19 AM, Jerzy Karczmarczuk wrote:

Bardur Arantsson comments the comment of Joe Quinn:

>On 8/7/2013 11:00 AM, David Thomas wrote:

>>twice :: IO () -> IO ()
>>twice x = x >> x
>>
>>I would call that evaluating x twice (incidentally creating two
>>separate evaluations of one pure action description), but I'd like to
>>better see your perspective here.

>
>x is only evaluated once, but/executed/  twice. For IO, that means
>magic. For other types, it means different things. For Identity, twice =
>id!
>

Your point being? x is the same thing regardless of how many times you
run it.


What do you mean by "the same thing"? You cannot compare 'them' in any
reasonable sense.
...


http://en.wikipedia.org/wiki/Identity_of_indiscernibles

(He is reasoning _about_ the language and not _within_ the language 
because Haskell does not support very powerful reasoning internally.)



...
You make the distinction between "evaluate",


Which essentially means applying reduction rules to an expression until 
the result is a value.



and  "execute" or "run", etc. This is not functional.


How would you know?


Your program doesn't "run" anything, it
applies (>>=) (or equivalent) to an IO (...) object. This is the only
"practical evaluation" of it, otherwise it can  be passed (or duplicated
as above). But you cannot apply "bind" twice to the same instance of it
(in fact, as I said above, "the same instance"  is a bit suspicious
concept...).
...


Indeed, but you didn't say that above.


The "running" or "execution" takes place outside of your program. In
such a way Richard O'Keefe and I converge... That's why I say that the
concept of purity is meaningless in the discussed context.


Not meaningless, but redundant. The point of having a purely functional 
programming language is to have reasoning based on purity be universally 
applicable.



It is a kind of counterfeit notion, inherited from "pure functions" to something
which belongs to two different worlds.
...


'putStr "c"' is a pure value.

On the other hand:

'unsafePerformIO (putStr "c")' is not a pure value.

(But this expression does not exist in standard Haskell. unsafePerformIO 
"unquotes" the action. You may be confusing the "quoted" and "unquoted" 
versions.)



___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] List Monads and non-determinism

[Timon Gehr]

On 07/20/2013 12:58 AM, Matt Ford wrote:

Hi,

Thanks for the help.

I thought >>= was left associative?  It seems to be in the examples from
Learn You A Haskell.
...


Yes, >>= is left-associative. The associativity of >>= is not relevant 
for your example because no two >>= operations actually occur next to 
each other. The second >>= is part of the lambda occurring as the second 
argument to the first >>=. Lambdas bind 'the rest of the expression'.


[1,2] >>= \n -> [3,4] >>= \m -> return (n,m)

is equivalent to:

let a = [1,2]
b = (\n -> [3,4] >>= \m -> return (n,m))
in a >>= b




I tried to use the associative law to bracket from the right but it
didn't like that either...

[1,2] >>= (\x -> (\n -> [3,4])) x  >>= \m -> return (n,m))

Any thoughts?
...


Where does that 'x' come from?


___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] List Monads and non-determinism

[Timon Gehr]

On 07/20/2013 12:23 AM, Matt Ford wrote:

Hi All,

I thought I'd have a go at destructing

[1,2] >>= \n -> [3,4] >>= \m -> return (n,m)

which results in [(1,3)(1,4),(2,3),(2,4)]

I started by putting brackets in

([1,2] >>= \n -> [3,4]) >>= \m -> return (n,m)
...


This is not the same expression any more. See below for the correct 
bracketing.



This immediately fails when evaluated: I expect it's something to do
with the n value now not being seen by the final return.

It seems to me that the return function is doing something more than
it's definition (return x = [x]).

If ignore the error introduced by the brackets I have and continue to
simplify I get.

[3,4,3,4] >>= \m -> return (n,m)

Now this obviously won't work as there is no 'n' value.  So what's
happening here? Return seems to be doing way more work than lifting the
result to a list, how does Haskell know to do this?  Why's it not in the
function definition?  Are lists somehow a special case?

Any pointers appreciated.
...



[1,2] >>= (\n -> [3,4] >>= (\m -> return (n,m)))

~>*

((\n -> [3,4] >>= (\m -> return (n,m))) 1) ++ ((\n -> [3,4] >>= (\m -> 
return (n,m))) 2)


~>*

([3,4] >>= (\m -> return (1,m))) ++ ([3,4] >>= (\m -> return (2,m)))

~>*

((\m -> return (1,m)) 3 ++ (\m -> return (1,m)) 4) ++ ((\m -> return 
(2,m)) 3 ++ (\m -> return (2,m)) 4)


~>*

return (1,3) ++ return (1,4) ++ return (2,3) ++ return (2,4)

~>*

[(1,3)] ++ [(1,4)] ++ [(2,3)] ++ [(2,4)]

~>*

[(1,3),(1,4),(2,3),(2,4)]

Where the definition return x = [x] has been applied in the second-last 
step.







___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Proposal: Non-recursive let

[Timon Gehr]

On 07/11/2013 08:37 AM, AntC wrote:

 okmij.org> writes:
...
In Haskell I'll have to uniquely number the s's:

 let (x,s1)  = foo 1 [] in
 let (y,s2)  = bar x s1 in
 let (z,s3)  = baz x y s2 in ...

and re-number them if I insert a new statement.

I once wrote about 50-100 lines of code with the fragment like the
above and the only problem was my messing up the numbering (at one
place I used s2 where I should've used s3). ...


Oleg, I hope you are not saying that in production code you use names like
x, y, z, s1, s2, s3, s4, ...



Depending on context, those can be perfectly good names, modulo the 
numbering. I'd be more worried about 'foo', 'bar', 'baz'. :o)



It leads to opaque code.


Questionable. Typically there tends to be more relevant information in 
the name of an arrow than in the name of a point, with the arrows 
connecting the points and thus clarifying their meaning.



If even you can mess up, what hope for us with only nano-Oleg brain capacity?



Non-recursive let.


(On a less tongue-in-cheek note, IMHO, assuming that there is something 
like a constant 'brain capacity' significantly varying between persons 
that limits how well one can master a certain discipline is a good start 
for painting oneself into a corner.)



Next you'll be wanting GOTO  and destructive assignment.



Unlikely. Haskell already has constructs which are more expressive than 
goto and destructive assignment, without requiring the language to give 
up the benefits of the absence of those features in direct code.



Who knows: one day somebody modifying your code might need to insert a
line. (That 'somebody' might be your future self.)



(That was part of his point.)


Just don't do that! Use long_and_meaningful names.



'meaningful' is long enough.


50-100 near-identical lines of code sounds like an opportunity for an
algorithm.
...


He expressed that he wrote 50-100 lines of code containing such a short 
fragment and the only problem was inside that fragment. Since the goal 
of that anecdote presumably was to establish the relevance of a pitfall 
that a non-recursive let would make less severe, I think this is a more 
natural way to interpret the only slightly ambiguous wording.



___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Comparing functions

[Timon Gehr]

On 07/11/2013 07:33 PM, Vlatko Basic wrote:

Hello Cafe,

I have

 data CmpFunction a = CF (a -> a -> Bool)

that contains comparing functions, like ==, <, > ..., and I'm trying to
declare the Show instance for it like this

 instance Show (CmpFunction a) where
   show (CF (==)) = "== "   -- no good
   show f = case f of-- no good also
CBF (==) -> "=="
 _ -> "Other"

but compiler complains for both with

This binding for `==' shadows the existing binding
imported from `Prelude' at src/Main.hs:6:8-11
(and originally defined in `ghc-prim:GHC.Classes')



Yes, (==) is a variable name in a pattern. Hence you are creating a new 
definition for (==) bound to the constructor argument to CF, which hides 
the (==) defined within the Eq type class.



Is it possible at all to compare two functions


Function types are opaque and values do not have an identity.


or how to solve this problem, to show some string for a specific function?


br,
vlatko


You could store the string alongside the function inside the data type 
in some way.



___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Lambda Calculus question on equivalence

[Timon Gehr]

On 05/02/2013 11:37 PM, Edward Z. Yang wrote:

Excerpts from Timon Gehr's message of Thu May 02 14:16:45 -0700 2013:

Those are not lambda terms.
Furthermore, if those terms are rewritten to operate on church numerals,
they have the same unique normal form, namely λλλ 3 2 (3 2 1).


The trick is to define the second one as x * 2 (and assume the fixpoint
operates on the first argument). Now they are not equal.

Edward



Neither equal nor extensionally equivalent.

mult = λm.λn.λf. n (m f)

mult 2 = λn.λf. n (2 f)

mult 2 = λn.λf. n (λx. f (f x))

flip mult 2 = λm.λf. 2 (m f)

flip mult 2 = λm.λf.λx. m f (m f x)


(λn.λf. n (λx. f (f x)) const = λf. const (λx. f (f x))
  = λf.λa.λx. f (f x)

This is clearly not the same as:

(λm.λf.λx. m f (m f x)) const = λf.λx. f


___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Lambda Calculus question on equivalence

[Timon Gehr]

On 05/02/2013 11:33 PM, Francesco Mazzoli wrote:

At Thu, 02 May 2013 23:16:45 +0200,
Timon Gehr wrote:

Yes, they can.  Take ‘f = λ x : ℕ → x + x’ and ‘g = λ x : ℕ → 2 * x’.

Those are not lambda terms.


How are they not lambda terms?



I guess if + and * are interpreted as syntax sugar then they are lambda 
terms with free variables. In this case, they are not equivalent.



Furthermore, if those terms are rewritten to operate on church numerals,
they have the same unique normal form, namely λλλ 3 2 (3 2 1).


You are assume things about the implementation of natural numbers, of *, and +
(admittedly they were underspecified on my side :).  They could be implemented
in different way, or I could simply change the second definition to ‘λ x → x *
2’, in which case execution would be stuck on the abstract variable.



AFAICS this does not show anything either, as the terms λλλ 3 2 (3 2 1) 
and λλ 2 (λ 2 (2 1)) are not extensionally equivalent. (since their 
domain is not restricted to terms corresponding to church numerals. Eg. 
feed them λλ 2.)



In any case, definitionally different functions can be extensionally equal,
there is little doubt on that.


These terms are not ‘definitionally’ equal (which could be the α-equivalence 
you cite
but can be extended to fancier checks on the term structure).  However, for all
(well typed)  inputs the result of those two functions are the same: they are
‘extensionally’ equal [1].  The first part (...(L A) is equivalent to (L B)...)
holds: the same function will always produce the same output given
definitionally equal arguments.
...


(I guess the question is about untyped lambda calculus.)


I don’t think so, since Ian talked about ‘terminating’ λ-calculus, while
the untyped λ-calculus isn’t...


'terminating' does not occur in the original post.


otherwise you can’t normalise and compare.
...


The terms in question are already normalised.


___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Lambda Calculus question on equivalence

[Timon Gehr]

On 05/02/2013 10:42 PM, Francesco Mazzoli wrote:

At Thu, 02 May 2013 20:47:07 +0100,
Ian Price wrote:

I know this isn't perhaps the best forum for this, but maybe you can
give me some pointers.

Earlier today I was thinking about De Bruijn Indices, and they have the
property that two lambda terms that are alpha-equivalent, are expressed
in the same way, and I got to wondering if it was possible to find a
useful notion of function equality, such that it would be equivalent to
structural equality (aside from just defining it this way), though
obviously we cannot do this in general.

So the question I came up with was:

Can two normalised (i.e. no subterm can be beta or eta reduced) lambda
terms be "observationally equivalent", but not alpha equivalent?

By observationally equivalent, I mean A and B are observationally
equivalent if for all lambda terms L: (L A) is equivalent to (L B) and
(A L) is equivalent to (B L). The definition is admittedly circular, but
I hope it conveys enough to understand what I'm after.

My intuition is no, but I am not sure how to prove it, and it seems to
me this sort of question has likely been answered before.


Yes, they can.  Take ‘f = λ x : ℕ → x + x’ and ‘g = λ x : ℕ → 2 * x’.


Those are not lambda terms.
Furthermore, if those terms are rewritten to operate on church numerals, 
they have the same unique normal form, namely λλλ 3 2 (3 2 1).



These terms are not ‘definitionally’ equal (which could be the α-equivalence 
you cite
but can be extended to fancier checks on the term structure).  However, for all
(well typed)  inputs the result of those two functions are the same: they are
‘extensionally’ equal [1].  The first part (...(L A) is equivalent to (L B)...)
holds: the same function will always produce the same output given
definitionally equal arguments.
...


(I guess the question is about untyped lambda calculus.)


___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] unsafeInterleaveST (and IO) is really unsafe

[Timon Gehr]

On 04/12/2013 10:24 AM, o...@okmij.org wrote:


Timon Gehr wrote:

I am not sure that the two statements are equivalent. Above you say that
the context distinguishes x == y from y == x and below you say that it
distinguishes them in one possible run.


I guess this is a terminological problem.


It likely is.


The phrase `context
distinguishes e1 and e2' is the standard phrase in theory of
contextual equivalence. Here are the nice slides
 http://www.cl.cam.ac.uk/teaching/0910/L16/semhl-15-ann.pdf



The only occurrence of 'distinguish' is in the Leibniz citation.


Please see adequacy on slide 17. An expression relation between two
boolean expressions M1 and M2 is adequate if for all program runs (for
all initial states of the program s), M1
evaluates to true just in case M2 does. If in some circumstances M1
evaluates to true but M2 (with the same initial state) evaluates to
false, the expressions are not related or the expression relation is
inadequate.



In my mind, 'evaluates-to' is an existential statement. The adequacy 
notion given there is inadequate if the program execution is 
indeterministic, as I would have expected it to be in this case. (They 
quickly note this on slide 18, giving concurrency features as an example.)



See also the classic
 http://www.ccs.neu.edu/racket/pubs/scp91-felleisen.ps.gz
(p11 for definition and Theorem 3.8 for an example of a
distinguishing, or witnessing context).



Thanks for the pointer, I will have a look. However, it seems that the 
semantics the definition and the proof rely on are deterministic?



In essence, lazy IO provides unsafe constructs that are not named
accordingly. (But IO is problematic in any case, partly because it
depends on an ideal program being run on a real machine which is based
on a less general model of computation.)


I'd agree with the first sentence. As for the second sentence, all
real programs are real programs executing on real machines. We may
equationally prove (at time Integer) that
 1 + 2^10 == 2^10 + 1
but we may have trouble verifying it in Haskell (or any other
language). That does not mean equational reasoning is useless: we just
have to precisely specify the abstraction boundaries.


Which is really hard. I think equational reasoning is helpful because it 
is valid for ideal programs and it seems therefore to be a good 
heuristic for real ones.



BTW, the
equality above is still useful even in Haskell: it says that if the
program managed to compute 1 + 2^10 and it also managed to compute
2^10 + 1, the results must be the same. (Of course in the above
example, the program will probably crash in both cases).  What is not
adequate is when equational theory predicts one finite result, and the
program gives another finite result -- even if the conditions of
abstractions are satisfied (e.g., there is no IO, the expression in
question has a pure type, etc).



The abstraction bound is where exact reasoning necessarily stops.


I think this context cannot be used to reliably distinguish x == y and y
== x. Rather, the outcomes would be arbitrary/implementation
defined/undefined in both cases.


My example uses the ST monad for a reason: there is a formal semantics
of ST (denotational in Launchbury and Peyton-Jones and operational in
Moggi and Sabry). Please look up ``State in Haskell'' by Launchbury
and Peyton-Jones. The semantics is explained in Sec 6.


InterleaveST is first referred to in chapter 10. As far as I can tell, 
the construct does not have specified a formal semantics.



Please see Sec
10.2 Unique supply trees -- you might see some familiar code. Although
my example was derived independently, it has the same kernel of
badness as the example in Launchbury and Peyton-Jones. The authors
point out a subtlety in the code, admitting that they fell into the
trap themselves.


They informally note that the final result depends on the order of 
evaluation and is therefore not always uniquely determined. (because the 
order of evaluation is only loosely specified.)



So, unsafeInterleaveST is really bad -- and the
people who introduced it know that, all too well.



I certainly do not disagree that it is bad. However, I am still not 
convinced that the example actually shows a violation of equational 
reasoning. The valid outputs, according to the informal specification in 
chapter 10, are the same for both expressions.



___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] unsafeInterleaveST (and IO) is really unsafe [was: meaning of "referential transparency"]

[Timon Gehr]

On 04/10/2013 04:45 AM, o...@okmij.org wrote:


...

And yet there exists a context that distinguishes x == y from y ==x.
That is, there exists
 bad_ctx :: ((Bool,Bool) -> Bool) -> Bool
such that

 *R> bad_ctx $ \(x,y) -> x == y
 True
 *R> bad_ctx $ \(x,y) -> y == x
 False



I am not sure that the two statements are equivalent. Above you say that 
the context distinguishes x == y from y == x and below you say that it 
distinguishes them in one possible run.



The function unsafeInterleaveST ought to bear the same stigma as does
unsafePerformIO. After all, both masquerade side-effecting
computations as pure.


Potentially side-effecting computations. There are non-side-effecting 
uses of unsafePerformIO and unsafeInterleaveST, but verifying this is 
outside the reach of the type checker. If they have observable 
side-effects, I'd say the type system has been broken and it does not 
make sense to have a defined language semantics for those cases.



Hopefully even lazy IO will get
recommended less, and with more caveats. (Lazy IO may be
superficially convenient -- so are the absence of typing discipline and
the presence of unrestricted mutation, as many people in
Python/Ruby/Scheme etc worlds would like to argue.)



In essence, lazy IO provides unsafe constructs that are not named 
accordingly. (But IO is problematic in any case, partly because it 
depends on an ideal program being run on a real machine which is based 
on a less general model of computation.)



The complete code:

module R where

import Control.Monad.ST.Lazy (runST)
import Control.Monad.ST.Lazy.Unsafe (unsafeInterleaveST)
import Data.STRef.Lazy

bad_ctx :: ((Bool,Bool) -> Bool) -> Bool
bad_ctx body = body $ runST (do
r <- newSTRef False
x <- unsafeInterleaveST (writeSTRef r True >> return True)
y <- readSTRef r
return (x,y))


t1 = bad_ctx $ \(x,y) -> x == y
t2 = bad_ctx $ \(x,y) -> y == x




I think this context cannot be used to reliably distinguish x == y and y 
== x. Rather, the outcomes would be arbitrary/implementation 
defined/undefined in both cases.



___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Object Oriented programming for Functional Programmers

[Timon Gehr]

On 01/02/2013 11:19 PM, MigMit wrote:


On Jan 3, 2013, at 2:09 AM, Gershom Bazerman  wrote:


On 1/2/13 4:29 PM, MigMit wrote:



BTW. Why you think that Eiffel type system is unsafe?

Well, if I remember correctly, if you call some method of a certain object, and 
this call compiles, you can't be certain that this object actually has this 
method. Could be that this object belongs to some subclass which removes this 
method.



Eiffel doesn't handle the relationship of co- and contra-variance of arguments with 
subtyping in a principled way. This is apparently known as the "catcall" 
problem. See, e.g., this article: http://www.eiffelroom.org/node/517


Yes, variance is another big source of unsafety, that's for sure. And another reason I think there 
is no real "theory" behind Eiffel, just a bunch of features (or "concepts") 
boiled together.



There seem to be efforts to fix this:
http://tecomp.sourceforge.net/index.php?file=doc/papers/proof/

The resulting language appears to be type safe:
http://tecomp.sourceforge.net/index.php?file=doc/papers/lang/modern_eiffel.txt#chapter_20




___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Object Oriented programming for Functional Programmers

[Timon Gehr]

On 01/03/2013 10:56 AM, Alberto G. Corona wrote:

Anyway, Type checking is essentially an application of set theory : (I
did no search in te literature for this, It is just my perception).


Not exactly. Type theory is not an application of set theory, it is an 
alternative to set theory.



When
I say   (+) :: Num a => a -> a -> a . I mean that (+) takes two elements
of the set of Num typeclass and return another.


If I get this right, you consider Num to be a set, and then its 
inhabitants would need to be be types, thus this describes a type-level 
mapping.

This is a more accurate description, (but there might be a better one):

(+) : (a : Type)->(i : (Num a : Prop))->(x : a)->(y : a)->(z : a)

(+) is a mapping from types 'a' to mappings from proofs 'i' of the 
proposition that 'a' is an instance of the 'Num' type class to a curried 
function that takes two arguments of type 'a' and produces a result of 
type 'a'.



This is in principle a
weak restriction, because many functions do it as well, for example (*).

A propery check or a contract would be much more restrictive and thus
would detect much more program errors. But it seems that no other
language but haskell took this set theoretical analysis so exhaustively,


There are quite a few that take it further than Haskell.

http://wiki.portal.chalmers.se/agda/pmwiki.php



and without it, a property check is like detecting microscopic cracks in
nuclear waste vessel without first making sure that the cover has been
sealed.




___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Fwd: Object Oriented programming for Functional Programmers

[Timon Gehr]

On 12/30/2012 10:57 PM, Eli Frey wrote:

sorry, forgot to reply-all

-- Forwarded message --
From: *Eli Frey* mailto:eli.lee.f...@gmail.com>>
Date: Sun, Dec 30, 2012 at 1:56 PM
Subject: Re: [Haskell-cafe] Object Oriented programming for Functional
Programmers
To: Brandon Allbery mailto:allber...@gmail.com>>


 > Except not quite... [...] It's not a built in table, it's a hidden
parameter.

I'll admit this doesn't HAVE to be the implementation.  Often time the
compiler can monomorphise the types and "perform the lookup" at compile
time.

But what's going on here tho.

 > {-# LANGUAGE ExistentialQuantification #-}
 >  data Showable = forall a. Show a => Showable a
 >
 > printShowable :: Showable -> IO ()
 > printShowable (Showable x) = print x
 >
 >  main = mapM printShowable [ Showable "bob", Showable 3, Showable
Nothing ]

If we take `mapM printShowable` and just give it an arbitrary list, it
has to lookup the correct implementations of `print` as it walks down
that list at run-time.  I believe similar things motivate vtables in
c++/java.  I don't have a strong intuition about how dynamically typed
OO langs deal with this, but I'm sure structural typing has similar issues.

...


The Showable constructor has two parameters. The 'Show' instance for 'a' 
(passed implicitly) and an 'a' (passed explicitly). When pattern 
matching, that instance gets unwrapped together with the payload. It is 
then implicitly passed to 'print', which finally uses it to look up the 
correct implementation of 'show'.




___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] How to fold on types?

[Timon Gehr]

On 12/25/2012 09:59 AM, Magicloud Magiclouds wrote:

Say I have things like:

data LongDec = LongDef a b c ... x y z
values = [ 'a', 'b', 'c', ... 'x', 'y', 'z' ]

Now I want them to be "LongDef 'a' 'b' 'c' ... 'x' 'y' 'z'".
In form, this is something like folding. But since the type changes, so
code like following won't work:

foldl (\def value -> def value) LongDef values

Is it possible to do this in some way?
--
竹密岂妨流水过
山高哪阻野云飞

And for G+, please use magiclouds#gmail.com .


___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe



This hack works, in case that helps:

{-# LANGUAGE FlexibleInstances, MultiParamTypeClasses #-}

data LongDec = LongDef Char Char Char Char Char Char
  deriving Show

values = [ 'a', 'b', 'c', 'x', 'y', 'z' ]

class Apply a b c where
  apply :: b -> [a] -> c
instance Apply a b b where
  apply = const
instance (Apply a b c) => Apply a (a -> b) c where
  apply f (x:xs) = apply (f x) xs

main = print (apply LongDef values :: LongDec)

It requires an explicit type annotation to fix type parameter 'c'. It 
cannot be a function type. (I am not sure why though.)



___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe