hiker
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
[1] https://leanprover-community.github.io/ [2] https://leanprover.zulipchat.com/
https://www.nature.com/articles/d41586-021-01627-2
https://leanprover-community.github.io/blog/posts/lte-final/
[1] https://github.com/leanprover-community/mathlib4/tree/master...
[2] https://leanprover-community.github.io/blog/posts/lte-final/
> 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.
[0] https://leanprover.github.io/programming_in_lean/#01_Introdu...
[1] https://github.com/leanprover-community/mathlib/blob/master/...
-- 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.
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;
}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.
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
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.
But I do like "Computability and naming things" better.
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.
`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).
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.
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.
Not to mention the better expressive power for describing data structures with algebraic data types (just + and * for types really).
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.
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.
It's not only a syntax, it's a functional programming language which turns out to be a computational model for logic.
I'll just leave this here https://78.media.tumblr.com/bfc158b432199a3e4f5de2ddc1bd7381...
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.