Excellent bikeshedding opportunity! Frontend syntax for pattern synonym types

Carter Schonwald carter.schonwald at gmail.com
Mon Dec 23 05:45:48 UTC 2013


i'm confused, are these types ever human writeable?

If not, are they meant to be an operational way of communicating how a
pattern works? In which case, wouldn't having the pattern definition
visible in the haddocks be a simpler way to communicate it?  There have
been several projects in the past to have type system for describing lambda
calculi with pretty right higher order pattern matching facilities, perhaps
that vocabulary could be used here?

cheers (i hope my questions make sense, I could merely be confused)
-Carter


On Sun, Dec 22, 2013 at 10:56 PM, Dr. ERDI Gergo <gergo at erdi.hu> wrote:

> On Sun, 22 Dec 2013, Dr. ERDI Gergo wrote:
>
>  If it's only A and B, perhaps abominations like these could be considered:
>>>
>>>     -- implicit foralls
>>>     pattern Show t => P t :: (Num t, Eq b) => b -> T t
>>>
>>>     -- explicit foralls
>>>     pattern forall t. Show t => P t :: forall b. (Num t, Eq b) => b -> T
>>> t
>>>
>>
>> I'm not 100% sure what that 't' in 'P t' is supposed to be in your
>> example. 'P' is not like a type constructor at all; it's a lot more like a
>> data constructor.
>>
>
> Thinking further about it, I think this could work, using a syntax similar
> to data constructor definitions instead of sticking to the function type
> syntax:
>
> pattern (Num a, Eq b) => P a b :: (Show a) => T a
>
> or with explicit foralls (using the fact that we can deduce which tyvars
> are universial vs existential simply by seeing if they occur in 'T a'):
>
> pattern forall a b. (Num a, Eq b) => P a b :: (Show a) => T a
>
> my only concern with this one is that the direction of the first double
> arrow doesn't "feel right".
>
> Other examples with this syntax:
>
> -- Number literal patterns
> pattern Z :: (Num a, Eq a) => a pattern Z = 0
>
> -- Monomorphic patterns
> pattern TrueAnd Bool :: [Bool]
> pattern TrueAnd b = [True, b]
>
> -- Infix notation
> pattern a :< Seq a :: Seq a
> pattern x :< xs <- (Seq.viewl -> x Seq.:< xs)
>
> I'm liking this so far.
>
> Bye,
>         Gergo
>
>
> --
>
>   .--= ULLA! =-----------------.
>    \     http://gergo.erdi.hu   \
>     `---= gergo at erdi.hu =-------'
> RICE: Race Inspired Cosmetic Enhancement
> _______________________________________________
> Glasgow-haskell-users mailing list
> Glasgow-haskell-users at haskell.org
> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/glasgow-haskell-users/attachments/20131223/bde51969/attachment.html>


More information about the Glasgow-haskell-users mailing list