1. 2

In a purely nominative type system, values are members of a type if and only if they are declared to be members of that type. For example:

TYPE amount = integer;
VAR a amount, i integer;

Would declare a and i as distinct types; integer values could not be assigned to a and amount values could not be assigned to i (how one constructs values of either type is not relevant at this point).

Languages like Pascal, Go, and Oberon are nominatively typed. C/C++ is too, but not as strictly.

However, even in languages like Pascal, Go, and Oberon, function/procedure types are still structural.

Take this Oberon-ish example:

TYPE callback = PROCEDURE (i : INT) : BOOL;

You could then assign any procedure that takes a single integer argument and returns a boolean value to a variable of type callback, even if there is no nominative declaration that the given procedure is of that type.

Is there a good way around this? My reading of the literature seems to say no. Obviously, one could simply do something like:

PROCEDURE Foo(i : INT) RETURNS BOOL IS callback
...
END

But that seems silly since it would be an inherently different mechanism for value construction that those for simple types. It rapidly gets uglier if you admit first-class functions.

The best I could come up with would be something along the lines of “allow Smalltalk-like blocks that are assigned to variables of named type”, but that just raises the question of how to construct and type the blocks: they would still be essentially structurally typed.

So, is there any literature that anyone could point me to? Have there been any languages with 100% nominative typing that admitted procedure/function types?

This thought experiment arose after reading up on Tutorial D, which has strict nominal typing (along with an elegant constructor/selector/constraint mechanism) but does not admit function/procedure types.

  1.  

  2. 3

    There’s no reason you couldn’t invent some new type that has the type system rules you want. The reason functions are typically handled structurally is because it’s typically what you want and you can recover nominal typing if you need it. Just wrap a structurally typed thing in a nominally typed container. For example, instead of a function, use an interface/class with a method.

    1. 2

      Just wrap a structurally typed thing in a nominally typed container.

      Like how Java did it before the addition of lambdas to the language. The problem there is that there has to be a way to declare the “function type” inside the nominally typed thing. If your system has structs, you could have a function in a struct…but how do you declare the type of the member of the struct without resorting to structural typing?

      If you have objects/classes where the function becomes a method of the class, that’s pretty close to working. The problem there for me is that there’s no classes in the type system that I’m thinking of. I realize that’s adding constraints after the fact, so it’s not really a fair objection. :)

      1. 3

        there’s no classes in the type system that I’m thinking of

        Just as you can embed a structural type in to a nominal context, you can embed a nominal type in a structural context. In fact, one way of looking at things is that nominal typing is really just the combination of structural typing plus “brands”, where brands are a special case of dependent types with type generativity. In the case of classes, the type depends on the value of the class name and the act of declaring a class generates a new class ID (some fully qualified name, or some gensym, or a memory address, whatever). So rather than adding classes to recover nominal typing, you can just add a pair of type-level operations for generating a brand and for embedding a brand in to a structural type.

        For example:

        class C {
          method: (int) -> int;
        }
        

        can be:

        brand C;
        
        struct S {
          static field = constant(C);
          method: (int) -> int;
        }
        

        Your solution doesn’t need the full generality of a “constant” evaluation form, or “literal types” or anything like that. Just trying to illustrate the idea.

    2. 2

      Go 1.9 introduced type aliases:

      type callback = func(int) bool
      
      func filter(xs []int, f callback) []int {
      	var filtered []int
      	for _, x := range xs {
      		if f(x) {
      			filtered = append(filtered, x)
      		}
      	}
      	return filtered
      }
      
      func main() {
      	fmt.Println(filter([]int{1, 2, 3, 4}, func(x int) bool {
      		return x < 3
      	}))
      }
      

      C# has delegate types:

      public delegate bool callback(int x);
      
      public static int[] filter(int[] xs, callback cb) {
          var filtered = new List<int>();
          foreach (int x in xs) {
              if (cb(x)) {
                  filtered.Add(x);
              }
          }
          return filtered.ToArray();
      }    
      
      public static void Main() {
          int[] xs = {1,2,3,4};
          foreach (int x in xs) {
              Console.Write(x + " ");
          }
          Console.WriteLine();
      }
      
      1. 2

        Excellent point, but the actual parameters still end up being structurally typed. The formal parameters get named as instances of the type, but the actual values when constructed are not declared to be of that type.

        That is, in your first example, I could do something like this:

        func foo(i int) bool {
            ...
        }
        
        filter(int_array, foo)
        

        The function foo was never explicitly declared to be of type callback, but rather assignment/passing was allowed because foo met the structural requirements of the callback type.

        I think the answer to my question may be “no, it’s not possible to reasonably have function types in a purely nominative type system” though that just rubs me the wrong way.

      2. 1

        This Ian opaque/transparent existential types. You can see some good exploration of this in OCaml and it works the way you want: it can be either structural or nominative depending on whether the information exists locally to treat the alias as transparent. These aliases work uniformly over any type, function or not.