[combatentropy]

  > 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).

[tathougies]

The 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]

Out of interest, how is common ORM support for custom Postgres types?

[siddboots]

GeoAlchemy 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.