Fix up dependent contract syntax #8

Closed
disnet opened this Issue Aug 30, 2011 · 10 comments

Comments

Projects
None yet
4 participants
@disnet
Owner

disnet commented Aug 30, 2011

I'm not too happy with the syntax we have for dependent contracts right now.

f :: (Num) -> !(result) -> $1 > result

Scope of $1 is not obvious and its a bit to magical. Would love to allow explicit naming:

f :: (arg:Num) -> !(result) -> arg > result

But this conflicts with object contracts (and I don't think this can be disambiguated). Some other ideas that have been bouncing around:

f :: (x::Num) -> !(result) -> x > result
f :: (x=Num) -> !(result) -> x > result
f :: (Num as x) -> !(result) -> x > result
@paulcc

This comment has been minimized.

Show comment
Hide comment
@paulcc

paulcc Oct 9, 2011

hi

+1 on explicit naming.

can you give some concrete examples of where object contracts conflict? or say which rules conflict? I know some LALR tricks which might (or might not) help.

Paul

paulcc commented Oct 9, 2011

hi

+1 on explicit naming.

can you give some concrete examples of where object contracts conflict? or say which rules conflict? I know some LALR tricks which might (or might not) help.

Paul

@paulmillr

This comment has been minimized.

Show comment
Hide comment
@paulmillr

paulmillr Oct 9, 2011

What about using Haskell syntax for this?

f :: (Num x) => x -> !(result) -> x > result

What about using Haskell syntax for this?

f :: (Num x) => x -> !(result) -> x > result
@paulcc

This comment has been minimized.

Show comment
Hide comment
@paulcc

paulcc Oct 9, 2011

perhaps a better question is: what syntax do you use for each in your papers?

paulcc commented Oct 9, 2011

perhaps a better question is: what syntax do you use for each in your papers?

@paulcc

This comment has been minimized.

Show comment
Hide comment
@paulcc

paulcc Oct 9, 2011

ie, if it's not obviously conflicting in your papers, then it's a shame to let LR dictate it.

paulcc commented Oct 9, 2011

ie, if it's not obviously conflicting in your papers, then it's a shame to let LR dictate it.

@disnet

This comment has been minimized.

Show comment
Hide comment
@disnet

disnet Oct 10, 2011

Owner

The problem isn't just disambiguation. It's that the syntax I'd love (and see most often in papers) where we name the argument like name:Num is exactly the same as an object contract (since CoffeeScript lets us have implicit braces). I don't think we want to change how object contracts are handled in the contract language so we have to do something else.

@paulmillr I think that syntax would be a bit confusing since in haskell that means to constrain by the typeclass right? Humm...maybe that'd work though. The multi arg would look like:

f :: (Num x, Str y) => (x, y) -> !(result) -> x > result and y > result

Or simpler since => is redundant:

f :: (Num x, Str y) -> !(result) -> x > result and y > result

But now x and y look like type variables instead of just names so probably not what we want.

I think my favorite syntax right now is (Num as x) -> !(result) -> result > x. Thoughts?

Owner

disnet commented Oct 10, 2011

The problem isn't just disambiguation. It's that the syntax I'd love (and see most often in papers) where we name the argument like name:Num is exactly the same as an object contract (since CoffeeScript lets us have implicit braces). I don't think we want to change how object contracts are handled in the contract language so we have to do something else.

@paulmillr I think that syntax would be a bit confusing since in haskell that means to constrain by the typeclass right? Humm...maybe that'd work though. The multi arg would look like:

f :: (Num x, Str y) => (x, y) -> !(result) -> x > result and y > result

Or simpler since => is redundant:

f :: (Num x, Str y) -> !(result) -> x > result and y > result

But now x and y look like type variables instead of just names so probably not what we want.

I think my favorite syntax right now is (Num as x) -> !(result) -> result > x. Thoughts?

@paulmillr

This comment has been minimized.

Show comment
Hide comment
@paulmillr

paulmillr Oct 10, 2011

Your "typeclass as var" proposition seems to me as good as haskell example.

Or simpler since => is redundant:

I don't think so: consider a function where we pass many similar arguments:

f :: (SomeLongClassName s, SomeLongClassName2 t) => (s, s, s, t) -> [t, s, t, s] -> t s s s
# or
f :: (SomeLongClassName as s, SomeLongClassName2 as t) => (s, s, s, t) -> [t, s, t, s] -> t s s s

What would this example look like without =>?

Your "typeclass as var" proposition seems to me as good as haskell example.

Or simpler since => is redundant:

I don't think so: consider a function where we pass many similar arguments:

f :: (SomeLongClassName s, SomeLongClassName2 t) => (s, s, s, t) -> [t, s, t, s] -> t s s s
# or
f :: (SomeLongClassName as s, SomeLongClassName2 as t) => (s, s, s, t) -> [t, s, t, s] -> t s s s

What would this example look like without =>?

@disnet

This comment has been minimized.

Show comment
Hide comment
@disnet

disnet Oct 10, 2011

Owner

That syntax wouldn't work for dependent types. The point is to name each parameter uniquely.

What you have might actually be useful as a kind of "contract variable" but we need something different for uniquely identifying each param. We could combine them:

f :: (SomeLongClassName s, SomeLongClassName2 t) => (s as arg1, s as arg2, s, t) -> !(result) -> arg1 > arg2 > result

But if we just want a way to alias long contract names there's already a way since contracts are just values:

s = SomeLongClassName
f :: (s, s as arg2) -> ...

Not sure if it's a good idea to introduce special syntax for this.

Owner

disnet commented Oct 10, 2011

That syntax wouldn't work for dependent types. The point is to name each parameter uniquely.

What you have might actually be useful as a kind of "contract variable" but we need something different for uniquely identifying each param. We could combine them:

f :: (SomeLongClassName s, SomeLongClassName2 t) => (s as arg1, s as arg2, s, t) -> !(result) -> arg1 > arg2 > result

But if we just want a way to alias long contract names there's already a way since contracts are just values:

s = SomeLongClassName
f :: (s, s as arg2) -> ...

Not sure if it's a good idea to introduce special syntax for this.

@paulmillr

This comment has been minimized.

Show comment
Hide comment
@paulmillr

paulmillr Oct 10, 2011

f :: (s, s as arg2) -> ...

This solution is OK then. So, I think the form f :: (s, s as arg2) -> ... is great (with no support for dependent types).

f :: (s, s as arg2) -> ...

This solution is OK then. So, I think the form f :: (s, s as arg2) -> ... is great (with no support for dependent types).

@TobiaszCudnik

This comment has been minimized.

Show comment
Hide comment
@TobiaszCudnik

TobiaszCudnik Mar 13, 2012

Why overcomplicate simple things? If return from 1st func is a param to the 2nd one, same the params of the 1st one should be. Like so:

    f :: (Num) -> !(result, params) -> params[0] > result

Using named params (Num as x) is harder to maintain, because you can define 2nd function as generic one and use it with many others. Then, you would have to maintain same param name in all of these functions.

Why overcomplicate simple things? If return from 1st func is a param to the 2nd one, same the params of the 1st one should be. Like so:

    f :: (Num) -> !(result, params) -> params[0] > result

Using named params (Num as x) is harder to maintain, because you can define 2nd function as generic one and use it with many others. Then, you would have to maintain same param name in all of these functions.

disnet added a commit that referenced this issue Mar 13, 2012

@disnet

This comment has been minimized.

Show comment
Hide comment
@disnet

disnet Mar 13, 2012

Owner

Ha! Yeah you're right, that does simplify things a bit.

Realized we have a bit of an ambiguity though. A dependent contract:

f :: (Num) -> !(res, params) -> params[0] > res

Not a dependent contract:

MyEven = (x) -> x % 2 is 0
f :: (!MyEven) -> !MyEven

! is overloaded here.

Owner

disnet commented Mar 13, 2012

Ha! Yeah you're right, that does simplify things a bit.

Realized we have a bit of an ambiguity though. A dependent contract:

f :: (Num) -> !(res, params) -> params[0] > res

Not a dependent contract:

MyEven = (x) -> x % 2 is 0
f :: (!MyEven) -> !MyEven

! is overloaded here.

@disnet disnet closed this Apr 19, 2012

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment