I'm working on a toy language, intended as a functional implementation of Date and Darwen's vision for a 'D' language to compete with SQL.
Right now, I'm considering how far to go with the ideas in Turner's Total Functional Programming.
Distinguishing data from codata and statically enforcing termination is pretty much entirely a win for this language, I think. Nearly all of the functions and IwishtheywerefunctionsSQLviewsqueriesprocedures I have in any of my example databases are structurally recursive or have entirely opaque implementations.
Some questions I am stuck on:

Where do the function types fall on this distinction? They are codata, right, because you can only observe them by applying (~= deconstructing) them? (As an aside, if so, is it possible to write a Turnerstyle codata declaration that starts
codata (>) a b =
? I'm not sure if the answer is yes, no, or not without referencing the builtin (>) type.)

It seems like equality and serializability, both obviously of interest to a database language, are sensibly defined for precisely those types that are data "all the way down" (counting function types as codata types). True, false, or trueishbutdistinguishthemanyway?

There is a weird thing that happens to function types when the following conditions are met:
 The argument type and result type are both data types
 The argument type is "finitely inhabited" (I'm not sure what the real name of this concept is) in that it classifies finitely many values.
data DayOfWeek = Monday  Tuesday  Wednesday  Thursday  Friday  Saturday  Sunday
is finitely inhabited, as are Haskell's Int
and even Float
, but neither Integer
nor [DayOfWeek]
When this happens, the (necessarily total) functions magically look like data again. Taking t to be the cardinality of the type t, a > b = b ^ a when these conditions are met. At least in principle (it might take a long time in some or most cases), we can compare functions of such a type for (extensional) equality by evaluating them at every inhabitant of the argument type. We can serialize them by (there may be more efficient ways, but who cares) serializing this table of results. What's happening here? Could/should a language recognize this special case and allow serializing functions with types like DayOfWeek > Bool
? Or provide conversions to/from Map a b
from/to a > b
if and only if these conditions hold? Or ignore this whole thing as an oddity?
Recent comments
1 hour 47 min ago
3 hours 32 min ago
11 hours 49 min ago
11 hours 49 min ago
12 hours 24 min ago
13 hours 59 min ago
16 hours 17 min ago
19 hours 6 min ago
19 hours 43 min ago
20 hours 32 min ago