The Stack Overflow podcast is back! Listen to an interview with our new CEO.

Hot answers tagged

13

You should be more precise. When you say that f(x), f a and m >>= f are "the same", that does not make sense as written. f(x) and f a cannot be the same, they do not even use the same variables. Did you mean to compare f(u), f u and u >>= f? It is true that f(u) and f u are the same thing, but u >>= f is not. If f has type a -> m b (...


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 ...


8

One obvious counterexample is a binary search tree. You cannot freely substitute the values in a binary search tree because a substitution might change the ordering (relative to Ord), or even replace the values with a type which is not an instance of Ord at all. A possibly less-obvious example is a contravariant endofunctor. Consider: data Tricky a = ...


6

Let me try to answer your question, I may be mistaken, so check it out first: Let's first state the definition of foldl: foldl :: (a -> b -> a) -> a -> [b] -> a foldl h b x = case x of [] -> b (x:xs) -> foldl h (h b x) xs Now, we aim to prove that, given f:: A -> B, g:: A -> C -> A, h:: B -...


6

The set-theoretic intuitions can make sense in the semantics, especially in the context of realizability semantics (where types are interpreted as sets of terms). In this case, the polymorphic type $\forall \alpha. \mathrm{Maybe}(\alpha)$, written Maybe a in Haskell, intuitively corresponds to the intersection over every type $T$ of the elements of $\mathrm{...


6

Proofs in Haskell? Okay, first let's talk about the Curry-Howard correspondence. This says that one can view theorems as types and proofs as programs. However, it says nothing about which specific logic a particular programming language represents. In particular, Haskell lacks dependent types. That means that it can't express statements with "forall x" or "...


6

The usual encoding of booleans, due to Church, is $$ {\sf true} = \lambda x. \lambda y. x \qquad {\sf false} = \lambda x. \lambda y. y $$ Roughly, "true" is the function which takes two arguments $x,y$ (first takes $x$, then also takes $y$) and returns the first one. Instead, "false" returns the second one. If-then-else is then encoded as applying an ...


6

Consider the simply-typed $\lambda$ calculus: this is one of the simplest functional languages you can define. It is very common to interpret it in a Cartesian closed category (CCC). Indeed, CCCs are the "ideal" categorical setting where to interpret simple types. CCCs, being categories, admit morphisms composition and identity. Taking your definition of "...


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 ...


5

Your goal is to “prove” --I'm using bullets “•” for syntactic separators-- $$ ∀x \;•\;\; ∃y \;•\;\; y² ≤ x < (y+1)²$$ Proof Methods In the natural deduction style, one proves “∀ x : ℕ • P x” by proving two statements: Base case :: P 0 Inductive step :: P a ⇒ P (S a) , for a : ℕ and S successor function Where, in this case, $$P x \;\;≡\;\; ∃y \;•...


5

Your question sounds redundant to me. By definition of category whenever two morphisms with common object $f\colon A \rightarrow B$ and $g\colon B \rightarrow C$ exist, then their composition $g\circ f \colon A \rightarrow C$ must exists as another arrow in that same category. (otherwise, that situation is just not a category.) So the redundant part in your ...


5

If I understand you question correctly, you are wondering how the typing judgment $f : \forall \alpha. \alpha \to \alpha \vdash f\;f : \beta$ can be proved, where $\beta$ is some (yet unknown) type. As we are dealing with an application, the only rule that applies is T-App, so we end up with the following (partial) typing derivation, where $\gamma$ is yet ...


4

The "fraction"-style notation is an inference rule in natural deduction style. See What is this fraction-like "discrete mathematics"–style notation used for formal rules?. $v_1,\dots,v_n\vdash \cdots$ means "in the environment $v_1,\dots,v_n$, such-and-such is true". (It's not an "or", and it doesn't mean "implies".) See What does ⊢ mean in ...


4

In it's simplest, original form, $[\![f\ x \ y]\!]$ just means $\eta(f)\circledast x \circledast y$ where $\circledast$ is what Haskell calls <*> and $\eta$ is what Haskell calls pure. Of course, this is only type correct if $x$, and $y$ have types like $\mathcal{F}(\dots)$ where $\mathcal{F}$ is an applicative functor. If they don't, we can be a bit ...


4

A pretty easy way to see if $t$ generalizes $u$ if $u$ matches $t$: replace all variables in $u$ by (fresh) constants, written $u_c$, and check if $u_c$ unifies with $t$. If so, then there is a substitution $\sigma$ such that $t\sigma\equiv u$ which means by definition that $t$ is more general than $u$. As mentioned in the comments, if $\mathrm{mgu}(t,u)$ ...


4

tl;dr: we can show that they are in fact isomorphic. Defining two different instances over them does not make them different. Defining two different functions over two types does not make them non-isomorphic! The instances are not describing an initial algebra structure, the data keyword is. As you say, the two instances play no role in the specification of ...


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

As a starting note, the rules are syntax-directed: there's only one rule for each language construct. This means that you can construct the typing proof from the bottom up, by always using the rule for the syntactic construct at the bottom of the program. The only uncertainty is what types to use. To do the type inference manually, use variables where you ...


3

To explain why I'm uncomfortable with Newsham's and (especially) Piponi's data wrappers ... (This is going to be more question than answer, but perhaps it'll work towards explaining what's wrong with my IsNat even though it seems very similar to Newsham.) Piponi page 17 on has: data Proposition = Proposition :-> Proposition | Symbol ...


3

So, while this question seems Haskell specific at first glance, I think it touches on enough aspects of modern Programming Languages theory and research that there's a good CS-general answer here. As DW says, it's impossible to automatically verify that an implementation satisfies the Functor laws, by Rice's theorem. However, strongly-typed languages give ...


2

By Rice's theorem, this is undecidable in general.


2

Yes, it is definitely possible. However your approach is a good starter but keep in mind to have a functional approach on writing code in Haskell. You can create expressions so you can define and 'override' methods. As a suggestion I will give a part of code of how such expressions can look like as values and types. data Exp = Lit Value | Assign ...


2

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 ...


1

It's possible with this: https://blog.jle.im/entry/verified-instances-in-haskell.html. We need several extensions and the Singleton library. And your functor become like this: {-# LANGUAGE MagicHash, RankNTypes, PolyKinds, GADTs, DataKinds, FlexibleContexts, FlexibleInstances, TypeFamilies, TypeOperators, TypeFamilyDependencies, ...


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