Provide a smart aliasing feature

[ahmadsalim]

Currently it is possible to some aliasing by simply declaring a function with result type Type, like

Pair : Type -> Type -> Type
Pair a b = HVect [a , b]

However, such declaration loses injectivity which is that if Pair a b = Pair a' b' then a = a' and b = b' are not necessarily true. It would therefore be desirable to be able to define an injective alias akin to

alias 
Pair : Type -> Type -> Type
Pair a b = HVect [a , b]

A more advanced feature would be to provide constructor aliases, which can also be used for pattern matching.

alias 
Singleton : a -> Vect 1 a
Singleton x = [x]        

Since overloading is usually possible in constructors, it would also be desirable to have overloading on aliases (and disambiguate by result type as usual), like overloading Singleton:

alias
Singleton : a -> List a
Singleton x = [x]

While there is a way to define new pattern syntax, it doesn't work well with pattern matching, e.g.

extract : Vec 1 a -> a
extract (Singleton {a = a} x) = the a $ x

is not nice to do with pattern syntax, especially with multiple different possible implicit arguments.

This request aims to make it easier to deprecate things by renaming, and provide ways to make more readable type signatures by simplifying complex types.

[ahmadsalim]

This would make it easier to provide deprecation support (#1455) for renamed functions in #1516.

[edwinb]

I don’t think the injectivity thing is a problem is it? Since unification looks at the normal form of a value rather than the top level it will know ‘Pair’ is injective because ‘HVect’ is injective. Or have you found a situation where this doesn’t work?

The pattern matching problem is different, though. I know some people have expected what you’re describing to work (e.g. defining one = S Z and expecting it to be possible to match on ‘one’, which doesn’t work because ‘one’ is bound as a pattern variable). Maybe instead of ‘alias’ we could mark a definition as a ‘pattern’ definition meaning that it should not be bound in a pattern clause.

(Usual caveat that I haven’t thought this through yet, this is just my first thoughts on the suggestion...)

On 9 Sep 2014, at 21:47, Ahmad Salim Al-Sibahi notifications@github.com wrote:

Currently it is possible to some aliasing by simply declaring a function with result type Type, like

Pair : Type -> Type -> Type
Pair a b = HVect [a , b]
However, such declaration loses injectivity which is that if Pair a b = Pair a' b' then a = a' and b = b' are not necessarily true. It would therefore be desirable to be able to define an injective alias akin to

alias

Pair : Type -> Type -> Type
Pair a b = HVect [a , b]
A more advanced feature would be to provide constructor aliases, which can also be used for pattern matching.

alias

Singleton : a -> Vect 1
a

Singleton x = [x]

Since overloading is usually possible in constructors, it would also be desirable to have overloading on aliases (and disambiguate by result type as usual), like overloading Singleton:

alias

Singleton : a -> List
a

Singleton x = [x]
While there is a way to define new pattern syntax, it doesn't work well with pattern matching, e.g.

extract : Vec 1 a ->
a
extract
(Singleton {a = a} x) = the a $
x

is not nice to do with pattern syntax, especially with multiple different possible implicit arguments.

This request aims to make it easier to deprecate things by renaming, and provide ways to make more readable type signatures by simplifying complex types.

—
Reply to this email directly or view it on GitHub.

[ahmadsalim]

@edwinb Hmm, I thought there was once a time where I experienced such issue; but I cannot remember exactly why. It is perhaps not a problem, but maybe it could be nice to have a way to enforce such thing (like the total keyword)?

I am not sure how pattern aliases should work yet, but I thought it might be a good idea to propose something.
It could however make sense to mark things as pattern definitions, and it would be nice if they enable symmetric use (construction/matching) on datatypes and provide a simpler way to work with some of the more complex types.

[edwinb]

Something like this would be very nice, but there hasn't been any proposal on exactly how to make this work or what the feature would look like, and there doesn't seem to be anyone enthusiastic about working on it.

I'm closing this, therefore, but any concrete proposals on this idea would still be welcome (perhaps better as a dragon egg)