Sub class and model expansion

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
6 messages Options
Reply | Threaded
Open this post in threaded view
|

Sub class and model expansion

Patrick Browne
Hi,
I'm not sure if this is possible but I am trying to use Haskell’s type
class to specify  *model expansion*. Model expansion allows the
specification of new symbols (known as enrichment) or the specification
further properties that should hold on old symbols. I am trying to
enrich simplified Monoids to Groups. The code below is not intended to
do anything other than to specify simplified Groups as a subclass of
Monoid. The main problem is that I cannot use ! on the LHS of equations
in Group.

Is it possible to expand the specification of Monoid to Group using
Haskell type classes?

Pat



data M = M deriving Show

-- Monoid with one operation (!) and identity e (no associativity)
class Monoid  a where
  (!)  ::  a -> a -> a
  e :: a
  a ! e = a


-- A  Group is a Monoid with an inverse, every Group is a Monoid
-- (a necessary condition in logic: Group implies Monoid)
-- The inverse property could be expressed as:
--      1) forAll a thereExists b such that a ! b = e
--      2)  (inv a) ! a  =  e
class Monoid a => Group a where
  inverse  ::  a -> a
-- Haskell does not like  ! on the LHS of equation for inverse in Group.
--  (inverse a) ! a  = e

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
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Sub class and model expansion

Ryan Ingram
Hi Patrick.

What you are doing isn't possible in source code (Haskell doesn't prove things at the value level like a dependently typed language does.)

Usually you document it just as you have, as a comment

    -- inverse a ! a = e

You can also specify a QuickCheck property:

propInverse :: (Eq a, Group a) => a -> Bool
propInverse a = (inverse a ! a) == e

I've put up an example on hpaste at http://hpaste.org/47234/simple_monoid

  -- ryan

On Sat, May 28, 2011 at 2:46 AM, Patrick Browne <[hidden email]> wrote:
Hi,
I'm not sure if this is possible but I am trying to use Haskell’s type
class to specify  *model expansion*. Model expansion allows the
specification of new symbols (known as enrichment) or the specification
further properties that should hold on old symbols. I am trying to
enrich simplified Monoids to Groups. The code below is not intended to
do anything other than to specify simplified Groups as a subclass of
Monoid. The main problem is that I cannot use ! on the LHS of equations
in Group.

Is it possible to expand the specification of Monoid to Group using
Haskell type classes?

Pat



data M = M deriving Show

-- Monoid with one operation (!) and identity e (no associativity)
class Monoid  a where
 (!)  ::  a -> a -> a
 e :: a
 a ! e = a


-- A  Group is a Monoid with an inverse, every Group is a Monoid
-- (a necessary condition in logic: Group implies Monoid)
-- The inverse property could be expressed as:
--      1) forAll a thereExists b such that a ! b = e
--      2)  (inv a) ! a  =  e
class Monoid a => Group a where
 inverse  ::  a -> a
-- Haskell does not like  ! on the LHS of equation for inverse in Group.
--  (inverse a) ! a  = e

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
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe


_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Sub class and model expansion

Patrick Browne
Ryan,
Thank you for your helpful reply.
I have no real understanding of dependent types (DT)
From the web is seems that DTs are types that depend on *values*.
How does the concept of DT relate to the equation from my example?

>>     -- inverse a ! a = e

What type is depending on what value?

Once again thanks for time and insight.
Pat


On 29/05/2011 22:45, Ryan Ingram wrote:

> Hi Patrick.
>
> What you are doing isn't possible in source code (Haskell doesn't prove
> things at the value level like a dependently typed language does.)
>
> Usually you document it just as you have, as a comment
>
>     -- inverse a ! a = e
>
> You can also specify a QuickCheck property:
>
> propInverse :: (Eq a, Group a) => a -> Bool
> propInverse a = (inverse a ! a) == e
>
> I've put up an example on hpaste at http://hpaste.org/47234/simple_monoid
>
>   -- ryan
>
> On Sat, May 28, 2011 at 2:46 AM, Patrick Browne <[hidden email]
> <mailto:[hidden email]>> wrote:
>
>     Hi,
>     I'm not sure if this is possible but I am trying to use Haskell’s type
>     class to specify  *model expansion*. Model expansion allows the
>     specification of new symbols (known as enrichment) or the specification
>     further properties that should hold on old symbols. I am trying to
>     enrich simplified Monoids to Groups. The code below is not intended to
>     do anything other than to specify simplified Groups as a subclass of
>     Monoid. The main problem is that I cannot use ! on the LHS of equations
>     in Group.
>
>     Is it possible to expand the specification of Monoid to Group using
>     Haskell type classes?
>
>     Pat
>
>
>
>     data M = M deriving Show
>
>     -- Monoid with one operation (!) and identity e (no associativity)
>     class Monoid  a where
>      (!)  ::  a -> a -> a
>      e :: a
>      a ! e = a
>
>
>     -- A  Group is a Monoid with an inverse, every Group is a Monoid
>     -- (a necessary condition in logic: Group implies Monoid)
>     -- The inverse property could be expressed as:
>     --      1) forAll a thereExists b such that a ! b = e
>     --      2)  (inv a) ! a  =  e
>     class Monoid a => Group a where
>      inverse  ::  a -> a
>     -- Haskell does not like  ! on the LHS of equation for inverse in Group.
>     --  (inverse a) ! a  = e
>
>     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
>     [hidden email] <mailto:[hidden email]>
>     http://www.haskell.org/mailman/listinfo/haskell-cafe
>
>


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
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Sub class and model expansion

Brandon Moore-2
> From: Patrick Brown; Sent: Sunday, May 29, 2011 5:42 PM

> Subject: Re: [Haskell-cafe] Sub class and model expansion
>
> Ryan,
> Thank you for your helpful reply.
> I have no real understanding of dependent types (DT)
> From the web is seems that DTs are types that depend on *values*.
> How does the concept of DT relate to the equation from my example?
>
>>>      -- inverse a ! a = e
>
> What type is depending on what value?

You want part of the group interface to be a proof
that your inverse function agrees property with the
monoid operation and unit.

If that's going to be a value, it has to have some type.
If that type is anything like "Proof that inverse a ! a = e",
then the type mentions, or "depends on" the values
inverse, (!), and e.

You can see exactly this in the Agda standard library,
in the definitions IsMonoid and IsGroup in
Algebra.Structures, which define records containing
proofs that a set of operations actually forms a monoid
or group.


You could probably avoid the apparent circularity
of full dependent types if you split up a language
into values which can have types, and a separate
pair of propositions and proofs which can refer to
values and types, but not to themselves.

I think that's basically the organization of any system
where you use a separate prover to prove things about
programs in some previously-existing programming
language, but I haven't stumbled across any examples
where that sort of organization was designed into
a single language from the start.


Brandon


_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Sub class and model expansion

Patrick Browne
Continuing the thread on model expansion.
I have changed the example trying to focus on expanding models of M in G
Why is the operation ! ok or RHS but not visible on LHS of G?
The equation itself does not seem to suffer from the dependent type
problem of my previous post.

class M a where
 (!)  ::  a -> a -> a
 e :: a


class M a => G a where
 (!-)  ::  a -> a -> a
-- OK in G
 a !- e = e ! a

-- Switching LHS/RHS is not OK in G but fine in S
--  if I declare both ! and !- in S
-- ! is not a (visible) method of class `G'
-- a ! e = e !- a


Thanks,
Pat







On 30/05/2011 00:47, Brandon Moore wrote:

>> From: Patrick Brown; Sent: Sunday, May 29, 2011 5:42 PM
>
>> Subject: Re: [Haskell-cafe] Sub class and model expansion
>>
>> Ryan,
>> Thank you for your helpful reply.
>> I have no real understanding of dependent types (DT)
>> From the web is seems that DTs are types that depend on *values*.
>> How does the concept of DT relate to the equation from my example?
>>
>>>>      -- inverse a ! a = e
>>
>> What type is depending on what value?
>
> You want part of the group interface to be a proof
> that your inverse function agrees property with the
> monoid operation and unit.
>
> If that's going to be a value, it has to have some type.
> If that type is anything like "Proof that inverse a ! a = e",
> then the type mentions, or "depends on" the values
> inverse, (!), and e.
>
> You can see exactly this in the Agda standard library,
> in the definitions IsMonoid and IsGroup in
> Algebra.Structures, which define records containing
> proofs that a set of operations actually forms a monoid
> or group.
>
>
> You could probably avoid the apparent circularity
> of full dependent types if you split up a language
> into values which can have types, and a separate
> pair of propositions and proofs which can refer to
> values and types, but not to themselves.
>
> I think that's basically the organization of any system
> where you use a separate prover to prove things about
> programs in some previously-existing programming
> language, but I haven't stumbled across any examples
> where that sort of organization was designed into
> a single language from the start.
>
>
> Brandon
>


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
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Sub class and model expansion

Ryan Ingram
On Tue, May 31, 2011 at 1:40 AM, Patrick Browne <[hidden email]> wrote:
Continuing the thread on model expansion.
I have changed the example trying to focus on expanding models of M in G
Why is the operation ! ok or RHS but not visible on LHS of G?
The equation itself does not seem to suffer from the dependent type
problem of my previous post.

class M a where
 (!)  ::  a -> a -> a
 e :: a


class M a => G a where
 (!-)  ::  a -> a -> a
-- OK in G
 a !- e = e ! a

This doesn't do what you think.  This is equivalent to

(!-) = (\a e -> e ! a)

That is, "e" is lambda-bound here, not the same "e" from M.  In this case you've defined (!-) as "flip (!)"

When you define functions in a class declaration, you are just defining a default implementation.  Generally this is used when you can implement some functions in terms of the others, such as:

class Eq a where
   (==) :: a -> a -> a
   (/=) :: a -> a -> a

   a == b = not (a /= b)
   a /= b = not (a == b)

Now someone making an instance of this class need only define (==) or (/=); the other one will be defined via the default instance.  (This has the somewhat undesirable property that 'instance Eq X where' with no methods is a valid instance declaration but in that instance == and /= are infinite loops)

Maybe this will help you think about this: what code do you expect to write for instances of this class?

instance M Int where
  e = 0
  (!) = +

instance G Int where
  -- do I need to write any code here?

It seems to me you are expecting the compiler to automatically derive the definition 'inverse = negate'; there's no general way for the compiler to do so, since it doesn't know the structure of your type.

Functions in Haskell, unlike, say, Prolog, only go from left of the = to the right of the =.  Thanks to referential transparency, you can go backwards from the point of view of proving properties about your code, but during evaluation term rewriting only happens from left to right.

  -- ryan

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe