Start a hangout

## Profile

Brent Yorgey

Works at University of Pennsylvania

Attends University of Pennsylvania

Lives in Philadelphia, PA

966 followers|70,073 views

AboutPostsPhotosYouTube

## Stream

### Brent Yorgey

Shared publicly -Our paper has been accepted for the 2015 Mathematics of Program Construction Conference:

Polynomial Functors Constrained by Regular Expressions

http://dept.cs.williams.edu/~byorgey/pub/type-matrices.pdf

It's based on some blog posts from a couple of years ago and shows how to define a tree type in a language like Haskell where the leaves of the tree are constrained to match a regular expression. A basic example that many are familiar with is the type of lists where the elements alternate between two types. The picture corresponds to an example of a binary tree with regular expression b*1a* where 1 is the type with just one inhabitant so it functions as a "hole". These types have the property that it's completely impossible to build a tree that fails to satisfy the constraint.

As a side effect it also shows how you can think of Conor McBride's Jokers and Clowns paper as really being about divided differences (ie. (f(x)-f(y))/(x-y)) applied to types, even though you can't literally divide types: https://personal.cis.strath.ac.uk/conor.mcbride/Dissect.pdf

Sadly it's hard to find a programming language that can truly automate this process, especially as it involves matrices whose entries are types. Brent and I both tried independently with Agda, but even with dependent types we got stuck. But that doesn't stop you using the paper to hand craft the appropriate type. (I guess Template Haskell would work fine but that's cheating.)

Polynomial Functors Constrained by Regular Expressions

http://dept.cs.williams.edu/~byorgey/pub/type-matrices.pdf

It's based on some blog posts from a couple of years ago and shows how to define a tree type in a language like Haskell where the leaves of the tree are constrained to match a regular expression. A basic example that many are familiar with is the type of lists where the elements alternate between two types. The picture corresponds to an example of a binary tree with regular expression b*1a* where 1 is the type with just one inhabitant so it functions as a "hole". These types have the property that it's completely impossible to build a tree that fails to satisfy the constraint.

As a side effect it also shows how you can think of Conor McBride's Jokers and Clowns paper as really being about divided differences (ie. (f(x)-f(y))/(x-y)) applied to types, even though you can't literally divide types: https://personal.cis.strath.ac.uk/conor.mcbride/Dissect.pdf

Sadly it's hard to find a programming language that can truly automate this process, especially as it involves matrices whose entries are types. Brent and I both tried independently with Agda, but even with dependent types we got stuck. But that doesn't stop you using the paper to hand craft the appropriate type. (I guess Template Haskell would work fine but that's cheating.)

3

5 comments

Very nice paper!

Add a comment...

### Brent Yorgey

Shared publicly -View from our new front door.

3

5 comments

A technician? I thought Google would deliver a self-decorating door in a self-driving car.

Add a comment...

In his circles

444 people

### Communities

8 communities### Brent Yorgey

Shared publicly -https://www.google.com/maps/@34.531485,-92.645217,3a,75y,257.33h,73.27t/data=!3m4!1e1!3m2!1sDL3lS3WL-jXfzFDk83M5nA!2e0

A one hour drive from where I will be living next year.

A one hour drive from where I will be living next year.

5

Debbie Yorgey

+

1

2

1

2

1

You'll have to host a Haskell symposium there!!

Add a comment...

### Brent Yorgey

Shared publicly -26

4 comments

Unfortunately, 'cum laude' differs highly per country. E.g. in The Netherlands 'cum laude' is the only distinction and is awarded to ~5-10% of PhDs. Germany follows the usual three distinctions of the Latin system (cum laude, magna cum laude, summa cum laude). tl;dr: in The Netherlands cum laude is the highest distinction, in Germany summa is the highest distinction and you probably want to get at least cum laude.

Though, I am not sure if this applies to 'with honours' to, if it is less ambiguous, that would be something :).

Though, I am not sure if this applies to 'with honours' to, if it is less ambiguous, that would be something :).

Add a comment...

### Brent Yorgey

Shared publicly -Noah's favorite game right now is to sing "A,B,C,D,E,F,____" where the

*__*is filled in with anything other than "G" (e.g. "Q", but more often non-letters such as "cow", "lobster", "seven", "climb"). Whereupon I tickle him in mock outrage and he shrieks with laughter. I'm very proud that my son finds type errors humorous.3

2 comments

Teach him 123456789ABCDEF0.

Add a comment...

### Brent Yorgey

Shared publicly -Me: "Noah, are you ready to get out of the bath now?"

Noah: "Not no. Yes!"

I should have given him a stern lecture about the dangers of double negation elimination, but I was blinded by the cuteness.

Noah: "Not no. Yes!"

I should have given him a stern lecture about the dangers of double negation elimination, but I was blinded by the cuteness.

11

2 comments

Andrew Bromage

+

3

4

3

4

3

Perhaps that was the point. Not only is it refutable that he wasn't ready to get out of the bath, it was also provable that he was.

Add a comment...

### Brent Yorgey

Shared publicly -When I picked up Noah from daycare yesterday, he wanted to go to the potty before we left for home. I then discovered he needed his diaper changed first. But it turned out his diaper bag was downstairs. So we had to get his diaper bag in order to change his diaper in order to go to the potty in order to go home. On the way down the stairs I taught him about the ways of the world. "We are shaving yaks, buddy," I said. "Saving ax," he repeated.

6

Add a comment...

### Brent Yorgey

Shared publicly -Pros and cons of having monsters on your plate. Pro: sometimes the monsters talk to you. Con: sometimes sauce gets on the monsters.

1

Add a comment...

People

In his circles

444 people

Communities

8 communities

Places

Currently

Philadelphia, PA

Previously

Washington, DC - Williamstown, MA

Links

Work

Occupation

PhD student

Employment

- University of PennsylvaniaPhD student, 2008 - present

Education

- University of PennsylvaniaComputer Science, 2008 - present
- Williams CollegeComputer Science, 2000 - 2004

Basic Information

Gender

Male

Birthday

January 10

Relationship

Married