mmirman / caledon Goto Github PK
View Code? Open in Web Editor NEWhigher order dependently typed logic programing
License: Other
higher order dependently typed logic programing
License: Other
For example, the following will stall when lpn
is reached.
defn list : prop → prop
>| nil = list P
>| cons = P → list P → list P
defn lp : {P : prop} list P → prop
| lpn = lp nil
| lpc = {l : list P} {e : P} lp l → lp (cons e l)
By changing that line to | lpn = lp {P = P} nil
, the stalling doesn't happen, but I think Caledon should be smart enough to know that P
can't be inferred and report an error instead of stalling.
As an aside, this glitch doesn't occur for this program;
defn num : prop
>| zero = num
>| succ = [n : num] num
defn list : prop -> prop
>| nil = list P
>| cons = P -> list P -> list P
defn append : {P : prop} list P -> list P -> list P -> prop
| nila = {l : list P} append nil l l
| nilc = {l m n : list P} {a : P} append l m n -> append (cons a l) m (cons a n)
defn length : {P : prop} list P -> num -> prop
| lengthn = length nil zero
| lengthc = {l : list P} {e : P} {n : num} length l n -> length (cons e l) (succ n)
nor this program
defn num : prop
>| zero = num
>| succ = [n : num] num
defn list : prop -> prop
>| nil = list P
>| cons = P -> list P -> list P
defn last : {P : prop} list P -> P -> prop
| lastn = {e : P} last (cons e nil) e
| lastc = {l : list P} {le e : P} last l e -> last (cons le l) e
defn length : {P : prop} list P -> num -> prop
| lengthn = length nil zero
| lengthc = {l : list P} {e : P} {n : num} length l n -> length (cons e l) (succ n)
but it does occur for this program
defn num : prop
>| zero = num
>| succ = [n : num] num
defn list : prop -> prop
>| nil = list P
>| cons = P -> list P -> list P
defn append : {P : prop} list P -> list P -> list P -> prop
| nila = {l : list P} append nil l l
| nilc = {l m n : list P} {a : P} append l m n -> append (cons a l) m (cons a n)
defn last : {P : prop} list P -> P -> prop
| lastn = {e : P} last (cons e nil) e
| lastc = {l : list P} {le e : P} last l e -> last (cons le l) e
defn length : {P : prop} list P -> num -> prop
| lengthn = length nil zero
| lengthc = {l : list P} {e : P} {n : num} length l n -> length (cons e l) (succ n)
stalling on lengthn. This is an odd glitch which is clearly sensitive to context, but I'm not certain how to describe it beyond these examples.
For whatever reason, the Caledon program will stall, eating up an arbitrarily large amount of memory when encountering certain code which should instead produce syntax errors. Here are some examples of code which, if encountered, will trigger what I'm talking about;
defn unit : prop
as
defn unit : prop
as \(P : prop) P . P
defn unit : prop
as [P : prop] P -> P
defn tt : unit
as \0 p . p
defn unit : prop
| tt =
defn unit : prop
| tt = \(P : prop) . unit
defn unit : prop
| one = unit
a(
A declarative, efficient, and flexible JavaScript library for building user interfaces.
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
The Web framework for perfectionists with deadlines.
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
We are working to build community through open source technology. NB: members must have two-factor auth.
Open source projects and samples from Microsoft.
Google ❤️ Open Source for everyone.
Alibaba Open Source for everyone
Data-Driven Documents codes.
China tencent open source team.