Am Dienstag, 17. März 2009 21:51 schrieben Sie:
On Tue, Mar 17, 2009 at 6:14 AM, Wolfgang Jeltsch wrote:
Am Dienstag, 17. März 2009 11:49 schrieb Yandex:
data (a :=: a') where
Refl :: a :=: a
Comm :: (a :=: a') - (a' :=: a)
Trans :: (a :=: a') - (a' :=: a'') - (a :=: a'')
I use these defs:
-- | Lift proof through a unary type constructor
liftEq :: a :=: a' - f a :=: f a'
liftEq Refl = Refl
-- | Lift proof through a binary type constructor (including '(,)')
liftEq2 :: a :=: a' - b :=: b' - f a b :=: f a' b'
liftEq2 Refl Refl = Refl
-- | Lift proof through a
Hi
On 18 Mar 2009, at 15:00, Conal Elliott wrote:
I use these defs:
-- | Lift proof through a unary type constructor
liftEq :: a :=: a' - f a :=: f a'
liftEq Refl = Refl
-- | Lift proof through a binary type constructor (including '(,)')
liftEq2 :: a :=: a' - b :=: b' - f a b :=: f a' b'
Olá café,
With the recent generic programming work and influences from
type-dependent languages such as Agda, the following data type seems to
come up often:
data (a :=: a') where
Refl :: a :=: a
Everyone who needs it writes their own version; I'd like to compile a
package with this
data (a :=: a') where
Refl :: a :=: a
Comm :: (a :=: a') - (a' :=: a)
Trans :: (a :=: a') - (a' :=: a'') - (a :=: a'')
Martijn van Steenbergen wrote:
Olá café,
With the recent generic programming work and influences from
type-dependent languages such as Agda, the following data type seems
Am Dienstag, 17. März 2009 11:49 schrieb Yandex:
data (a :=: a') where
Refl :: a :=: a
Comm :: (a :=: a') - (a' :=: a)
Trans :: (a :=: a') - (a' :=: a'') - (a :=: a'')
I don’t think, Comm and Trans should go into the data type. They are not
axioms but can be proven. Refl says that each
On Tue, Mar 17, 2009 at 11:39:05AM +0100, Martijn van Steenbergen wrote:
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeOperators #-}
module Eq where
data (a :=: a') where
Refl :: a :=: a
class Eq1 f where
eq1 :: f a - f a' - Maybe (a :=: a')
class Eq2 f where
eq2 :: f a b - f a' b' -
On Tue, Mar 17, 2009 at 10:30 AM, Brent Yorgey byor...@seas.upenn.edu wrote:
I don't understand your classes Eq1, Eq2, and Eq3. How would you make
an instance of Eq1 for, say, [] ?
You don't.
It seems you are confusing _value_ equality with _type_ equality? A
value of type a :=: a' is a
On Tue, Mar 17, 2009 at 6:14 AM, Wolfgang Jeltsch
g9ks1...@acme.softbase.org wrote:
Am Dienstag, 17. März 2009 11:49 schrieb Yandex:
data (a :=: a') where
Refl :: a :=: a
Comm :: (a :=: a') - (a' :=: a)
Trans :: (a :=: a') - (a' :=: a'') - (a :=: a'')
I don’t think, Comm and
2009/3/17 Luke Palmer lrpal...@gmail.com:
Here are the original definition and the proofs of comm and trans.
Compiles
fine with GHC 6.10.1.
data (a :=: a') where
Refl :: a :=: a
comm :: (a :=: a') - (a' :=: a)
comm Refl = Refl
trans :: (a :=: a') - (a' :=: a'') - (a
Hi
On 17 Mar 2009, at 21:06, David Menendez wrote:
2009/3/17 Luke Palmer lrpal...@gmail.com:
Here are the original definition and the proofs of comm and trans.
Compiles
fine with GHC 6.10.1.
data (a :=: a') where
Refl :: a :=: a
comm :: (a :=: a') - (a' :=: a)
comm Refl =
Ryan Ingram wrote:
These types are very useful for construction of type-safe interpreters
and compilers.
That's exactly what I have in mind.
In my specific case I want to compare the constructors of the GADT
representing a datatype family in the multirec package:
data AST a where
Stmt
Conor McBride wrote:
instance Category (:=:) where
id = Refl
Refl . Refl = Refl
That and the identity-on-objects functor to sets and
functions.
Not sure what you mean by this, Conor. Can you please express this in
Haskell code?
Thanks,
Martijn.
Martijn van Steenbergen wrote:
class Eq2 f where
eq2 :: f a b - f a' b' - Maybe (a :=: a', b :=: b')
Is that right, or does the following make more sense?
class Eq2 f where
eq2 :: f a b - f a' b' - (Maybe (a :=: a'), Maybe (b :=: b'))
Thanks,
Martijn.
On 17 Mar 2009, at 21:44, Martijn van Steenbergen wrote:
Conor McBride wrote:
instance Category (:=:) where
id = Refl
Refl . Refl = Refl
That and the identity-on-objects functor to sets and
functions.
Not sure what you mean by this, Conor. Can you please express this
in Haskell code?
15 matches
Mail list logo
