How to implement dependent types in 80 lines of code

• nbe

  1 1 2.5 Scala

Neat! Somewhat similar approach in Scala: https://github.com/julesjacobs/nbe/blob/main/src/main/scala/tt2.worksheet.sc

• wlang

  4 3 10.0 TypeScript

  a language that compiles to C (by willow385)

You can do something kind of similar in Typescript using kind of similar syntax: https://github.com/DanteFalzone0/wlang/blob/main/src/Types.ts

• InfluxDB

  www.influxdata.com featured

  Power Real-Time Data Analytics at Scale. Get real-time insights from all types of time series data with InfluxDB. Ingest, query, and analyze billions of data points in real-time with unbounded cardinality.

  

• elaboration-zoo

  23 562 5.3 Haskell

  Minimal implementations for dependent type checking and elaboration

Thanks, yeah, I haven't benchmarked the implementation yet, and I see the repeated substitution happening. Would the NbE approach where we have indices for terms and levels for values fix the issue (I believe you wrote the implementation here)?

Suggest a related project