CODEWITHSUNDEEP
haskellfree-theorem
NietzscheanAI
NietzscheanAI

Reputation: 966

Finding a "free theorem"

How do I derive the free theorem for the type:

data F a = C1 Nat | C2 Bool Nat a

where Nat is simply data Nat = Z | S Nat?

In principle, this can be answered by the Haskell 'free-theorems' package, but it's too elderly to compile under any GHC version I can reasonably install.

Upvotes: 2

Views: 276

Answers (1)

Joachim Breitner
Joachim Breitner

Reputation: 25763

There is an online generator for free theorems at, and when it was down a little while ago I created an alternative UI that runs completely in the browser (using reflex-dom).

But the deeper problem is that free theorems, in the sense of these packages, are properties of polymorphic functions, so in order to answer your question, you have to give a function (like map) whose free theorem you are interested in.

Upvotes: 6

Related Questions