3 ms·
> Dependent types > > Example languages: Idris, Agda, Coq > > You’re probably used to type systems in languages like C and Java, > where the compile
by combatentropy 9y ago
> Dependent types
>
> Example languages: Idris, Agda, Coq
>
> You’re probably used to type systems in languages like C and Java,
> where the compiler can check that a variable is an integer, list, or string.
> But what if your compiler could check that a variable is “a positive integer”,
> “a list of length 2”, or “a string that is a palindrome”?
This is what I love about SQL. You can even define your own types, like "email", at least in PostgreSQL:
create table contacts (
name text not null,
age int check (age >= 0),
email email
);
It already has a few of these special types built in, like for IP and MAC addresses (https://www.postgresql.org/docs/current/static/datatype.html https://www.postgresql.org/docs/current/static/datatype.html).
- tathougies 9y agoThe author got the gist of dependent types wrong. It's not simply about checks. Dependently typed languages allow the result type to explicitly depend on the input data. Thus, a dependently typed database would allow one columns type to depend on the value of another column. It would be like saying Create table dep ( name text, fieldType int not null, fieldValue (if fieldType = 1 then int else varchar)) Notice the 'if' in the type of fieldValue
- kornish 9y agoOut of interest, how is common ORM support for custom Postgres types?
- siddboots 9y agoGeoAlchemy for PostGIS/SQLAlchemy is a good example of explicit support. But typically, you can always "deal" with custom types in your ORM, even if that means falling back to binary data.