Trying to formalize the type of first class pattern matching in JS

typeofmatch.hs

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}

import Data.Proxy
import Data.Kind

type family Uncurry as x where
  Uncurry '[] x = x
  Uncurry (a ': as) x = a -> Uncurry as x

type family Constructors (d :: [(k, [*])]) x where
  Constructors '[] _ = '[]
  Constructors ('(k, as) ': d) x = ('(k, Uncurry as x) ': Constructors d x)

data Obj o where
  Empty :: Obj '[]
  With :: Proxy k -> v -> Obj o -> Obj ('(k, v) ': o)

type Match d i = forall o. Obj (Constructors d o) -> i -> o
data ADT d x = ADT { match :: Match d x, constructors :: Obj (Constructors d x) }

type DNatF a = '[ '("Z", '[]), '("Succ", '[a])]

intAsNat :: ADT (DNatF Int) Int
intAsNat = ADT match constructors where
  match :: Match (DNatF Int) Int
  match (With _ z (With _ succ Empty)) i = if i == 0 then z else succ (i - 1)

  constructors :: Obj (Constructors (DNatF Int) Int)
  constructors = With Proxy 0 (With Proxy (\n -> n + 1) Empty)

display :: Int -> String
display = match intAsNat (With Proxy z (With Proxy succ Empty)) where
  z = "Zero"
  succ i = "(Succ " ++ display i ++ ")"

main = print $ display 5
-- => "(Succ (Succ (Succ (Succ (Succ Zero)))))"

typeofmatch.js

const { adt, match } = require("@masaeedu/adt");
const { Arr } = require("@masaeedu/fp");

// :: type Fix f = f (Fix f)

// :: type Algebra f a = f a -> a
// :: Functor f -> Algebra f a -> Fix f -> a
const cata = F => alg => {
  const rec = x => alg(F.map(rec)(x));
  return rec;
};

// :: type Coalgebra f a = a -> f a
// :: Functor f -> Coalgebra f a -> Fix f -> a
const ana = F => coalg => {
  const rec = x => F.map(rec)(coalg(x));
  return rec;
};

// :: type Uncurry '[]         x = x
// ::      Uncurry '[a, ...as] x = a -> Uncurry as x

// :: type Constructors '{}               _ = '{}
// ::      Constructors '{ [k]: a, ...o } x = '{ [k]: Uncurry a x, ...(Constructors o) }

// :: type Match d i = forall o. Constructors d o -> i -> o

// :: type ADT d v = '{ match: Match d v, ...(Constructors d v) }

// :: type ADTValue '{}               = ⊥
// ::      ADTValue '{ [k]: c, ...o } = '{ label: k, values: c } | ADTValue o

// :: type Base (Fix f) = f

// :: Functor (Base a) -> ADT d a -> ADT d b -> a -> b
const fromADT = F => A => B => cata(F)(A.match(B));
// :: Functor (Base b) -> ADT d a -> ADT d b -> a -> b
const toADT = F => A => B => ana(F)(A.match(B));

// :: adt :: Rep d -> ADT d (ADTValue d)

// Test 1
{
  // :: type DNatF a = '{ Z: '[], Succ: '[a] }
  // :: type NatF a = ADTValue (DNatF a)

  // :: forall a. ADT (DNatF a) (NatF a)
  const Nat = adt({ Z: [], Succ: ["a"] });
  const { Z, Succ } = Nat;

  // :: Functor NatF
  const NatF = { map: f => match({ Z, Succ: v => Succ(f(v)) }) };

  // :: type Nat = Fix NatF

  // :: ADT (DNatF Number) Number
  const Num = (() => {
    const Z = 0;
    const Succ = n => n + 1;
    const match = ({ Z, Succ }) => n => (n === 0 ? Z : Succ(n - 1));

    return { Z, Succ, match };
  })();

  // :: Nat -> Number
  const num2nat = toADT(NatF)(Num)(Nat);
  // :: Number -> Nat
  const nat2num = fromADT(NatF)(Nat)(Num);

  console.log(nat2num(num2nat(5)));
}

// Test 2
{
  // :: type DListF x xs = '{ Nil: '[], Cons: '[x, xs] }
  // :: type ListF x xs = ADTValue (DListF x xs)
  // :: forall x xs. ADTValue (DListF x xs) (ListF x xs)
  const List = adt({ Nil: [], Cons: ["x", "xs"] });
  const { Nil, Cons } = List;

  // :: Functor ListF
  const ListF = { map: f => match({ Nil, Cons: x => xs => Cons(x)(f(xs)) }) };

  // :: type List = Fix ListF

  // :: [a] -> List a
  const arr2list = toADT(ListF)(Arr)(List);
  // :: List a -> [a]
  const list2arr = fromADT(ListF)(List)(Arr);

  // :: [Number]
  const l1 = list2arr(arr2list([1, 2, 3, 4, 5]));
  console.log(JSON.stringify(l1));
}