11
$\begingroup$

Fixpoint of type addition or type multiplication is no big deal. You just need to store data in heap. Haskell does this well for lists for example:

data [a] = [] | a : [a]

Yet Haskell also permits fixpoint of type exponentiation. I'll take the following example:

newtype FixPower = FixPower {appFixPower :: FixPower -> Bool}

Some examples of values of this type include:

example1 = FixPower (\_ -> False)
exmaple2 = FixPower (\_ -> True)
example3 = FixPower (`appFixPower` example1)
example4 = FixPower (`appFixPower` example4)
example5 = FixPower (not . `appFixPower` example5)
example6 = FixPower (join appFixPower)

I cannot even grasp how these values are stored in hardware. I don't see how to imitate this type in (relatively) low-level languages such as C. Does this involve some unsafe casting of function pointers? Or is there some other way?

$\endgroup$
2
  • 1
    $\begingroup$ Just because C has no spelling for it doesn’t mean it can’t exist. Function pointers are all the same in the hardware. $\endgroup$
    – Bbrk24
    Commented May 23, 2023 at 2:56
  • 1
    $\begingroup$ OP posted a similar question on StackOverflow 2 years ago, if that's interesting to anyone: stackoverflow.com/q/68735804 $\endgroup$
    – pxeger
    Commented May 23, 2023 at 12:21

1 Answer 1

7
$\begingroup$

In GHC Haskell:

  • FixPower has kind Type
  • Type is a synonym of TYPE LiftedRep
  • LiftedRep is a synonym of 'BoxedRep 'Lifted
  • BoxedRep indicates that this object is represented by a pointer
  • Lifted indicates that the pointer may be a lazy computation, not just a value
  • (->) is a synonym of FUN
  • FUN has kind forall r1 r2. TYPE r1 -> TYPE r2 -> Type
  • In this case, r1 and r2 are both instantiated to LiftedRep as well

Therefore, FixPower is a closure thunk pointer, whose underlying function pointer takes a pointer of the same description, and returns a Bool thunk pointer.

If we ignore laziness and closures, and just focus on the essence of the function itself, a translation to C is surprisingly direct:

typedef struct FixPower {
  bool (*app)(struct FixPower);
} FixPower;
// FixPower (const False)
bool const_false(FixPower fp) { return false; }
FixPower example_false = (FixPower){ .app = &const_false };
// FixPower (const True)
bool const_true(FixPower fp) { return true; }
FixPower example_true = { const_true };
int main(int argc, char **argv) {
  bool result = example_true.app(example_false);
  printf("%s\n", result ? "true" : "false");
  return 0;
}

Does this involve some unsafe casting of function pointers?

No, you do need a struct in order to be able to express a self-referential type definition in C, just as you need a newtype in Haskell. But C has no problem with it, as long as the type is finite in size—which is so, if the self-reference goes through an indirection, as in a more familiar case like a linked list:

struct Node {
  int value;
  struct Node *next;
};

In FixPower, the pointer just happens to be a function pointer, rather than a data pointer. Note that we can pass struct FixPower by value to the function call, since it’s just a function pointer, which has a fixed and finite size. This is really the essence of representation-hiding: sizeof(T *) is independent of sizeof(T).

Another way of thinking of this type, and hyperfunctions more generally, is as a chain of cooperatively scheduled coroutines, navigating over a tree of possible computations.

A FixPower value represents a label for a computation, which is passed a “next routine” label by its caller. It can return a result back up the tree to its caller—in this case just a Bool, but in general it could be any value. Before the routine returns, it has the chance to yield down the tree to the next routine, as many times as it likes. And each time it yields, it’s allowed to decide which routine will be “next” for that subtree.

$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .