8,470 reputation
22945
bio website jozefg.bitbucket.org
location United States
age 19
visits member for 3 years, 4 months
seen 11 hours ago

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


May
8
comment Functional programming and Text adventures
I think Chris Marten's research would be interesting, it aims to show how to make interactive fiction in declarative languages nice. github.com/chrisamaphone/interactive-lp
May
1
answered Haskell types for functions
Apr
7
comment difference between generics and interfaces
This seems related
Mar
23
awarded  programming-languages
Mar
22
answered Is higher-rank parametric polymorphism useful?
Mar
21
comment Is it possible to “bake dimension into a type” in haskell?
@BenjaminHodgson You can't do dependent types with templates because you cannot simulate a pi type. The "canonical" dependent type must would claim you need is Pi (x : A). B which is a function from A to B x where x is the argument of the function. Here the return type of the function dependents upon the expression supplied as an argument. However, all of this can be erased, it's compile time only
Mar
17
awarded  Enlightened
Mar
17
awarded  Nice Answer
Mar
16
revised Why C# is not statically typed but F# and Haskell are?
added 32 characters in body
Mar
16
awarded  Nice Answer
Mar
16
answered What is the reason of using an interface versus a generically constrained type
Mar
13
comment Missing `$` like operators in Haskell
@BenjaminHodgson GHC can't assume that you actually obey the type class's laws though. Somewhere, some (probably mean) person has a codebase relying on a broken functor :/
Feb
16
comment Why are language features more popular than compiler design?
Well that's not the case. If you choose the AST to be assembly for an architecture then pretty much every language does indeed target the same base. If you're wondering why have different languages at all: well there are certain language features that are just not compatible. You can't have general recursion and termination, it's just not possible. Different languages are necessarily different chunks of some Platonic language of computation because it's contradictory to glom everything together into one thing.
Feb
9
comment Using uniqueness types to implement safe parallelism
I think you should look into linear types for parallelism. IIRC uniqueness types are built on linear types. Frank Pfenning has some interesting stuff on the subject
Feb
9
awarded  Nice Answer
Feb
8
comment Is a programming language a set of programs or a set of instructions?
@FredOverflow Fixed, it now reads "catch before runtime"
Feb
8
revised Is a programming language a set of programs or a set of instructions?
added 4 characters in body
Feb
8
revised Is a programming language a set of programs or a set of instructions?
added 63 characters in body
Feb
8
comment Is a programming language a set of programs or a set of instructions?
@RobertHarvey Not necessarily :) There's a very rich field of using a programming language we don't know how to implement (Martin Lof Type Theory + Univalence) to prove interesting things about math. We also use unimplemented programming languages in proof theory or other areas of logic
Feb
8
comment Is a programming language a set of programs or a set of instructions?
@Tim Pretty much any formal treatment of programming languages is split along these lines because that's how all interesting theorems work.