341 reputation
111
bio website
location Lima, Peru
age 27
visits member for 3 years, 10 months
seen yesterday

Subject is a functional programming and type theory nerd. The extent to which mathematical thinking has affected subject has not been fully assessed yet, but the brain damage is known to be quite serious already. In particular, subject's ability to communicate with other programmers (such as his coworkers) is severely hampered by his tendency to talk about abstract concepts in terms of themselves rather than in terms of examples.

Subject has expressed hope that a language will be developed with the following features:

  1. as concise as GHC Haskell (at least for the non-proof parts of his programs)
  2. as modular as Standard ML (also add applicative functors)
  3. as pedantic about correctness as Coq (without the admit tactic)
  4. compiles to native binaries as fast as C (with pointers marked as "restrict" whenever possible, and preferring direct system calls to libc calls)
  5. a comprehensive standard library of data structures and algorithms, in the spirit of C++'s STL, but better

Subject has been observed talking about what he calls "deep" analogies between type systems and database schemas. Subject has expressed dismay at the failure of major DBMS implementors to provide sufficiently expressive schemas, alleging that this failure forces him to encode certain business model constraints as database triggers, which he claims is "time-consuming" and "error-prone". Mentioning NoSQL in subject's presence must be avoided at all costs - subject may go on a rampage and cause both material destruction and loss of life.

Subject's outlook on life has been interestingly affected by recent developments, such as his exposure to the Rust programming language, which he now claims has the potential to unify the mathematical elegance of Haskell with the performance focus of C and C++. Subject is probably the only Rust programmer trying to do purely functional programming in Rust. "A Fortran programmer can write Fortran programs in any language. A Haskell programmer will dismiss any language he cannot write Haskell programs in." Rust is one of the few languages subject has not dismissed so far. For some perspective on what this achievement means, especially for a C-family language, the list of languages subject has dismissed includes even the likes of Scala and F#.

Subject goes by the nick "pyon" on both Freenode and Mozilla's IRC network.


Nov
3
answered Is it good practice to catch a checked exception and throw a RuntimeException?
Sep
24
awarded  Autobiographer
Dec
16
comment Are there any implementations of deterministic regular expressions?
@delnan: OTOH, the NFA to DFA transformation is a lot harder, and this is why I write regular expressions whose NFAs are guaranteed to be DFAs without performing any transformation.
Dec
16
comment Are there any implementations of deterministic regular expressions?
@delnan: Those ε-transitions can be eliminated easily, giving a regular NFA. Wherever there is a transation A -ε-> B, consider every transition of the form B -x-> C and insert a transition A -x-> C. Also if B is an accepting state, then so must be A. Now you can remove A -ε-> B. Moreoever, the Thompson construction can be modified to insert the A -x-> C transitions directly, without inserting A -ε-> B in first place.
Dec
16
comment Are there any implementations of deterministic regular expressions?
@KilianFoth: If you come up with a better title, feel free to edit my question. :-)
Dec
16
comment Are there any implementations of deterministic regular expressions?
@KilianFoth: I edited my question to clarify what I mean by "determinstic regular expression". Also, I want an implementation that I can conveniently use in a conventional statically typed programming language, which grep is clearly not.
Dec
16
revised Are there any implementations of deterministic regular expressions?
added 85 characters in body
Dec
16
asked Are there any implementations of deterministic regular expressions?
Sep
8
comment Is functional programming a superset of object oriented?
Errr... C++11 lambdas are hardly first-class functions: Each lambda has its own ad-hoc type (for all practical purposes, an anonymous struct), incompatible with a native function pointer type. And std::function, to which both function pointers and lambdas can be assigned, is decidedly generic, not object-oriented. This is no surprise, because object-orientation's limited brand of polymorphism (subtype polymorphism) is strictly less powerful than parametric polymorphism (even Hindley-Milner, let alone full System F-omega).
Aug
23
comment Which one subsumes the other: class-based object-orientation or prototypal inheritance?
@BenjaminGruenbaum: Sorry, I meant to say that two languages being Turing-completeness is not enough to guarantee that one can replicate the operational semantics of the other.
Aug
23
comment Which one subsumes the other: class-based object-orientation or prototypal inheritance?
The operational semantics of C++ member functions and a struct full of function pointers are completely different.
Aug
23
comment Which one subsumes the other: class-based object-orientation or prototypal inheritance?
Syntactic issues aside (my use of object["member"] instead of object.member in the C++ implementation), why would 2 make no sense for static languages? (By the way object["member"] is also legal JavaScript.)
Aug
23
revised Which one subsumes the other: class-based object-orientation or prototypal inheritance?
deleted 391 characters in body
Aug
23
asked Which one subsumes the other: class-based object-orientation or prototypal inheritance?
Aug
5
comment Generic and type safe I/O model in any language
@MattFenwick: What would your sum type look like, then?
Aug
1
comment I have to compromise: DRY, or Command-Query-Separation?
@StefanBilliet: By using the formal semantics of the programming language I am using to show that my program meets the formal specification I have given it. If some part is too critical to rely on myself alone for proving purposes, I write an obviously correct but possibly inefficient implementation in Coq, then I construct another more efficient implementation, and I prove as a theorem that the two implementations produce the same result.
Aug
1
comment I have to compromise: DRY, or Command-Query-Separation?
@StefanBilliet: My point is that testing itself is not a terribly useful activity.
Aug
1
comment I have to compromise: DRY, or Command-Query-Separation?
@StefanBilliet: "Testing can only show the presence of bugs, never their absence." - Dijkstra
Aug
1
comment I have to compromise: DRY, or Command-Query-Separation?
@Lavinski: Is there any tool (say, a Coq library) that provides a formal definition of what CQRS is, and that I can use to certify that a design I may come up with fits the CQRS pattern?
Aug
1
comment I have to compromise: DRY, or Command-Query-Separation?
@Lavinski: Sorry, in my line of work, I need a level of confidence in the correctness of my designs that only mathematics can provide.