HN user
Plexes are first mentioned in 1960
https://dl.acm.org/doi/pdf/10.1145/366199.366256
and the paper even starts with a critique of the efficiency of Lisp's approach for representing data with cons pairs (citing McCarthy's paper from the same year).
You might also want to watch Casey's great talk on the history of OOP
Lean[1] Zulip chat[2]
[1] https://leanprover-community.github.io/ [2] https://leanprover.zulipchat.com/
Liquid Tensor Experiment also comes to mind:
https://www.nature.com/articles/d41586-021-01627-2
https://leanprover-community.github.io/blog/posts/lte-final/
Get on Zulip[1] and ask for help when stuck. The community is friendly and has gotten quite large although they are mostly mathematicians at the moment.
Yes for the fragment of total and noncomputable functions which mathematicians use. For partial functions (which Lean also supports) I think the same arguments hold as for the "Haskell Category".
There are definitions for sheaves, Grothendieck topologies and sites[1] which were extensively used in the Liquid Tensor Experiment[2]
[1] https://github.com/leanprover-community/mathlib4/tree/master...
[2] https://leanprover-community.github.io/blog/posts/lte-final/
It still supports sbrk since it's available on WebAssembly but mmap is not.
Cool, I have no idea what the fuck this means and how it is useful to me.
Oh wait, I use them every day.
Do you really? Do the `functions` you use even fit the above definition?
I bet you can think of infinite number of functions (bool -> bool). The above definition admits only 4 such functions.
Lean[0]'s mathlib has quite nice formalisation of category theory[1] with plenty examples of concrete categories even sheaves and toposes.
[0] https://leanprover.github.io/programming_in_lean/#01_Introdu...
[1] https://github.com/leanprover-community/mathlib/blob/master/...
If the focus is on finite data structures only and the equivalence relation is "are the types isomorphic", then each type is isomorphic to the ordinary generating functor with some coefficients C : N->N:
-- ogf(c,x) = Σ n:ℕ, cₙ xⁿ
def ogf (c : ℕ → ℕ) (α : Type) :=
Σ n:ℕ, fin (c n) × (fin n → α)
For example list has coefficients Cn = {1,1,1,1...}
inductive list (α : Type)
| nil : list
| cons (hd : α) (tl : list) : list
inductive bin_tree (α : Type)
| leaf : bin_tree
| branch (x : α) (left : bin_tree) (right : bin_tree) : bin_tree
Computing those coefficients from a type definition is not always trivial though (see the symbolic method http://algo.inria.fr/flajolet/Publications/AnaCombi/book.pdf).
This can be extended to infinite data structures too by switching the natural numbers to ordinal numbers in the ogf definition.
Maybe
int getint(const char **s) {
int res = 0;
for (; **s && isspace(**s); (*s)++);
for (; **s && isdigit(**s); (*s)++)
res = 10 * res + **s - '0';
return res;
}Integer factorization is also reducible to Knapsack:
To factorize integer N invoke a Knapsack solver with knapsack size of log(N) and items of size logarithm of all prime numbers up to sqrt(N): [log 2, log 3, log 5, ...].
If N=pq (say p and q are prime) then log(N)=log(p)+log(q).
So from all possible items in the item set, only log(p) and log(q) will fill the knapsack as tight as possible leaving zero empty space in it.
No suite of tests is complete enough to replace a proof. Unless the domain is finite and the tests exhaust all values in it.
Data flow and perhaps control systems (AI scripts and GUIs built around something declarative and event-driven come to mind) indeed seem to be the only commercially successful examples of visual programming thus far.
I strongly disagree. Here's an incomplete list of commercial software in VFX for visual "programming" for artists:
Houdini by SideFX
Katana and Nuke by The Foundry
Most typed languages have two separate levels: expressions (and statements in imperative languages) and types. Dependent types unify those two levels into one. This allows one to use values in types, or vice versa, effectively making types first class in the sense that functional programming makes functions first class.
As an example this is Haskell's core language:
data Expr b
= Var Id
| Lit Literal
| App (Expr b) (Arg b)
| Lam b (Expr b)
| Let (Bind b) (Expr b)
| Case (Expr b) b Type [Alt b]
| Tick (Tickish Id) (Expr b)
| Type Type
| Cast (Expr b) Coercion
| Coercion Coercion
data Type
= TyVarTy Var
| LitTy TyLit
| AppTy Type Type
| ForAllTy !TyCoVarBinder Type
| FunTy Type Type
| TyConApp TyCon [KindOrType]
| CastTy Type KindCoercion
| CoercionTy Coercion
And this is Lean core language (a dependently type language):
inductive expr
| var : nat → expr
| sort : level → expr
| const : name → list level → expr
| mvar : name → name → expr → expr
| local_const : name → name → binder_info → expr → expr
| app : expr → expr → expr
| lam : name → binder_info → expr → expr → expr
| pi : name → binder_info → expr → expr → expr
| elet : name → expr → expr → expr → expr
| macro : macro_def → list expr → expr
So what's the best type system? Dependent types' answer: the language itself. Instead of having two separate languages, have a single language that acts as its own type system, powerful enough to describe both programs and types. Then types become first class - you can pass them to a function as parameters, or return them as values, or use any function at compile time.
In physics progress usually comes in the form of unification. Two seemingly separate phenomena (say electricity and magnetism) turn out to be described by a single theory. Dependent types provide such a unification between expressions and types in programming languages. Imo definitely a step forward in the noisy sea of programming languages.
That's not even touching the mathematical side of things, Curry-Howard correspondence, proof assistants and using dependent types for proving theorems.
"There are only two hard things in Computer Science: cache invalidation and naming things." -- Phil Karlton
But I do like "Computability and naming things" better.
Going further one will need a word for "the kind of a kind", "the kind of a kind of a kind" and so on.
One solution is TypeInType, that is the type of a type is another type (not kind or something else). That's where Haskell is going with the work of adding Dependent Types to the language.
The problem with TypeInType is that it is logically inconsistent - it leads to Girard's paradox, analog to Russel's paradox in set theory.
The correct solution is type universes where every type lives in some type universe indexed by a natural number. For example terms are of type 'Type 1', 'Type 1' types are of type 'Type 2' and so on. The usual 'Type' is then just the first universe level 'Type 1' and 'Kind' is 'Type 2'.
Type universes is what most proof assistants employ, e.g. Agda, Coq, Lean. Idris uses TypeInType which is easier to use and there's no need to massage your program until all type universes type check but is logically inconsistent so one has to be careful to not reproduce Girard's paradox in some form or another.
`Void` being the uninhabited type, in the light of the Curry-Howard isomorphism stands for a false proposition.
`a -> Void` get interpreted as "not a" or "from a follows contradiction" or equivalently "a is uninhabited". Combinatorially it's `0 ^ a` which for non-empty a is zero but is equal to 1 when a is empty (0^0=1). In other words there are no functions of type `a -> Void` for non-empty a and there's exactly one such function for uninhabited a (id :: Void -> Void).
`Void -> a` is interpreted "from falsehood, anything (follows)" https://en.wikipedia.org/wiki/Principle_of_explosion. Combinatorially a^0 = 1 for all a so there's exactly one such function. An easy way to define it is by induction on Void (which has no cases and you're done).
That's just not true. Functional programming does not eliminate state.
And yet it says so in the first sentence in the Wikipedia page for functional programming https://en.wikipedia.org/wiki/Functional_programming
a style of building the structure and elements of computer programs—that treats computation as the evaluation of mathematical functions and avoids changing-state and mutable data.
But I'll take it that you don't have much functional programming experience.
Of course one can still go with a big global array and keep updating it in-place. A good programmer can write Fortran (or C in that case) in any language.
Trees, graphs?
Of course one can force anything into a relational database. The data analog of "Turing tarpit".
Ironically graph databases are way better for describing relations than relational databases.
Except that functional programming completely eliminates (yet still allows) concern no. 1 in the mentioned order -- state > coupling > complexity > code.
Not to mention the better expressive power for describing data structures with algebraic data types (just + and * for types really).
I agree with everything besides your stated difficulties with infinities in type theory. Here's one infinity
inductive ℕ : Type
| zero : ℕ
| succ (n : ℕ) : ℕ
ℕ → ℕ
From then on one can start talking about different injective functions between those types and infer cardinality of which is bigger and so forth and so forth.
It's values, types and functions all the way down. Nothing from ZFC is lost, on the bright side, your proofs are checked by a computer. On an even brighter side, your proofs can be semi-automated, even brute forced.
Also set theory vs type theory (in Math) is really just dynamic typing vs static typing (in CS). And we already know how that played out in CS.
Not really. The boundaries of type theory (say HoTT) are exactly what is possible on a Turing machine (computable). And a step beyond those throws ZFC itself into paradoxes (say Russel's). Moreover ZFC is directly expressible in type theory https://hott.github.io/book/nightly/hott-online-1174-g29279f...
https://en.wikipedia.org/wiki/History_of_type_theory
Not that much surprised. History of type theory is a history of trying to define precisely computation. That is, try to allow recursion but enforce that all programs terminate.
The solution to this problem these days is to use a purely functional programming language with dependent types (e.g. Homotopy Type Theory, Lean).
Haskell, for example, being a practical functional programming language, is logically inconsistent. Using the fix function:
fix :: (a -> a) -> a
fix f = let x = f x in x
Prelude Data.Function> :t fix id
fix id :: a
In a logically consistent functional language such as Lean https://leanprover.github.io, this definition is not allowed.
So you think the key for understanding constructive logic is to understand some peculiar syntax.
It's not only a syntax, it's a functional programming language which turns out to be a computational model for logic.
The key to understanding logic constructively goes through type theory, not philosophy.
I'll just leave this here https://78.media.tumblr.com/bfc158b432199a3e4f5de2ddc1bd7381...
Reminds me of the evolution of Lua https://www.lua.org/history.html from a configuration language to a full blown programming language.
Awhile ago, we've used this code as data approach in a game development studio for everything. For example, maps/levels were stored as a Lua scripts that get executed on load and contain a sequence of PlaceObject, SetProperty, etc invocations.
It doesn't come without drawbacks, though. For example, Autodesk Maya stores scenes as Mel code (as a bunch of createNode, connectAttribute, setAttribute commands). This script gets executed on load in a single thread (utilizing a single from your N cores) and scene loading can take ~30 min on large scenes. Security is also an issue but it's fixable with proper environment sanitation and sandboxing.
Of course you can. The good old {-# LANGUAGE OverlappingInstances #-}.