Reputation
15,403
Top tag
Next privilege 20,000 Rep.
Access 'trusted user' tools
Badges
38 81
Newest
 Nice Answer
Impact
~138k people reached

Feb
7
comment `f_equal` isn't doing anything
The type valid m_value = true and valid n_value = true are propositionally equal, which means that the type (valid m_value = true) = (valid n_value = true) is inhabited by some p. But they are not judgmentally equal, an so from x : valid m_value = true we cannot conclude x : valid n_value = true. Instead we get to conclude that the transport of x along p has type valid n_value = true. Have you looked at homotopy type theory? There these things are explained carefully (and also why things are done this way).
Feb
6
revised `f_equal` isn't doing anything
added 99 characters in body
Feb
6
answered `f_equal` isn't doing anything
Jan
26
comment Is there a result in computability theory that does not relativize?
Good question :-)
Jan
8
comment Misunderstanding the Church-Turing thesis?
I tell my students that modern computers are Universal Turing Machines, as long as we're willing to buy more RAM as needed.
Nov
17
awarded  Nice Answer
Nov
14
comment Status quo of category theory and monads in theoretical computer science research?
You should know a bit about universal algebra and/or Lavwere's theory of algebraic theories. If you are not familiar with typing rules then you could study a general textbook on programming languages, such as Benjamin Pierce's TAPL or Bob Harper's Practical foundations of programming languages.
Nov
13
comment Status quo of category theory and monads in theoretical computer science research?
I asked Matija to fix the link, in the meantime you could look at arxiv.org/abs/1203.1539.
Nov
13
revised Status quo of category theory and monads in theoretical computer science research?
added 529 characters in body
Nov
13
answered Status quo of category theory and monads in theoretical computer science research?
Nov
13
comment Status quo of category theory and monads in theoretical computer science research?
Before we answer this question: it is not research-level is it? It may be better suited for cs.stackexchange.com.
Oct
19
comment How to implement a functional programming language efficiently?
Sorry, this is still not a research-level question, nor is it clear what you're asking. Now it looks like you're really asking about resource management for functional languages, i.e., you are worried about allocation of environments and the heap, but at the same time you are confounding your problem with an alleged solution, i.e., that if we could get rid of the environments and the heap then the problems would go away. Can you describe the problem you would like to solve (and possibly the motivation), without interleaving it with a solution?
Oct
19
awarded  Enlightened
Oct
19
awarded  Nice Answer
Oct
19
revised Applications of “Seemingly Impossible Functional Programs”
deleted 10 characters in body
Oct
19
comment How to implement a functional programming language efficiently?
Thanks for rephrasing. Now it's not a research-level question anymore :-) I recommend that this be migrated to cs.stackexchange.com where we'll provide some standard references and point out that functional programming languages are compiled efficiently on today's hardware. (I can come up with an infefficient way of compiling while-loops, too.)
Oct
18
comment How to implement a functional programming language efficiently?
A closure is an implementation concept, as well as heap, so it makes no sense to say "functional programming (FP) language without closures". At best you could say "an implementation of a FP language without closures", in which case we can answer that there are implementations of FP which do not use closures. I think you need to rephrase your question. Perhaps you are asking whether a FP language with only first-order functions is complete? That would make more sense, but then you need to be precise about what primitive types you admit. If you put in nat it'll be Turing complete.
Sep
29
awarded  Nice Answer
Sep
23
awarded  Good Answer
Sep
15
awarded  Good Answer