
On Tue, Dec 20, 2011 at 3:10 PM, Chris Wong
On Wed, Dec 21, 2011 at 10:53 AM, Matthew Farkas-Dyck
wrote: With GHC 7.0.3:
$ cat test.hs class ℝ a where { test :: a; };
(∈) :: Eq a => a -> [a] -> Bool; x ∈ (y:ys) = x == y || x ∈ ys;
main = putStrLn "Two of three ain't bad (^_~)"; $ runhaskell test.hs Two of three ain't bad (^_~) $
Why not expand it even further?
My experience with Agda makes me think that extending it further can make it painful to program in. Initially I thought that using unicode symbols would just make input a bit slower and that editor support could address that. You know, like writing about math using latex. My actual experience with Agda was different than that. I was using Emacs and I found that I needed to make my font size very large to see all the detail of the unicode symbols clearly enough to distinguish between them fully. The alternative was using the support in emacs for displaying the codepoint, as a number, for any glyph I wanted to distinguish. Perhaps it's still "just an issue of editor support" but it left a sour taste in my mouth. Jason