7,592 reputation
22841
bio website jozefg.bitbucket.org
location United States
age 18
visits member for 3 years
seen 19 hours ago

I am a student who enjoys type theory, formal verification, and compilers. I blog about [dys]functional things a lot.


Jan
24
awarded  Nice Answer
Jan
22
awarded  Yearling
Jan
21
comment class in OOP language and type
Just a really pendantic note, in PL theory we usually wouldn't state that a type is a set of its values because this doesn't actually work when you add functions + generics. With even fancier type systems you can run into Russell's paradox as well.
Jan
8
comment How much does C help you in other languages?
@Deduplicator Some people call methods or functions in languages procedures because they're a list of imperative instructions rather than a function we'd find in math.
Jan
5
comment Is there a way to write this fold neater in Haskell?
I'd suggest using Maybe rather than an exception here. The type [(Int, Int)] -> Int says to me that this function accepts all lists including empty onces. Rather than rely on documentation we can force the user to be aware of the limitations of this function by saying [(Int, Int)] -> Maybe Int. Force the failure to be explicit especially given the awkwardness of exceptions in Haskell.
Jan
4
awarded  Enlightened
Jan
4
awarded  Nice Answer
Dec
29
comment Can most compilers check for errors?
@DonalFellows Well ish. You can put the burden of proof on the user in which case compilation is proof checking. A much simpler proposition. That's what dependently typed languages do. There's still things you can't prove though because Godel.
Dec
29
answered Can most compilers check for errors?
Dec
12
answered Missing `$` like operators in Haskell
Dec
5
comment Haskell, Rust, or D for POSIX shell implementation?
I'm horribly biased (hence the comment not answer), but I think Haskell or Rust would be lovely for such things. There's some precedence for Haskell with Hell which uses Haskell to create a dsl for shell scripting. Haskell has a nice FFI but Rust's is arguably nicer. I know zip about D though.
Nov
27
comment What is Banana split and fusion in functional programming?
@YannisRizos Good point, I wrote some of the core ideas down :)
Nov
27
answered What is Banana split and fusion in functional programming?
Nov
27
comment What is Banana split and fusion in functional programming?
If you'd permit some self promotion, I wrote a post about this ideas. A banana split refers to banana brackets which indicate a catamorphism. Fusion is an optimization stemming from a theorem about catamorphisms, but the core idea is a generalization of folds.
Nov
20
awarded  Nice Answer
Nov
20
comment type infered statically typed languages?
@Jules Actually that's not quite true, there's a fascinating type of type system called a linear type system which can ensure that each malloc matches one and only one free at compile time. Rust sports a version of such a type system
Nov
20
comment type infered statically typed languages?
@MichaelKohne Anything undefined is what a PL theorist means by "goes wrong" or "gets stuck". In practice of course the program does something. It's just that what happens isn't predictable so it's bad. A well typed program in C can go wrong, so it isn't type safe.
Nov
19
revised type infered statically typed languages?
added 221 characters in body
Nov
19
answered type infered statically typed languages?
Nov
19
comment Why do functional programs have a correlation between compilation success and correctness?
@faif Expanded my answer. TLDR: everyone is a mathematician.