Add comparable typevar constraints #229

New Issue

2020-02-20T23:15:44+09:00

zxq9 commented

2020-02-20 23:15:44 +09:00

(Migrated from gitlab.com)

Created by: radrow

Currently all types can be combined with == and =<-like relation operators. While this works cool on ints, strings and possibly some other types, it seems to be completely useless for custom ADTs and functions. In my opinion the expression ((x, y) => x) == ((x, y) => y) shouldn't typecheck, as it may lead to hard to find bugs.
Another example: FixedTTL(x) > FixedTTL(y) works as expected comparing x > y, but if we accidentally compare FixedTTL and RelativeTTL the first one will be always greater, no matter of the arguments.

To solve this issue I propose adding qualification to typevars (similar to typeclasses, but restricted only to Ord and Eq):

// Most general type is spelled 'a. It cannot be compared and unified with generalized non-comparable typevar.
function id(x : 'a) : 'a = x

// Types that can be compared using `==` operator would have double tick before the tvar name
function neq(x : ''a, y : ''a) : bool = !(x == y)

// Types forming a linear order would require triple tick (or something else, this is starting to look ugly)
function lt(x : '''a, y : '''a) : bool = x < y
// ''a unifies with '''a
function spec_eq(x : '''a, y : '''a) : bool = x == y

The new syntax opens another way of dealing with it:

function 
  lt : 'a is ord, ('a, 'a) => bool
  lt(x, y) = x < y

I think this is the place where we could accept operator overloading. Although in situations where == can be derived automatically it is usually the best and the only solution, the < like operators can be more tricky so we could let the users define the comparison by themselves. Of course not stateful nor payable.

*Created by: radrow* Currently all types can be combined with `==` and `=<`-like relation operators. While this works cool on ints, strings and possibly some other types, it seems to be completely useless for custom ADTs and functions. In my opinion the expression `((x, y) => x) == ((x, y) => y)` shouldn't typecheck, as it may lead to hard to find bugs. Another example: `FixedTTL(x) > FixedTTL(y)` works as expected comparing `x > y`, but if we accidentally compare `FixedTTL` and `RelativeTTL` the first one will be always greater, no matter of the arguments. To solve this issue I propose adding qualification to typevars (similar to typeclasses, but restricted only to `Ord` and `Eq`): ``` // Most general type is spelled 'a. It cannot be compared and unified with generalized non-comparable typevar. function id(x : 'a) : 'a = x // Types that can be compared using `==` operator would have double tick before the tvar name function neq(x : ''a, y : ''a) : bool = !(x == y) // Types forming a linear order would require triple tick (or something else, this is starting to look ugly) function lt(x : '''a, y : '''a) : bool = x < y // ''a unifies with '''a function spec_eq(x : '''a, y : '''a) : bool = x == y ``` The new syntax opens another way of dealing with it: ``` function lt : 'a is ord, ('a, 'a) => bool lt(x, y) = x < y ``` I think this is the place where we could accept operator overloading. Although in situations where `==` can be derived automatically it is usually the best and the only solution, the `<` like operators can be more tricky so we could let the users define the comparison by themselves. Of course not stateful nor payable.

Sign in to join this conversation.

1 Participants

Notifications

Due Date

No due date set.

Dependencies

No dependencies set.

Reference: QPQ-AG/sophia#229