Foxp

Enabling pseudo Dependent Types --- foxp🦊 does type-check div-by-zero, type-safe get/upd, range-of-number, sized-array, email-with-regex and more, ...and more, as needed.

Try it:
Playground | Source

Installation

pnpm - pnpm add @taiyakihitotsu/foxp
npm - npm install @taiyakihitotsu/foxp

Usage

import { foxp } from '@taiyakihitotsu/foxp'

💡 Philosophical Note: Static-First Design

Foxp focus strictly on compile-time verification.
It does NOT provide runtime validation logic or error handling.

If it type-checks, it is guaranteed to be safe under the defined preconditions.
There is no runtime overhead for checking; the "magic" happens entirely within the TypeScript compiler.

See DEV.md if you want to see the details.

Basic Example

test/doc/basic-example.ts

All built-in functions are higher-order and accept optional pre-conditions. If you provide nothing, defaults are used.

And values must be wrapped with put*. Pick its value via the .value property.

const div = foxp.bi.div()

// => 3/2
const t0 =
  div(
    foxp.putPrim(3)
  , foxp.putPrim(2)).value

// => Error but success to catch at the type-check.
  div(
// @ts-expect-error:
    foxp.putPrim(3)
  , foxp.putPrim(0)).value

If a value violates a pre-condition, Foxp replaces the argument type with never at the type level.
This "Type-Level Firewall" ensures that the code will not compile, preventing any potentially unsafe execution.

Merging Pre-conditions

test/doc/merging-pre-conditions.ts

You can merge pre-conditions using tuples of the same length as function arguments. Use empty strings '' to skip merging for an argument.

// NOTE: To keep a default pre, see `t3` pattern.
type Merged = foxp.pre.MergeTuple<[foxp.pre.Greater<2>, foxp.pre.Less<4>]>
const div = foxp.bi.div<Merged>()

// => 3/3
const t0 =
  div(
    foxp.putPrim(3)
  , foxp.putPrim(3)).value

const t1 =
  div(
// @ts-expect-error:
    foxp.putPrim(3)
  , foxp.putPrim(9)).value

const t2 = 
  div(
    foxp.putPrim(3)
  , foxp.putPrim(0)).value

If you want to keep a default, get it with foxp.pre.bi.* and then merge them.

type NewMerged = foxp.pre.MergePreStr<Merged, foxp.pre.bi.div>
const newdiv = foxp.bi.div<NewMerged>()

const t3 = 
  newdiv(
// @ts-expect-error:
    foxp.putPrim(3)
  , foxp.putPrim(0)).value

Lambda

test/builtins/lambda.ts

The first function is unary.
The second needs anonymous function, with foxp.putSym.
The third and fourth are the same structure of built-ins.

You can define custom preconditions as Lisp S-expressions in this situation.

const lambdatest0 = (n: number) => add()(foxp.putPrim(1), foxp.putSym('n', n))

const lambdatestr0n  = lambda<'n', 'neg-int?'>(1)(lambdatest0)()(foxp.putPrim(-1))

const lambdatestr1nf =
  lambda<'n', 'neg-int?'>
    (1)
    (lambdatest0)
    ()
// @ts-expect-error:
    (foxp.putPrim(1))

Higher order function

test/sample/higher-order-fn.ts

⚠️ Beta Notice: This is currently a temporary API designed to remain faithful to TypeScript's behavior where functions are first-class objects.

The HOF (Higher-Order Function) API and some internal type-evaluators are currently in Beta.
The syntax (including runHof) is subject to change as we explore more ergonomic ways to align with TypeScript's native functional patterns.

This is somewhat tricky. You should call runHof, a type-level closure to earn env, and push every results into it.

const hof = foxp.bi.hof
const add = foxp.bi.add
const sub = foxp.bi.sub
const runHof = foxp.bi.runHof

const define_hof3 =
  hof<'o', foxp.pre.NegInt>(1)(
    (o: number) =>
      hof<'m', foxp.pre.PosInt>(1)(
        (m:number) => (
          hof<'n', foxp.pre.Num>(1)(
            (n: number) =>
              ( sub
                  ()
                  (foxp.putSym('o', o)
                , add
                    <foxp.pre.MergeTuple<[pre.Greater<5>, pre.Greater<9>]>>
                    ()
                    ( foxp.putSym('m', m)
                    , foxp.putSym('n', n))))))))

const runHof2_value_r0 = define_hof3.value.fn(foxp.putPrim(-1))
const runHof2_value_r1 = runHof2_value_r0.value.fn(foxp.putPrim(6))
const runHof2_value_r2 = runHof2_value_r1.value.fn(foxp.putPrim(10))

const runHof2_engine   = runHof()
const runHof2_engine_r0 = runHof2_engine(runHof2_value_r0)
const runHof2_engine_r1 = runHof2_engine_r0(runHof2_value_r1)
const runHof2_engine_r2 = runHof2_engine_r1(runHof2_value_r2)

Other Sample

See test/sample

Lens

test/builtins/get-in.ts

You should foxp.ro if you want to use nested data.

const map_getIntest_nest_with_ro_leaf =
  getIn<pre.getIn>()
    ( foxp.putRecord(foxp.ro({a: [0,2], b: 2} as const))
    , foxp.putVec([':a', 1] as const))

const map_getIntest_nest_out_of_bound0 =
  getIn<pre.getIn>()
// @ts-expect-error:
    ( foxp.putRecord(foxp.ro({a: [0,2], b: 2} as const))
    , foxp.putVec([':c'] as const))

Range

test/sample/numrange.ts

const tested_num = foxp.putPrim(3)
type tested_pre = pre.Range<0,10>

const testnum0_ok = bi.inc<tested_pre>()(tested_num)

const testnum0_ffailure =
  bi.inc<tested_pre>()
// @ts-expect-error:
    (foxp.putPrim(20))

Vect

test/sample/vect.ts

const tested_vec = foxp.putVec(foxp.ro([0, 1, 2] as const))

const testvect0 = bi.first<pre.VectN<3>>()(tested_vec)
const testvect0_ffailure =
  bi.first<pre.VectN<3>>()
// @ts-expect-error:
    (foxp.putVec(foxp.ro([0, 1] as const)))

Regex

test/sample/email.ts

type email = `'(([^<>()[\\].,;: @"]+(\\.[^<>()[\\].,;: @"]+)*)|(".+"))@((\\[[0-9]{1,3}\\.[0-9]{1,3}\\.[0-9]{1,3}\\.[0-9]{1,3}\\])|(([a-zA-Z0-9-]+\\.)+[a-zA-Z]{2,}))'`
const test_refind0 : Cion.Lisp<`(re-find ${email} '[email protected]')`> = `'[email protected]'`
const test_refind1 : Cion.Lisp<`(re-find ${email} 'https://github.com/taiyakihitotsu/foxp/tree/main')`> = "''"

const email_str = foxp.putPrim('[email protected]')
const not_email_str = foxp.putPrim('https://github.com/taiyakihitotsu/foxp/tree/main')
// identity function usable for type checking
const email = foxp.tid<foxp.pre.IsEmail>()(email_str)
// @ts-expect-error:
const notemail = foxp.tid<foxp.pre.IsEmail>()(not_email_str)

Core Concept

Foxp🦊 wraps values into objects that carry both the value and a type-level representation (S-expression).
Pre-conditions are executed using CionLisp to perform type checks at compile time.

For a detailed explanation of how Foxp🦊 lifts TypeScript values to Cion Lisp and checks types, see DEV.md.

builtins

Core API: foxp

put* and ro is used for general values to pass into a function of foxp.bi.

• putPrim --- wrap primitive values
• putVec --- wrap vectors
• putRecord --- wrap records
• putFn1 --- wrap unary functions
• putSym --- used only with lambda / hof
• tid --- identity with checking
• tap1 --- apply unary function with checking
• ro --- readonly for nested data.

Builtin Functions: foxp.bi

They all are almost copied from Clojure Core Builtins.

• fn, lambda, hof
• Arithmetic : add(+), sub(-), mul(*), div(/)
• Data : assoc, assoc-in, update, update-in, get, get-in
• Compare : gt (>), lt (<), eq (=), gte (>=), lte (<=)

Pre-conditions: foxp.pre

They are pre-conditions or Type Function to generate them.

Types starting with a lower-case are pre-condition. With a upper-case, they are type function to return a pre-condition type.

• Eq, Vect, NotZero, Greater, Less, Interval, EmailRegex
• assocLax, assoc (for update / assoc-in / update-in too.)
• MergePreStr, MergePreTuple --- merge preconditions

Pre-conditions: foxp.pre.bi

• Pre-conditions for foxp.bi

More builtins and preconditions are planned.

Pre-conditions are Lisp S-exprs; you can write them directly as string, e.g. 'neg-int?'

FAQ & more

Feel free to open issues for questions. See DEV.md for developer documentation.

Author

taiyakihitotsu

LICENSE

3-clause BSD license