Ord for partially ordered sets

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

Ord for partially ordered sets

Ivan Lazar Miljenovic
What is the validity of defining an Ord instance for types for which
mathematically the `compare` function is partially ordered?

Specifically, I have a pull request for fgl [1] to add Ord instances
for the graph types (based upon the Ord instances for Data.Map and
Data.IntMap, which I believe are themselves partially ordered), and
I'm torn as to the soundness of adding these instances.  It might be
useful in Haskell code (the example given is to use graphs as keys in
a Map) but mathematically-speaking it is not possible to compare two
arbitrary graphs.

What are people's thoughts on this?  What's more important: potential
usefulness/practicality or mathematical correctness?

(Of course, the correct answer is to have a function of type a -> a ->
Maybe Ordering :p)

[1]: https://github.com/haskell/fgl/pull/11

--
Ivan Lazar Miljenovic
[hidden email]
http://IvanMiljenovic.wordpress.com
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Ord for partially ordered sets

Tom Ellis
On Fri, Apr 24, 2015 at 11:06:07PM +1000, Ivan Lazar Miljenovic wrote:
> What is the validity of defining an Ord instance for types for which
> mathematically the `compare` function is partially ordered?

I'm confused.  What is supposed to be the result of `g1 <= g2` when `g1` and
`g2` are not comparable according to the partial order?
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Ord for partially ordered sets

Ivan Lazar Miljenovic
On 24 April 2015 at 23:17, Tom Ellis
<[hidden email]> wrote:
> On Fri, Apr 24, 2015 at 11:06:07PM +1000, Ivan Lazar Miljenovic wrote:
>> What is the validity of defining an Ord instance for types for which
>> mathematically the `compare` function is partially ordered?
>
> I'm confused.  What is supposed to be the result of `g1 <= g2` when `g1` and
> `g2` are not comparable according to the partial order?

With the proposed patch, it's the result of <= on the underlying [Int]Maps.

Does the definition of Ord on Data.Map make sense?  e.g. what should
be the result of (fromList [(1,'a'), (2,'b'), (3, 'c')]) <= (fromList
[(1,'a'), (4,'d')])?  What about (fromList [(1,'a'), (2,'b'), (3,
'c')]) <= (fromList [(1,'a'), (2,'e')])?

--
Ivan Lazar Miljenovic
[hidden email]
http://IvanMiljenovic.wordpress.com
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Ord for partially ordered sets

Tom Ellis
On Fri, Apr 24, 2015 at 11:27:46PM +1000, Ivan Lazar Miljenovic wrote:

> On 24 April 2015 at 23:17, Tom Ellis
> <[hidden email]> wrote:
> > On Fri, Apr 24, 2015 at 11:06:07PM +1000, Ivan Lazar Miljenovic wrote:
> >> What is the validity of defining an Ord instance for types for which
> >> mathematically the `compare` function is partially ordered?
> >
> > I'm confused.  What is supposed to be the result of `g1 <= g2` when `g1` and
> > `g2` are not comparable according to the partial order?
>
> With the proposed patch, it's the result of <= on the underlying [Int]Maps.

Ah, so it's a case of adding a valid Ord instance that isn't a natural one
for the particular datatype.  If you really need something like that, for
example to add your graphs to a Data.Set, then I would suggest a newtype
might be appropriate.

Tom

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

Re: Ord for partially ordered sets

Henning Thielemann
In reply to this post by Ivan Lazar Miljenovic

On Fri, 24 Apr 2015, Ivan Lazar Miljenovic wrote:

> Specifically, I have a pull request for fgl [1] to add Ord instances for
> the graph types (based upon the Ord instances for Data.Map and
> Data.IntMap, which I believe are themselves partially ordered), and I'm
> torn as to the soundness of adding these instances.

In an application we needed to do some combinatorics of graphs and thus
needed Set Graph.

Nonetheless, I think that graph0 < graph1 should be a type error. We can
still have a set of Graphs using a newtype.
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Ord for partially ordered sets

Ivan Lazar Miljenovic
On 25 April 2015 at 00:01, Henning Thielemann
<[hidden email]> wrote:

>
> On Fri, 24 Apr 2015, Ivan Lazar Miljenovic wrote:
>
>> Specifically, I have a pull request for fgl [1] to add Ord instances for
>> the graph types (based upon the Ord instances for Data.Map and Data.IntMap,
>> which I believe are themselves partially ordered), and I'm torn as to the
>> soundness of adding these instances.
>
>
> In an application we needed to do some combinatorics of graphs and thus
> needed Set Graph.
>
> Nonetheless, I think that graph0 < graph1 should be a type error. We can
> still have a set of Graphs using a newtype.

This could work; the possible problem would be one of efficiency: if
it's done directly on the graph datatypes they can use the underlying
(ordered) data structure; going purely by the Graph API, there's no
guarantees of ordering and thus it would be needed to call sort, even
though in practice it's redundant.

--
Ivan Lazar Miljenovic
[hidden email]
http://IvanMiljenovic.wordpress.com
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Ord for partially ordered sets

Andreas Abel
In reply to this post by Ivan Lazar Miljenovic
On 04/24/2015 03:06 PM, Ivan Lazar Miljenovic wrote:
> What is the validity of defining an Ord instance for types for which
> mathematically the `compare` function is partially ordered?

I'd say this is harmful, as functions like min and max (and others) rely
on the totality of the ordering.

Partial orderings are useful in itself, I implemented my own library

 
https://hackage.haskell.org/package/Agda-2.4.2/docs/Agda-Utils-PartialOrd.html

mainly to use it for maintaining sets of incomparable elements:

 
https://hackage.haskell.org/package/Agda-2.4.2/docs/Agda-Utils-Favorites.html

> Specifically, I have a pull request for fgl [1] to add Ord instances
> for the graph types (based upon the Ord instances for Data.Map and
> Data.IntMap, which I believe are themselves partially ordered), and
> I'm torn as to the soundness of adding these instances.  It might be
> useful in Haskell code (the example given is to use graphs as keys in
> a Map) but mathematically-speaking it is not possible to compare two
> arbitrary graphs.
>
> What are people's thoughts on this?  What's more important: potential
> usefulness/practicality or mathematical correctness?
>
> (Of course, the correct answer is to have a function of type a -> a ->
> Maybe Ordering :p)
>
> [1]: https://github.com/haskell/fgl/pull/11
>


--
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

[hidden email]
http://www2.tcs.ifi.lmu.de/~abel/
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Ord for partially ordered sets

Tikhon Jelvis
I would be hesitant about adding an Ord instance normally, because there's no clear semantics for it. If we just pass it through to the underlying data structure, it might behave differently depending on how you implement the graph, which is something fgl should ideally abstract over.

Maybe you could provide them in a newtype yourself, in the library? You could call it something like GrKey to make it clear that it has an Ord instance for practical reasons rather than because graphs are meaningfully orderable. This just forces people who need the capability to be a bit more explicit about it.

On Fri, Apr 24, 2015 at 7:47 AM, Andreas Abel <[hidden email]> wrote:
On 04/24/2015 03:06 PM, Ivan Lazar Miljenovic wrote:
What is the validity of defining an Ord instance for types for which
mathematically the `compare` function is partially ordered?

I'd say this is harmful, as functions like min and max (and others) rely on the totality of the ordering.

Partial orderings are useful in itself, I implemented my own library


https://hackage.haskell.org/package/Agda-2.4.2/docs/Agda-Utils-PartialOrd.html

mainly to use it for maintaining sets of incomparable elements:


https://hackage.haskell.org/package/Agda-2.4.2/docs/Agda-Utils-Favorites.html

Specifically, I have a pull request for fgl [1] to add Ord instances
for the graph types (based upon the Ord instances for Data.Map and
Data.IntMap, which I believe are themselves partially ordered), and
I'm torn as to the soundness of adding these instances.  It might be
useful in Haskell code (the example given is to use graphs as keys in
a Map) but mathematically-speaking it is not possible to compare two
arbitrary graphs.

What are people's thoughts on this?  What's more important: potential
usefulness/practicality or mathematical correctness?

(Of course, the correct answer is to have a function of type a -> a ->
Maybe Ordering :p)

[1]: https://github.com/haskell/fgl/pull/11



--
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

[hidden email]
http://www2.tcs.ifi.lmu.de/~abel/

_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries


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

Re: Ord for partially ordered sets

Alexander Solla
In reply to this post by Ivan Lazar Miljenovic
I see it as "morally wrong".  It's like a Monad instance that doesn't obey the monad laws.  The kind of ticking timebomb strong typing is supposed to protect us against.  But that only works if we do our part and don't make non-sense instances.

Can your consumer get away with using a Hashable instance?  (I.e., for use in unordered-containers).  This would be morally correct -- the graph could presumably have a valid Hashable instance.


On Fri, Apr 24, 2015 at 6:06 AM, Ivan Lazar Miljenovic <[hidden email]> wrote:
What is the validity of defining an Ord instance for types for which
mathematically the `compare` function is partially ordered?

Specifically, I have a pull request for fgl [1] to add Ord instances
for the graph types (based upon the Ord instances for Data.Map and
Data.IntMap, which I believe are themselves partially ordered), and
I'm torn as to the soundness of adding these instances.  It might be
useful in Haskell code (the example given is to use graphs as keys in
a Map) but mathematically-speaking it is not possible to compare two
arbitrary graphs.

What are people's thoughts on this?  What's more important: potential
usefulness/practicality or mathematical correctness?

(Of course, the correct answer is to have a function of type a -> a ->
Maybe Ordering :p)

[1]: https://github.com/haskell/fgl/pull/11

--
Ivan Lazar Miljenovic
[hidden email]
http://IvanMiljenovic.wordpress.com
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe


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

Re: Ord for partially ordered sets

Jay Sulzberger
In reply to this post by Ivan Lazar Miljenovic



On Fri, 24 Apr 2015, Ivan Lazar Miljenovic <[hidden email]> wrote:

> What is the validity of defining an Ord instance for types for which
> mathematically the `compare` function is partially ordered?
>
> Specifically, I have a pull request for fgl [1] to add Ord instances
> for the graph types (based upon the Ord instances for Data.Map and
> Data.IntMap, which I believe are themselves partially ordered), and
> I'm torn as to the soundness of adding these instances.  It might be
> useful in Haskell code (the example given is to use graphs as keys in
> a Map) but mathematically-speaking it is not possible to compare two
> arbitrary graphs.
>
> What are people's thoughts on this?  What's more important: potential
> usefulness/practicality or mathematical correctness?
>
> (Of course, the correct answer is to have a function of type a -> a ->
> Maybe Ordering :p)
>
> [1]: https://github.com/haskell/fgl/pull/11
>
> --
> Ivan Lazar Miljenovic

Of course these type-classes (I hope I am using the
word correctly) should be standard:

1. Ord, which is the class of all totally ordered set-like things

2. PoSet, which is the class of all partially ordered set-like things

3. NonStrictPoSet, which is the class of all partially ordered
set-like things, but without the requirement that a <= b and b <= a implies
a Equal b.

4. Things like above, but with the requirement of a Zero, with
the requirement of a One, and the requirement fo both a Zero and a One.

oo--JS.


> [hidden email]
> http://IvanMiljenovic.wordpress.com
> _______________________________________________
> Haskell-Cafe mailing list
> [hidden email]
> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
>
>
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Ord for partially ordered sets

Barak A. Pearlmutter
In reply to this post by Ivan Lazar Miljenovic
> I'm confused.  What is supposed to be the result of `g1 <= g2` when `g1` and
> `g2` are not comparable according to the partial order?

Surely it would make things less confusing to simply follow existing
precedent already in the standard prelude?

$ ghci
Prelude> let nan=0/0::Double
Prelude> nan==nan
False
Prelude> compare 0 nan
GT
Prelude> compare nan 0
GT
Prelude> compare nan nan
GT
Prelude> 0<=nan
False
Prelude> nan<=0
False
Prelude> nan<=nan
False
Prelude> let infty=1/0::Double
Prelude> infty <= nan
False
Prelude> nan <= infty
False

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

Class-like features for explicit arguments (was: Ord for partially ordered sets)

Ertugrul Söylemez-2
In reply to this post by Jay Sulzberger
> 3. NonStrictPoSet, which is the class of all partially ordered
> set-like things, but without the requirement that a <= b and b <= a
> implies a Equal b.

Those are preorders.  An antisymmetric preorder is a non-strict poset.

Also it's difficult to capture all of those various order types in
Haskell's class system.  A type can have many orders and many underlying
equivalence relations in the case of partial and total orders, and there
are different ways to combine them.  For example equality is a partial
order, modular equivalence is a preorder, etc.  Those denote bags and
groups more than sequences or trees.

Perhaps it's time to add a type class-like system to Haskell, but for
explicitly passed arguments:

    record Relation a where
        related :: a -> a -> Bool

        unrelated :: a -> a -> Bool
        unrelated x y = not (related x y)

    func1 :: Relation A -> A -> A -> A
    func1 _ x y = ... related x y ...

    func2 :: Relation A -> Relation A -> A -> A -> A
    func2 r1 r2 x y = ... r1.related x y ... r2.unrelated x y ...

In a lot of cases this is much more appropriate than a type class, and
it would turn many things that are currently types into regular
functions, thus making them a lot more composable:

    down :: Ord a -> Ord a
    down o =
        Ord { compare x y = o.compare y x }
        -- The remaining Ord functions are defaulted.

Perhaps all we need is to generalise default definitions to data types
and add module-like dot syntax for records (mainly to preserve infix
operators).  Formally speaking there is also little that prevents us
From having associated types in those records that can be used on the
type level.

For actual record types (i.e. single-constructor types) we could even
have specialisation and get a nice performance boost that way, if we ask
for it:

    {-# SPECIALISE down someOrder :: Ord SomeType #-}

This would be extremely useful.


> 4. Things like above, but with the requirement of a Zero, with the
> requirement of a One, and the requirement fo both a Zero and a One.

Zero and one as in minBound and maxBound or rather as in Monoid and a
hypothetical Semiring?  In the latter case I believe they don't really
belong into an additional class, unless you have some ordering-related
laws for the zeroes and ones.  If not, you can always simply use an
Ord+Semiring constraint.

There may be some motivation to make Bounded a subclass of Ord though.


Greets,
Ertugrul

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

signature.asc (482 bytes) Download Attachment
Reply | Threaded
Open this post in threaded view
|

Re: Ord for partially ordered sets

Ertugrul Söylemez-2
In reply to this post by Tom Ellis
> I'm confused.  What is supposed to be the result of `g1 <= g2` when `g1` and
> `g2` are not comparable according to the partial order?

False.


Greets,
Ertugrul

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

signature.asc (482 bytes) Download Attachment
Reply | Threaded
Open this post in threaded view
|

Re: Ord for partially ordered sets

Mike Izbicki
>> I'm confused.  What is supposed to be the result of `g1 <= g2` when `g1` and
>> `g2` are not comparable according to the partial order?
>
>False.

The operators aren't a problem for this reason.  The real problem is
what does `compare` return?

On Fri, Apr 24, 2015 at 1:32 PM, Ertugrul Söylemez <[hidden email]> wrote:

>> I'm confused.  What is supposed to be the result of `g1 <= g2` when `g1` and
>> `g2` are not comparable according to the partial order?
>
> False.
>
>
> Greets,
> Ertugrul
>
> _______________________________________________
> Haskell-Cafe mailing list
> [hidden email]
> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
>
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Class-like features for explicit arguments (was: Ord for partially ordered sets)

Carter Schonwald
In reply to this post by Ertugrul Söylemez-2
hrm, wouldn't your proposed extension be largely accomplished by using Record pun and Record WildCards?

eg 

{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE  RecordPuns #-}
module Foo where
data Relation a = Rel{related :: a -> a ->Bool,unrelated :: a -> a -> Bool}

foo :: Relation A -> A -> A -> Bool
foo Rel{..} x y = related x y 

------
or am i over looking something?
I do realize this may not quite be what youre suggesting, and if so, could you help me understand better? :) 


On Fri, Apr 24, 2015 at 4:26 PM, Ertugrul Söylemez <[hidden email]> wrote:
> 3. NonStrictPoSet, which is the class of all partially ordered
> set-like things, but without the requirement that a <= b and b <= a
> implies a Equal b.

Those are preorders.  An antisymmetric preorder is a non-strict poset.

Also it's difficult to capture all of those various order types in
Haskell's class system.  A type can have many orders and many underlying
equivalence relations in the case of partial and total orders, and there
are different ways to combine them.  For example equality is a partial
order, modular equivalence is a preorder, etc.  Those denote bags and
groups more than sequences or trees.

Perhaps it's time to add a type class-like system to Haskell, but for
explicitly passed arguments:

    record Relation a where
        related :: a -> a -> Bool

        unrelated :: a -> a -> Bool
        unrelated x y = not (related x y)

    func1 :: Relation A -> A -> A -> A
    func1 _ x y = ... related x y ...

    func2 :: Relation A -> Relation A -> A -> A -> A
    func2 r1 r2 x y = ... r1.related x y ... r2.unrelated x y ...

In a lot of cases this is much more appropriate than a type class, and
it would turn many things that are currently types into regular
functions, thus making them a lot more composable:

    down :: Ord a -> Ord a
    down o =
        Ord { compare x y = o.compare y x }
        -- The remaining Ord functions are defaulted.

Perhaps all we need is to generalise default definitions to data types
and add module-like dot syntax for records (mainly to preserve infix
operators).  Formally speaking there is also little that prevents us
From having associated types in those records that can be used on the
type level.

For actual record types (i.e. single-constructor types) we could even
have specialisation and get a nice performance boost that way, if we ask
for it:

    {-# SPECIALISE down someOrder :: Ord SomeType #-}

This would be extremely useful.


> 4. Things like above, but with the requirement of a Zero, with the
> requirement of a One, and the requirement fo both a Zero and a One.

Zero and one as in minBound and maxBound or rather as in Monoid and a
hypothetical Semiring?  In the latter case I believe they don't really
belong into an additional class, unless you have some ordering-related
laws for the zeroes and ones.  If not, you can always simply use an
Ord+Semiring constraint.

There may be some motivation to make Bounded a subclass of Ord though.


Greets,
Ertugrul

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



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

Re: Class-like features for explicit arguments (was: Ord for partially ordered sets)

Ertugrul Söylemez-2
> hrm, wouldn't your proposed extension be largely accomplished by using
> Record pun and Record WildCards?

A part of it would, but it wouldn't preserve operators.  For example
instead of `x r.<> y` you would have to write `(<>) r x y`.  Also
defaults are not available.  Other class features are not accessible,
most notably type-level features like associated types.

The idea is that a record would be completely equivalent to a class with
the only difference being that you define values instead of instances,
that there are no constraints on which values can exist and that those
values must be passed explicitly to functions as regular arguments.


>> Perhaps it's time to add a type class-like system to Haskell, but for
>> explicitly passed arguments:
>>
>>     record Relation a where
>>         related :: a -> a -> Bool
>>
>>         unrelated :: a -> a -> Bool
>>         unrelated x y = not (related x y)
>>
>>     func1 :: Relation A -> A -> A -> A
>>     func1 _ x y = ... related x y ...
>>
>>     func2 :: Relation A -> Relation A -> A -> A -> A
>>     func2 r1 r2 x y = ... r1.related x y ... r2.unrelated x y ...
>>
>> In a lot of cases this is much more appropriate than a type class, and
>> it would turn many things that are currently types into regular
>> functions, thus making them a lot more composable:
>>
>>     down :: Ord a -> Ord a
>>     down o =
>>         Ord { compare x y = o.compare y x }
>>         -- The remaining Ord functions are defaulted.
>>
>> Perhaps all we need is to generalise default definitions to data types
>> and add module-like dot syntax for records (mainly to preserve infix
>> operators).  Formally speaking there is also little that prevents us
>> From having associated types in those records that can be used on the
>> type level.
>>
>> For actual record types (i.e. single-constructor types) we could even
>> have specialisation and get a nice performance boost that way, if we ask
>> for it:
>>
>>     {-# SPECIALISE down someOrder :: Ord SomeType #-}
>>
>> This would be extremely useful.

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

signature.asc (482 bytes) Download Attachment
Reply | Threaded
Open this post in threaded view
|

Re: Class-like features for explicit arguments

Roman Cheplyaka-2
On 25/04/15 15:51, Ertugrul Söylemez wrote:
>> hrm, wouldn't your proposed extension be largely accomplished by using
>> Record pun and Record WildCards?
>
> A part of it would, but it wouldn't preserve operators.  For example
> instead of `x r.<> y` you would have to write `(<>) r x y`.

Not at all.

  {-# LANGUAGE RecordWildCards #-}

  import Prelude hiding (sum)

  data Monoid a = Monoid { empty :: a, (<>) :: a -> a -> a }

  sum :: Num a => Monoid a
  sum = Monoid 0 (+)

  three :: Integer
  three =
    let Monoid{..} = sum in
    1 <> 2

> Other class features are not accessible,
> most notably type-level features like associated types.

Associated types become additional type variables of the record type.

A class

  class C a where
    type T a

is essentially equivalent to

  class C a t | a -> t

But the functional dependency is not enforceable on the value level
(isn't the whole point of this discussion not to restrict what
"instances" can be defined), so you end up with

  class C a t,

a simple MPTC.

> Also defaults are not available.

Now this is a good point.

> The idea is that a record would be completely equivalent to a class with
> the only difference being that you define values instead of instances,
> that there are no constraints on which values can exist and that those
> values must be passed explicitly to functions as regular arguments.

Except we already have regular records (aka data types) which satisfy
90% of the requirements, and adding another language construct to
satisfy those remaining 10% feels wrong to me. I'd rather improve the
existing construct.

Roman



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

signature.asc (836 bytes) Download Attachment
Reply | Threaded
Open this post in threaded view
|

Re: Class-like features for explicit arguments

Ertugrul Söylemez-2
>>> hrm, wouldn't your proposed extension be largely accomplished by

>>> using Record pun and Record WildCards?
>>
>> A part of it would, but it wouldn't preserve operators.  For example
>> instead of `x r.<> y` you would have to write `(<>) r x y`.
>
> Not at all.
>
>   three :: Integer
>   three =
>     let Monoid{..} = sum in
>     1 <> 2
Puns become tedious and error-prone as soon as you need to refer to
multiple records, when operators are involved.  But it's not that
important actually.  I can live with the current record syntax.

The most useful features would be defaults, a more suitable syntax for
defining record types and potentially the following:


>> Other class features are not accessible, most notably type-level
>> features like associated types.
>
> Associated types become additional type variables of the record type.

Indeed.  However, when the type follows from other type arguments, it
would often be convenient not to spell it out and instead bring an
associated type constructor into scope.  This is especially true when
the AT refers to a type that isn't used very often.

    record Extractor a where
        type Elem a
        extract :: a -> Maybe (Elem a, a)

    extractTwo
        :: (e1 : Extractor a)
        -> (e2 : Extractor a)
        -> a
        -> Maybe (e1.Elem a, e2.Elem a, a)
    extractTwo e1 e2 xs0 = do
        (x1, xs1) <- e1.extract xs0
        (x2, xs2) <- e1.extract xs1
        return (x1, x2, xs2)


> But the functional dependency is not enforceable on the value level
> (isn't the whole point of this discussion not to restrict what
> "instances" can be defined), so you end up with
>
>   class C a t,
>
> a simple MPTC.

I don't see a reason to enforce a dependency, since there is no
equivalent to instance resolution.  Regular unification should cover any
ambiguities, and if it doesn't you need ScopedTypeVariables.


>> The idea is that a record would be completely equivalent to a class
>> with the only difference being that you define values instead of
>> instances, that there are no constraints on which values can exist
>> and that those values must be passed explicitly to functions as
>> regular arguments.
>
> Except we already have regular records (aka data types) which satisfy
> 90% of the requirements, and adding another language construct to
> satisfy those remaining 10% feels wrong to me. I'd rather improve the
> existing construct.
That's actually what I'm proposing.  The record syntax would simply be
syntactic sugar for single-constructor data types that is more suitable
for records, especially when defaults and other class-like features are
involved.  Most notably it would support layout.  There is no reason why
you shouldn't be able to use `data` to achieve the same thing, except
with a clumsier syntax and the option to have multiple constructors.


Greets,
Ertugrul

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

signature.asc (482 bytes) Download Attachment
Reply | Threaded
Open this post in threaded view
|

Re: Class-like features for explicit arguments

Carter Schonwald
Isn't your associated type here more like a dependent record field/ existential that we can kinda expose?

This does seem to veer into first class module territory.  Especially wrt needing first class types in a fashion. 

Have you had a chance to peruse the Andreas Rossberg 1ml paper on embedding first class modules into f omega that has been circulating? Perhaps there are ideas There that could be adapted. Especially since core is an augmented f omega

On Saturday, April 25, 2015, Ertugrul Söylemez <[hidden email]> wrote:
>>> hrm, wouldn't your proposed extension be largely accomplished by
>>> using Record pun and Record WildCards?
>>
>> A part of it would, but it wouldn't preserve operators.  For example
>> instead of `x r.<> y` you would have to write `(<>) r x y`.
>
> Not at all.
>
>   three :: Integer
>   three =
>     let Monoid{..} = sum in
>     1 <> 2

Puns become tedious and error-prone as soon as you need to refer to
multiple records, when operators are involved.  But it's not that
important actually.  I can live with the current record syntax.

The most useful features would be defaults, a more suitable syntax for
defining record types and potentially the following:


>> Other class features are not accessible, most notably type-level
>> features like associated types.
>
> Associated types become additional type variables of the record type.

Indeed.  However, when the type follows from other type arguments, it
would often be convenient not to spell it out and instead bring an
associated type constructor into scope.  This is especially true when
the AT refers to a type that isn't used very often.

    record Extractor a where
        type Elem a
        extract :: a -> Maybe (Elem a, a)

    extractTwo
        :: (e1 : Extractor a)
        -> (e2 : Extractor a)
        -> a
        -> Maybe (e1.Elem a, e2.Elem a, a)
    extractTwo e1 e2 xs0 = do
        (x1, xs1) <- e1.extract xs0
        (x2, xs2) <- e1.extract xs1
        return (x1, x2, xs2)


> But the functional dependency is not enforceable on the value level
> (isn't the whole point of this discussion not to restrict what
> "instances" can be defined), so you end up with
>
>   class C a t,
>
> a simple MPTC.

I don't see a reason to enforce a dependency, since there is no
equivalent to instance resolution.  Regular unification should cover any
ambiguities, and if it doesn't you need ScopedTypeVariables.


>> The idea is that a record would be completely equivalent to a class
>> with the only difference being that you define values instead of
>> instances, that there are no constraints on which values can exist
>> and that those values must be passed explicitly to functions as
>> regular arguments.
>
> Except we already have regular records (aka data types) which satisfy
> 90% of the requirements, and adding another language construct to
> satisfy those remaining 10% feels wrong to me. I'd rather improve the
> existing construct.

That's actually what I'm proposing.  The record syntax would simply be
syntactic sugar for single-constructor data types that is more suitable
for records, especially when defaults and other class-like features are
involved.  Most notably it would support layout.  There is no reason why
you shouldn't be able to use `data` to achieve the same thing, except
with a clumsier syntax and the option to have multiple constructors.


Greets,
Ertugrul

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

Re: Class-like features for explicit arguments

Ertugrul Söylemez-2
> Isn't your associated type here more like a dependent record field/
> existential that we can kinda expose?

Not quite.  There is still a clear distinction between type and value
level.  You cannot refer to an AT on the value level or to a member
value on the type level.


> This does seem to veer into first class module territory.  Especially
> wrt needing first class types in a fashion.

I think formally there is little difference between a powerful record
system and a first-class module system.  However, even in a
non-dependent language a first class module could still expect a value
argument.  A record type couldn't do this without essentially making the
language dependent on the way.


> Have you had a chance to peruse the Andreas Rossberg 1ml paper on
> embedding first class modules into f omega that has been circulating?
> Perhaps there are ideas There that could be adapted. Especially since
> core is an augmented f omega

I haven't read it, sorry.  My proposal should conform to the current
core language, as it's mostly just a syntax transformation.  The only
new semantics would be defaults.

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

signature.asc (482 bytes) Download Attachment
12