3 ms·
Probably with a function with a type signature something like this (which is in Agda, another dependently typed language, but the idea holds): nGram : {l :
by joel_ms 10y ago
Probably with a function with a type signature something like this (which is in Agda, another dependently typed language, but the idea holds):
nGram : {l : Nat}{n : Fin l} -> Vec l Char -> n -> List (Vec n Char)
To break it up:
"nGram" is the name of the function
"{l : Nat}" means l is a natural number
"{n : Fin l}" means n is a finite number smaller than l
"Vec l Char" is the first argument, declared as a
vector of characters, with length l
"n" is the second argument (previously declared as
a finite number smaller than l)
"List (Vec n Char)" is the return type, a list which consists
of vectors of characters where each vector is of length n
For an explanation on how and why this works you can check out these papers:
http://www.cse.chalmers.se/~ulfn/papers/afp08/tutorial.pdf http://www.cse.chalmers.se/~ulfn/papers/afp08/tutorial.pdf
http://www.cse.chalmers.se/~peterd/papers/DependentTypesAtWork.pdf http://www.cse.chalmers.se/~peterd/papers/DependentTypesAtWo...
The first is more about programming in Agda while the second goes into how dependently typed languages relate to logic. Together they provide sufficient definitions of Nat, Fin, Vec and List to declare the nGram function.
If you're unfamiliar with ML-style syntax the above definiton probably looks weird, but can be written in a pseudo-java style like this:
List<Vec<N,Char>> nGram<Nat L,Fin<L> N>(Vec<L,Char> input_string, N n){}
- twblalock 10y agoThis makes no sense. No language can know the value of a variable at compile time, unless that variable is a constant. If the function you have defined is passed a string s and an int n, where n is greater than len(s), there is no way the compiler can know that will happen in advance. It will be a runtime error. IllegalArgumentException is also a runtime error. You have not solved anything.
- curryhoward 10y agoActually, joel_ms is correct; you can encode these "dynamic" properties of values in a static type system, in the same way that you can prove properties about a program on paper without actually running it. The connection between programs and proofs [1] is rather mind-blowing to learn about, and unfortunately no popular programming language supports this style of "certified" programming. But there are some interesting languages which do, such as Idris and Coq. [1] https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon...
- joel_ms 10y agoDid you check out the papers I linked to? Because they explain how this "makes sense". Dependently typed languages allow for type-level functions (actually they erase the separation between type-level and value-level). This is why you can define a type like "Fin n" meaning a number smaller than n. "Fin n" is a function that takes one argument "n" and returns a type that limits its values to the set of (natural) numbers smaller than n. Arguably, Agda is more often used as a proof assistant, rather than as a programming language (although I've had the pleasure of watching Ulf Norell implement a limited programming language interpreter in Agda, using non-total functions, which was quite nice.) But Idris is a serious effort to create a language that's both dependently typed and performs decently when used as a regular programming language. If you want to see some real world examples of using dependently typed languages, I would suggest looking at the CompCert C Compiler[0]. It is a C Compiler that's been formally verified using the Coq proof assistant, which is a precursor to both Agda and Idris. Coq is as far as I know the first dependently typed language. To be fair, programming in a dependently typed language usually requires more effort upfront, but the ability to encode properties that are usually considered runtime errors into the type system does seem like an interesting future for programming languages. [0] http://compcert.inria.fr/compcert-C.html http://compcert.inria.fr/compcert-C.html (edit: shout out to the excellently named sibling commenter "curryhoward", IMHO one of the most interesting results in programming language technology and type theory research!)