On Dec 23, 2005, at 11:53, Arjen wrote:
On Fri, 23 Dec 2005, Joel Reymont wrote:
Folks,
I have been looking at the code for the Arrows for invertible
programming paper (http://www.cs.ru.nl/A.vanWeelden/bi-arrows/) and
I have a question about syntax. ghci surely does not like it.
I've
Folks,
I have been looking at the code for the Arrows for invertible
programming paper (http://www.cs.ru.nl/A.vanWeelden/bi-arrows/) and
I have a question about syntax. ghci surely does not like it.
What does this mean and how do I make it compile?
mapl{|a, b|arr|} :: (mapl{|a, b|arr|},
What does this mean and how do I make it compile?
mapl{|a, b|arr|} :: (mapl{|a, b|arr|}, ArrowChoice arr, BiArrow arr) = arr a
b
It's Generic Haskell source code, see
http://www.generic-haskell.org/
Generic Haskell is an extension of Haskell that supports generic programming.
Is this something that can be compiled with GHC right now? I noticed -
fgenerics but I think it does something else entirely.
On Dec 23, 2005, at 8:52 AM, Ralf Hinze wrote:
It's Generic Haskell source code, see
http://www.generic-haskell.org/
Generic Haskell is an extension of
Is this something that can be compiled with GHC right now? I noticed -
fgenerics but I think it does something else entirely.
GH is a pre-compiler that takes GH code to Haskell code,
so this is a two-step process. -fgenerics turns derivable
type classes on (see Derivable type classes, Ralf
On Fri, 23 Dec 2005, Joel Reymont wrote:
Folks,
I have been looking at the code for the Arrows for invertible
programming paper (http://www.cs.ru.nl/A.vanWeelden/bi-arrows/) and
I have a question about syntax. ghci surely does not like it.
I've updated the web page to say that is does not
G |- f :: all x::S . T G |- s :: S
--
G |- f s :: [s/x]T
Any more takers? I still don't have any pointers to literature where
this theorem notation is explained more fully, and I'd
Juan Carlos Arevalo Baeza wrote (on 28-05-01 18:02 -0700):
Just a very naive question, because I'm really curious. I've seen in
previous messages here discussions about type systems using this kind of
notation:
G |- f :: all x::S . T G |- s :: S
and not just type systems but also other aspects of operational
semantics. What we have here is a single rule from a rule-based
inductive definition of a certain relation G |- s :: S between typing
environments G, expressions s and types S.
It's probably worth mentioning here that this
Another introduction, with emphasis on the historical development:
Philip Wadler, Proofs are Programs: 19th Century Logic and 21st
Century Computing.
http://www.cs.bell-labs.com/who/wadler/topics/history.html
It's a fun read, too.
Cheers,
Tom
Just a very naive question, because I'm really curious. I've seen in
previous messages here discussions about type systems using this kind of
notation:
G |- f :: all x::S . T G |- s :: S
--
G |- f s :: [s/x]T
I'd never seen it before,
On Mon, 28 May 2001, Juan Carlos Arevalo Baeza wrote:
Just a very naive question, because I'm really curious. I've seen in
previous messages here discussions about type systems using this kind of
notation:
G |- f :: all x::S . T G |- s :: S
At 09:24 PM 5/28/2001 -0400, Mark Carroll wrote:
G |- f :: all x::S . T G |- s :: S
--
G |- f s :: [s/x]T
I'm far from the right person to have a go, but while we're waiting for
someone who knows what they're talking about:
:) Thanx.
- Original Message -
From: Juan Carlos Arevalo Baeza [EMAIL PROTECTED]
To: [EMAIL PROTECTED]
Sent: Tuesday, May 29, 2001 11:02 AM
Subject: Notation question
Just a very naive question, because I'm really curious. I've seen in
previous messages here discussions about type systems
14 matches
Mail list logo
