# Tag Info

12

This is a suggested "interpretation" of the IO monad. If you want to take this "interpretation" seriously, then you need to take "RealWorld" seriously. It's irrelevant whether action world gets speculatively evaluated or not, action doesn't have any side-effects, its effects, if any, are handled by returning a new state of the universe where those effects ...

5

Your Haskell encoding fails to capture proofs in propositional calculus (which is what the book you referred to does). The failure is not due to your using Haskell, but because of your encoding evaluation of Boolean values instead of proofs, and these are two completely different things. When people speak about "Haskell proving things" they mean the ...

4

The expression case e of p1 -> e1 p2 -> e2 ... can be rewritten as let k p1 = e1 k p2 = e2 ... in k e where k is a fresh identifier. This translation assumes that the language has some way to define a local function by pattern matching (e.g. let). If local functions can not be defined, there's always the possibility of lifting the ...

3

I don't know what rule Jones intended to use, but I'd guess it's something like $$\dfrac{ \Gamma' = \Gamma,x_1:\tau_1,\ldots,x_n:\tau_n \\ \Gamma' \vdash e_1 : \tau_1 \\ \cdots \\ \Gamma' \vdash e_n : \tau_n \\ \Gamma' \vdash e : \tau }{ \Gamma \vdash {\sf let}\ x_1=e_1;\cdots;x_n=e_n\ {\sf in}\ e : \tau }$$ which handles mutual recursion in groups. The ...

3

The meaning of curry can be easier to be seen when the type signature is written as curry :: ((a, b) -> c) -> (a -> b -> c) that is, a function taking a single parameter of type (a, b) and yielding a result of type c is turned into a function taking two separate values of types a and b yielding the same result type c. We might define curry for ...

1

By being corecursive between the types, you indeed get a representation of a grammar, and it does have binding. But now you've sort of "baked in" the unembedding by making it "definitionally id". (This is similar to the Place constructor in Fegaras and Sheard). So you can evaluate to Value. But what if you want to evaluate to anything else? You can't, ...

1

Question 1 Does the bracketed "(v o)" in the Vehicles context refer a type constructor and its argument, rather than two independent types? In the constraint Surfaces v o, v and o are two separate type arguments to class Surfaces. Constraint Paths a b (v o) has three arguments: a, b, (v o). The third is v applied to o, so we can infer parameter v to ...

Only top voted, non community-wiki answers of a minimum length are eligible