Re: Next meeting?

[Lyle Kopnicky]

I'll let Matt speak to the slots, but I would love to hear presentations on those. I've heard a few on Agda but never heard of Idris, so I would vote for Idris as the lesser-known.

- Lyle

On Fri, Nov 9, 2012 at 9:30 AM, Caylee Hogg <cayle...@gmail.com> wrote:

So I had to run shortly after 9, but was there discussion of when the next meeting will be and what topics are to be had? If there's open slots, I could always talk about Agda or Idris.

--
Z
---
You received this message because you are subscribed to the Google Groups "Zissou Society for Programming Language Exploration" group.
To post to this group, send email to pdx...@googlegroups.com.
To unsubscribe from this group, send email to pdxlang+u...@googlegroups.com.
Visit this group at http://groups.google.com/group/pdxlang?hl=en-US.
 
 

[Matt Youell]

On Fri, Nov 9, 2012 at 9:30 AM, Caylee Hogg <cayle...@gmail.com> wrote:

So I had to run shortly after 9, but was there discussion of when the next meeting will be and what topics are to be had? If there's open slots, I could always talk about Agda or Idris. 

Our next meeting will be sometime in February/March.

Right now the agenda is wide open. We'd love to have you talk. I'm with Lyle, I'd favor Idris for the same reason. Agda is practically mainstream! :)

[Matt Youell]

While I'd love to see more discussion on this list, the theme is programming language exploration. Let's stick with that. Personal queries are best left to direct email.

Thanks for understanding.

Matt

[Echo Nolan]

I'd like to hear more about dependent types. Can we do a worked example of proving a bijection between the naturals and integers or something?

[Matt Youell]

On Sat, Nov 10, 2012 at 1:30 PM, Echo Nolan <ec...@echonolan.net> wrote:

I'd like to hear more about dependent types. Can we do a worked example of proving a bijection between the naturals and integers or something?

I'm interested in the intersection between dependent types and pattern matching. Personally, I'd rather see a more practical demonstration than a bijective proof. Text manipulation or something. IANACS :)

[Joe Groff]

Chris Double has some informative articles about ATS, a systems programming language with several advanced type system features including dependent and linear types that compiles to C:

http://www.bluishcoder.co.nz/tags/ats/

His examples are of the more practical "build a provably memory-safe device driver" than theoretical "construct Church numerals" sort, so they might be what you're looking for.

-Joe