Lambda the Ultimate

Any type should be nullable, e.g., Nullable◅Integer▻, which is different from Nullable◅Nullable◅Integer▻▻.

Haskell, and similar functional languages have:

data Maybe t = Nothing | Just t

So you can have "Maybe Integer" or "Maybe String". Apart from syntax, this looks identical to Nullable.

Edit: my point being that separating nullability from the underlying type seems to be widely accepted as a good idea.

What I don't see in the ActorScript version is any kind of value level tag to discriminate the union. In Haskell's Maybe, you clearly have the value-constructors "Just" and "Nothing".

A Nullable◅T▻ can only be un-nulled to an Actor of type T in order to avoid have nulls as Actors.

What is the value of a nullable type that is null and how is this distinguished from a non-nullable value. In Haskell the datatype definition for Maybe defines the values "Nothing" and the value constructor "Just x". So the same is true of the Haskell definition, there is no null type, only a null-value.

This of course can be extended to concepts like " Either":

Either x y = Left x | Right y

This is often used for error handling where a function may return either an error of type y or the answer of type x. You can see that Nothing is just a special case of "Left x" where we have no error data to return.

What should the examples at top of this LtU topic look like?

It would be interesting to see a different approach.

Nullable is a very special kind of discrimination that deserves its own treatment.

How is it treated specially. Special treatment seems a bad idea to me. Every time you treat something specially it makes the world more complex and less general. The most beautiful theories say the most with the least special cases. For example E = mc^2, or the Euler identity. Nullable just seems to a a regular discriminated union to me.

Nullable◅aType▻ should be very simple and obviously secure, e.g., the examples at the top of this LtU topic ;-)

Nil in Objective C can be perilous in that it can result silent failure.

Option types can have Nothing, None, etc. which may be just as bad as Null :-(

Void is an Actor that does not receive any messages, i.e., it is not defined how to send a message to Void.

So what is Null (as opposed to Null Integer, which is of type Nullable◅Integer▻)?

Null is an error with no message. See above, its a special case of the discriminated union "data Either x y = Left x | Right y" where 'x' is 'Void'.

Hence if 'x' == 'Void' the above reduces to:

data Either x y = Left x | Right y 

substitute x = Void:

data Either y = Left Void | Right y

simplify:

data Maybe x = Nothing | Just x

so Nothing = "Left Void" of a discriminated union.

Another way to think of it, is "Nothing" is polymorphic over all "Maybe" types. Without polymorphism you might have to write:

Maybe<Integer>.Nothing

But thanks to polymorphism and type inference, we can just write "Nothing" and the compiler will figure out which type of nothing it is. We could represent this as a function:

Nothing :: forall t . Maybe t

And interestingly, because the function has no inputs, there is only one possible definition of a function with this type. Of course if we never access the 'Just' value of the Maybe, we never need to know what the type of 't' is.

As far as I can tell, the difference between the ActorScript type system and a Haskell like type system is that that ActorScript type system would require 't' to be grounded, even if it is not used, whereas in Haskell 't' can be a universally quantified type, providing we do not access the value.

This leads on to the question: "What's wrong with universally quantified types?". Do you want to start another thread to discuss this, or if it has already been discussed do you have a link to the conversation?

Tony's whole point was that Null/Nothing are harmful.

There is no difference between Haskell's Maybe and what you are suggesting, except ActorScript forces the type parameter to be grounded.

What does it mean for a type parameter to be grounded?

It means it cannot be free. In other words my understanding is in ActorScript "Nothing<T>" is not really a type, but "Nothing<String>" is a type. In Haskell "forall T . Nothing<T>" is a type, but of course the only value is _|_ (bottom). Here's a Haskell example of a term:

second (id, 2) 

has the type "Int", but the "id" in it has the type "forall a . a -> a".
An example using "Nothing"

let x = Nothing in case x of
    Nothing -> True
    otherwise -> False

Here the maybe type is never fully defined, but as we never access the value "Just y" the type variable can be free "forall t . Maybe t", so the above Haskell code is accepted even though all the type variables are not grounded. Another (more useful) example would be polymorphic recursion.

Claim: ⊥ is not a type in the foundations of Computer Science.

Claim: Also, there are no nonconstructive types, e.g., Any is not a type.

Claim: All types are constructive, e.g, using the rules in Inconsistency Robustness in Foundations.

I was referring to the value of bottom, being the subtype of all types, given "forall T . T", the only value it can contain is the value in the bottom type, which is empty.

If you don't have subtyping, then there is no bottom, but I was using it casually to refer to that which is common to all types.

Bottom for a specific language may not be empty of course. For example every type in a language could be printable, in which case you could call print on an ungrounded type. This of course is just a special case of type-classes, where every type is a member of "printable".

Edit: Any is a type in some type systems, so I have difficulty with unqualified statements like that above. If you want to be taken seriously, you should say "Any is not a type in the ActorScript type system".

⊥ is this value.

 may be what you are referring to ;-)

Claim: There is no extension type of all types in foundations.

No such thing is needed and can be harmful.

If you don't have subtyping

aType is plainly and obviously a subtype of Nullable◅aType▻, for example.

If you want to be taken seriously, you should say

You were not confused. Why are you being dictatorial? Is your writing style to be taken as exemplary?

Claim: Integer is not an extension of Nullable◅Integer▻.

Nor is Nullable◅Integer▻ an extension of Integer.

Integer is not an extension of Nullable◅Integer▻.

Every Integer can be cast to a Nullable◅Integer▻.

Does Java allow a cast from Integer to Optional◅Integer▻?

In ActorScript, the following is of type Nullable◅Integer▻:

Nullable 3

Note: ActorScript does not allow subtyping of an implementation so that an implementation can be securely branded. However, multiple implementations can be used in another implementation.

Of course, interface types can be extended :-)

Note: ActorScript does not allow subtyping of implementations so that implementations can be securely branded. However, implementations can be used in other implementations.

Mathematically I expect to identify Integer objects with the corresponding Nullable◅Integer▻ objects, just as I'd identify ℕ objects with reals.

In ActorScript I think this would be reflected in the definitions of equality and arithmetic operators over the two types.

That's all I mean by "subtype" in this context.

Where's my error?

1 plus a Nullable◅Integer▻ can throw an exception.

If you are willing to put up with the exceptions, you can use nullables in your arithmetic operators.

Yeah, obviously, but the operators when domain-restricted to the subtype are identical to the subtype operators. Not sure what else "subtype" should mean, here.

Pick your poison between f and g below.

f.[x:Nullable◅Integer▻]:Integer ≡
  x � ⦾Null ⦂  SomethingElse.[ ] ⍌
       ⦾n ⦂ 1+n▮

g.[x:Nullable◅Integer▻]:Integer ≡
  Try 1+x
     catch� IsNull[ ] ⦂ SomethingElse.[ ]▮

There are many type systems where 'Any' is a type, for example intersection type systems with 'omega'. So the claim that 'any' is not a type, without qualification, is wrong.

Making such obviously incorrect claims results in people who have studied other type systems immediately stopping taking this seriously.

Claim: Type Any has many problems, e.g., it is not constructive and allows free-floating Y fixed point.

Also type intersection systems have many problems, e.g., vacuous types.

Type Any is not needed in mathematical foundations of Computer Science.

Intersection type systems may have problems, but they still exist, and to imply they don't exist seems poor form.

I have no problems with the restatement above, and agree that intersection type systems have problems.

Making such obviously incorrect claims

There are (roughly) two readings to what Hewitt said that you object to.

One is a prima facia absurd reading which is clearly not meant.

The other is perfectly sensible, albeit arguable.

Why do you consistently pick the absurd one?

"Any is not a type." seems fairly unambiguous to me. I find it hard to read past such claims. It feels like an attempt to own the term 'type' without respect to other peoples work and other type systems.

I also suggest that from following other threads that these kind of claims are partly responsible for the difficulty in getting people interested this topic, and I would like to help improve that situation.

I can read past such claims inserting "in ActorScript" to myself, but that runs the risk of missing more profound and wide-reaching claims that affect all type-systems.

Type Any is not constructive and allows the free-floating Y fixed point.

I have no problems with that statement either. It seems to me that this is true for all type systems. Hence why it is problematic to mix generally applicable statements like this with "Any is not a type" which is specific to ActorScript.

Type Any is not needed in mathematical foundations of Computer Science.

This does seem problematic, however my intuition is that this may be the case, and yet the Peano-Dedekind axioms assume an 'any' type which is constrained by the axioms. It seems there is an implicit any type, and that concerns me. Why is Any okay implicitly in second order logic.

Higher-kinded functions require universal quantification, which is a kind of any type:

any :: forall t . t

Of course this does not behave like omega in intersection type systems.

Type Any is not needed for Peano/Dedekind axioms for ℕ; only Boolean^ℕ is needed.

What is "N"? If you do not presuppose N, then it is any type, constrained by the axioms? What other way is there of interpreting N?

ℕ is axiomatized by the Peano/Dedekind categorical axioms which can be found in the LtU archives.

The axioms are explained here.

It is not constructive, and the axioms act as constraints on an implicit "any" type. The any is implicit in the structure of second order logic, it does not occur as an explicit type. It is not needed, yet it is unavoidable.

Peano/Dedekind induction axiom is quantification over Boolean^ℕ, not over Any.

Doesn't the fact that it is a single model up to isomorphism imply that any model that is isomorphic satisfies the axioms. Therefore there might be infinite concrete models that are isomorphic. Isn't this a kind of constrained universal quantification? Such that we are saying 'T' can be any type as long as it is part of a model that complies to the axioms? This is remarkably similar to type classes, where we have a constrained universally quantified type.

Edit: This paper seems interesting https://www4.in.tum.de/~wenzelm/papers/axclass-TPHOLs97.pdf
It shows how to represent type-classes in higher-order-logic. What is not clear is whether all of higher-order-logic is encodable as type classes, or if not, whether all of higher-order-logic necessary for the foundations of computer-science can be encoded in type classes.

feels like... an attempt to own the term 'type' without respect to other peoples work

That must feel strange.

I can only explain how it comes across to me, as I can't speak for what the intention was. I was referring to feeling in the emotional sense.

Claim: Anything useful can be expressed using parameterized types.

Are there any known counterexamples to the above claim?

Polymorphic recursion is the most obvious thing that you can't do using parameterised types. Did you respond to "What is wrong with universal quantification"? I am interested in why you have gone a different way from other type systems?

Leaf and Fork can be defined as extensions of Tree using:

Actor Leaf◅aType▻[aTerminal:aType]
   extends Tree◅aType▻ using
       getHash[ ]:Integer → Hash◅aType▻.[aTerminal]
       getTerminal[ ]:aType → aTerminal▮

Actor Fork◅aType▻[aLeft:Tree◅aType▻, aRight:Tree◅aType▻]
   extends Tree◅aType▻ using
       getHash[ ]:Integer → Hash◅aType▻.[aLeft.getHash[ ], aRight.getHash[ ]]
       getLeft[ ]:Tree◅aType▻ → aLeft
       getRight[ ]:Tree◅aType▻ → aright▮

where

Interface Tree◅aType▻ with getHash[ ]↦Integer▮

A classic polymorphic recursion example is to have two types, I will try and use ActorScript style notation:

Z
S<T>

It is important these are types not values. So we can now construct types with integer values:

S<S<S<Z>>>

These should also have constructors MkS and MkZ.

The above is a type representing the number three. Now we want a function that can be passed a number as a value that returns it as a type, the one restriction is we cannot return the type because it will fail to unify, so the number type is 'returned' by passing to a continuation, in Haskell the complete example looks like:

{-# LANGUAGE RankNTypes #-}

-- type definitions.
data Z = MkZ
data S t = MkS t

-- This type-class is so we have something to do with the number type.
-- it converts a type number to a value.
class ToValue t where
    toValue :: t -> Int
instance ToValue Z where
    toValue MkZ = 0
instance (ToValue t) => ToValue (S t) where
    toValue (MkS t) = 1 + toValue t

-- polymorphic recursion to lift a number to a type
toType :: Int -> (forall u . ToValue u => u -> Int) -> Int
toType x f = toType' x MkZ f where
    toType' :: ToValue t => Int -> t -> (forall u . ToValue u =>  u -> Int) -> Int
    toType' 0 a f = f a
    toType' x a f = toType' (x - 1) (MkS a) f

-- call poly recursion with value 3 and continuation
-- round trip, value to type back to value and print.
main = do
    putStrLn $ show $ toType 3 toValue

I am not sure the ActorScript type system can cope with higher-ranked types at all?

How can Poly Recursion can do the Fork example above?

Yes. See (to save time in writing an example myself): http://stackoverflow.com/questions/2199891/creating-polymorphic-recursive-types-in-haskell

For a more thorough treatment see: http://itrs04.di.unito.it/papers/hk.pdf

I will try and write the exact example when I get a few minutes (maybe using string concatenation to avoid having to define the hash functions).

Since you didn't do the job, I have tried to decipher this stuff.

It's not looking good :-(

My current attempt is below based on Creating polymorphic recursive types in Haskell, which was recommended by Keean Schupke (above).

data TypeLeaf(aType, dummyType) = Leaf(dummyType(aType))

data TypeFork(aType, dummyType) = Fork(dummyType(aType, aType))

data TypeTree(aType, dummyType) =  
    Leaf(dummyType(aType)) | Fork(dummyType(aType, aType))

newtype Leaf(dummyType) = Leaf(dummyType(TypeLeaf, dummyType)) 

newtype Fork(dummyType) = Fork(dummyType(TypeFork, dummyType))

newtype Tree(dummyType) = Tree(dummyType(TypeTree, dummyType))  

The following is an example of a tree:

Tree(Fork(Tree(Leaf(Integer(1))), Tree(Leaf(Integer(2)))))

PS. The above code doesn't yet do the messages getHash[ ], getLeft[ ], or getRight[ ] :-(

Edit: The above code is wonderfully recursive! But it manifestly lacks something in practice :-(

Here's my first attempt, you have to use type-classes if you want to pattern match on types, otherwise it works just like the polymorphic recursion example:

{-# LANGUAGE RankNTypes, FlexibleInstances #-}

data Fork x y = MkFork x y
data Leaf x = MkLeaf x

myTree = MkFork (MkLeaf "a") (MkLeaf "b")

class ToString t where
    toString :: t -> String
instance ToString (Leaf String)  where
    toString (MkLeaf x) = x
instance (ToString x, ToString y) => ToString (Fork x y) where
    toString (MkFork x y) = toString x ++ toString y

main = do
    putStrLn $ toString myTree

The type of "toString" is "forall t . (ToString t) => t -> String".

Are you unable to completely and exactly do the example?

Well I used 'toString' instead of 'hash' i don't see that being a significant difference. The other difference using a ToString class instead of Tree is not significant either, but I can rewrite with a Tree and the same methods when I can get to a computer later.

Here's my second attempt, using getString instead of getHash still, but defining Fork as an instance of Tree with the interface getString, getLeft, and getRight, which I think is equivalent to the example:

{-# LANGUAGE RankNTypes, FlexibleInstances, TypeFamilies #-}

data Undefined
data Fork x y = MkFork x y
data Leaf x = MkLeaf x

class Tree t where
    type LeftType t :: *
    type RightType t :: *
    getString :: t -> String
    getLeft :: t -> LeftType t
    getRight ::  t -> RightType t

instance Tree (Leaf String)  where
    type LeftType (Leaf String) = Undefined
    type RightType (Leaf String) = Undefined
    getString (MkLeaf x) = x
    getLeft _ = undefined
    getRight _ = undefined

instance (Tree a, Tree b) => Tree (Fork a b) where
    type LeftType (Fork a b) = a
    type RightType (Fork a b) = b
    getString x = getString (getLeft x) ++ getString (getRight x)
    getLeft (MkFork x _) = x
    getRight (MkFork _ y) = y


myTree = MkFork (MkLeaf "a") (MkLeaf "b")

main = do
    putStrLn $ getString myTree

How did polymorphic recursion become so convoluted :-(

It is not really very convoluted, lets compare like for like:

Actor Fork◅aType▻[aLeft:Tree◅aType▻, aRight:Tree◅aType▻]
   extends Tree◅aType▻ using
       getHash[ ] → Hash.[aLeft.getHash[ ], aRight.getHash[ ]]
       getLeft[ ]:Tree◅aType▻ → aLeft
       getRight[ ]:Tree◅aType▻ → aright▮

with

instance (Tree a, Tree b) => Tree (Fork a b) where
    type LeftType (Fork a b) = a
    type RightType (Fork a b) = b
    getString x = getString (getLeft x) ++ getString (getRight x)
    getLeft (MkFork x _) = x
    getRight (MkFork _ y) = y

The definitions of the three 'get' functions look very similar. The main difference is because Haskell does not have dependent types, we have to define the type-level functions (LeftType and RightType) separately from the value level functions. I think the clear separation of type level from value level makes some things easier to understand than with dependent-types (the ActorScript type system appears to be a form of dependent-type system to me).

It's interesting how polymorphic recursion can turn implementations into pretzels :-(

The principal difference is in the syntax. In Haskell you define "data Fork x y = MkFork x y" where the left hand side is the type constructor, and the right hand side the value constructor, such that (MkFork 2 "a") has type "Fork Int String". If a function is passed a Fork you access the contents by pattern matching so that "f (MkFork x y) = x" would be 2 from the above definition, and "f (MkFork x y) = y" would be "a". These differences account for most of the difference in syntax between the actor-script version and the Haskell version.

The other big difference is the separation of the type level functions LeftType and RightType. This is because in order to type check a function that uses a "Tree" we require all the type equations be known at compile time. If the types of a function using Tree depend on the instance passed (Leaf or Fork) we cannot type check program modules separately at compile time, because another module might extend Tree with a new type that breaks the type safety of our function. The way Haskell uses type families as associated types avoids this problem.

I don't see how ActorScript could be implemented as a practical safe compiled language because of this. You can have any two, it can be practical unsafe and compiled, impractical safe and compiled (no separate compilation or runtime dynamic loading), or practical safe and interpreted.

Claim: ActorScript can provide specifications for safe, practical, very efficient implementations.

It is fairly widely agreed that a language needs to support separate compilation to be practical with large projects.

It is also widely accepted that type safety requires compile time checking that prevents type errors at runtime.

Both of the following can be separately compiled:

Actor Leaf◅aType▻[aTerminal:aType]
   extends Tree◅aType▻ using
       getHash[ ]:Integer → Hash◅aType▻.[aTerminal]
       getTerminal[ ]:aType → aTerminal▮

Actor Fork◅aType▻[aLeft:Tree◅aType▻, aRight:Tree◅aType▻]
   extends Tree◅aType▻ using
       getHash[ ]:Integer → Hash◅aType▻.[aLeft.getHash[ ], aRight.getHash[ ]]
       getLeft[ ]:Tree◅aType▻ → aLeft
       getRight[ ]:Tree◅aType▻ → aright▮

How can you compile an actor that uses the Tree actor without access to both of those? You have the same problem as C++ templates, you need to see all the definitions to compile any code. There is also no separation of interface and implementation.

Tree is an interface type; not an implementation type Of course, Tree is an Actor.

But Tree knows nothing about Leaf and nothing about Fork :-)

Yes, I can see that is true in this case as the types from 'Fork' are never exposed. It works for simple cases where the return type is a 'simple' type, or one of the type parameters of the interface.

But what if you wanted to expose getLeft and getRight as part of the interface?

The messages getLeft and getRight are in the Fork implementation type signatures.

Can you add getLeft and getRight to the interface so that an external actor can iterate over the tree?

Messages getLeft and getRight are in the signature of the implementation type Fork:

Fringe◅aType▻.[aTree:Tree]:[aType*]  ≡ 
   aTree � 
     aLeaf↓Leaf ⦂ [aLeaf.getTerminal[]]
     aFork↓Fork ⦂ [⩛Fringe.[aFork.getLeft[]], ⩛Fringe.[aFork.getRight[]]]▮

What I am trying to understand is what happens if you have an interface were the return type of a procedure depends on the actor you pass a message to. For example:

interface Test where
    test[] : ???

actor A extends Test using
    test[] : Int -> 3

actor B extends Test using
    test[] : String -> "test"

What is the type of 'test' in the interface?

The Signature return type can be an interface or discrimination allowing flexibility in what is actually returned.

I prefer Haskell's case syntax:

fringe<t>.[tree:t]:[t] = 
   case tree {
      leaf : Leaf -> [leaf.getTerminal[]]
      fork : Fork -> concat.[fringe.[fork.getLeft[]], fringe.[fork.getRight[]]]
   }

You also need to concat the lists, otherwise you end up with nested lists.

⩛ implements appending, concatenating, etc. in both expressions and patterns.

yes, I found it in the book. Personally I would rather just have a actor that concatenates, as the semantics of \|/ seem problematic, it has to know not just about its argument, but its context. It doesn't seem straightforward to implement \|/ as an actor, if it is possible at all?

⩛ is unified notation in both expressions and patterns

How do you implement it as an actor though?

⩛ is notation like other notation in ActorScript expressed in Unicode.

That's an odd concept for a programming language. If everything is an actor, it should be an actor. Personally I would rather use the existing actor mechanism:

concat.[list1, ... listN]

Would seem better to me, with a mechanism for messages with a variable number of arguments. Concat would then be a standard library actor, rather than special syntax.

If there were a way to use actors in pattern matches, like Haskell's guard syntax, then you would not lose any functionality, you can get rid of the special syntax, and you can use other user-defined actors in the same way in pattern matches.

As "getHash" is used in both "Leaf" and "Fork", it may have the type, "Leaf t -> Integer" or "Fork a b -> Integer", you effectively have an intersecion type:

getHash :: Leaf<a> /\ Fork<a> -> Integer

Intersection types cause all sorts of problems.

getHash is a message and *not* a type.

And what is the type of the messsage? Data in transit should by typed, so that both receiver and sender agree on the type.

The type of the getHash message is as follows where ⨀ is the name qualifier:

Message◅getHash⨀Tree[ ]↦Integer▻

Does that mean because you qualify the 'Tree' type by the 'value' getHash, that this is not statically checkable? I don't really understand what that value name is doing in the type. I probably need to read a bit more of the book, but intuitively it does seem like it needs to depend on run-time information, and therefore checking needs to be deferred until runtime.

It also seems like it is doing something similar to a type-class where you might have:

forall t . (Tree t) => t -> Integer

Which means t is a universally quantified type, constrained by the type-constraint "Tree t". This type could be wrapped in a message type:

Message (forall t . (Tree t) => t -> Integer)

Note because the universal quantification is inside the Message type, this is an existential-type, and this means you cannot recover the type of 't' from the container, you are strictly limited to only using the 'Tree' interface to the type, and that is not allowed to 'leak' the type of 't'.

getHash⨀Tree says which particular getHash using name qualifier⨀

So the message must contain a tag that tells the receiver which 'getHash' is in the message. This is what I mean by not statically checkable. If types are completely checkable statically, you can use type-erasure to remove all types from the actual runtime code.

The Haskell method would include the type-class dictionary in the message along with the data payload. Now the receiver does not need to know the type of the 'getHash' in the message, provided it uses only the specified interface. This means all instances of the class have to share the same method types, and hence why you need to have a single definition of getHash in the 'Tree' class in my latest Haskell implementation.

An Actor of type Tree only accepts getHash⨀Tree messages

A tree can be a Fork or a Leaf, so there has to be type information inside the message to tell the receiver whether the root of the tree in the message is a Fork or a Leaf.

Note: In Haskell's datatypes, for example:

data Tree x = Fork (Tree x) (Tree x) | Leaf x

Tree is a single type, and Fork and Leaf are values of a discriminated union. There is a 'tag' implicit in each node to say whether it is a Fork or a Leaf, but this is not type information.

This is similar but different to the situation where Fork and Leaf are types.

Actor of another implementation type (e.g. Branch) can be of an extension of Tree.

True, it can, but that doesn't change the need to have type information in the message to indicate the type of each node in the tree.

What languages like Haskell really need is extensible datatype, that way you don't have to use type-classes and have separate types for Fork, Leaf etc.

True, it can, but that doesn't change the need to have type information in the message to indicate the type of each node in the tree.

Why does a getHash message need "to have type information in the message to indicate the type of each node in the tree"?

Hmm.

A tree can be a Fork or a Leaf, so there has to be type information inside the message to tell the receiver whether the root of the tree in the message is a Fork or a Leaf.

What is the "root of the tree in the message?"

What tree is "in the [getHash] message"?

I have realised I am wrong, the type information is implicit in the actor you are sending the message to. Sometimes it's hard to switch between thinking about a problem the Haskell way (or other language) to the ActorScript way.

I am not necessarily saying the problem isn't there, just that getHash does not send anything and returns a simple integer.

If we pass the tree to an actor as part of the message, then the type information is in the message.

The type of an Actor must be known in order to send it a message.

Tree is *not* a discrimination; Fork and Leaf are extension implementation types of interface type Tree.

PS. ActorScript also has discriminations, but as defined the interface type Tree is not one of them.

getHash on Fork and Leaf functions a bit like a virtual function, so that the tree is kind of a discriminated union. Its a bit like this equivalence:

data Tree x = Fork (Tree x) (Tree x) | Leaf x

and

template <typename T>
class tree {
...
}

template <typename T>
class fork : public tree {
...
}

template <typename T>
class leaf : public tree {
...
}

which in turn is similar to:

interface Tree with getHash[] -> Integer

actor Leaf[terminal:t] extends Tree using
    getHash[] -> Hash.[terminal]
    getTerminal[] -> terminal
   
actor Fork[left:Tree, right:Tree] extends Tree using
    getHash[] -> Hash.[left.getHash[], right.getHash[]]
    getLeft[]:Tree -> left
    getRight[]:Tree -> right

see earlier.

We could also have the following:

Actor Branch◅aType▻[aLeft:Tree◅aType▻, aRight:Tree◅aType▻, aTerminal:aType]
   extends Tree◅aType▻ using
       getHash[ ]:Integer → Hash◅aType▻.[aLeft.getHash[ ], aRight.getHash[ ]]
       getLeft[ ]:Tree◅aType▻ → aLeft
       getRight[ ]:Tree◅aType▻ → aright
       getTerminal[ ]:aType → aTerminal▮

Edit: getHash should have return type

There is no reason why datatypes cannot be extensible. Haskell does not do this, but a syntax like this is possible, and there are no real semantic problems with doing this:

data Tree x
data Tree x <| Leaf x
data Tree x <| Fork (Tree x) (Tree x)
data Tree x <| Branch (Tree x) (Tree x) x

Using record format we get access functions too:

data Tree x
data Tree x <| Leaf {leaf_terminal :: x}
data Tree x <| Fork {fork_left :: Tree x, fork_right :: Tree x}
data Tree x <| Branch {
    branch_left :: Tree x,
    branch_right :: Tree x,
    branch_terminal :: x
}

I think I will redo the last Haskell example with record format so it looks more like the ActorScript example.

Reading this here is something that confuses me:

getLeft[]:Tree<aType> -> aLeft

Why are we passing a tree to 'getLeft'? We are passing the getLeft message to an actor that is a fork, so message does not need to include any parameters. Also:

getTerminal[ ]:aType → aTerminal

"aType" seems to be redundant, again we know we want terminal from the receiving actor.

So the following would seem correct to me:

actor Branch<t>[left:Tree<t>, right:Tree<t>, terminal:t] extends Tree {
    getHash[] -> Hash<t>.[left.getHash[], right.getHash[]]
    getLeft[] -> left
    getRight[] -> right
    getTerminal[] -> terminal
}

Am I misunderstanding something?

Edit: I think I have worked out its the return type? Why is it not needed for 'getHash'? Seems like it could easily be inferred from the first line of the actor definition in any case.

I think I have worked out its the return type?

Good job.

Seems like it could easily be inferred from the first line of the actor definition in any case.

Perhaps but type inference will never be non-trivial in ActorScript since there is no universal quantifcation over all types. (So, forget about type inference? Its at most a minor syntax hack in this context.)

So why does getHash not need a return type, but the others do. It looks to me that the type inference is trivial in these examples, why not infer if you can?

Good catch, Keean!

Actually, getHash *should* have a return type for better error checking. The issue is whether the extension is introducing a new getHash or using the one from Tree.

Given we have:

Message◅getHash⨀Tree[ ]↦Integer▻

Surely we can get both the message and response type from the definition of "getHash"? Also why have a different syntax? What would be wrong with:

Message<Tree<Int>.getHash>

It is clear we mean the actor and are not calling it because of the lack of '[...]' after getHash. Further given we have "Tree[].getHash"it should be clear we want the type not the value/definition from the context, which is needing a type.

The Tree interface type is extensible, e.g., the Fork implementation type and the Leaf implementation type both extend Tree.

In addition,
* there might be another implementation type that extends Tree
* there might be another interface type that extends Tree

The Tree type class is extensible, and other modules can extend with local or global instances, and yet the Haskell system with type classes does allow for separate compilation. This is because all the type definitions are in the class not the instance (normally).

Actually this has made me realise something important about type-families and associated types compared to functional-dependencies. FunDeps seem to have fallen out of favour compared to associated types, but the compile time separation is better. I will redo the example using FunDeps when I get a minute.

Here's the Haskell version using functional dependencies:

{-# LANGUAGE MultiParamTypeClasses,
    FunctionalDependencies,
    FlexibleInstances,
    UndecidableInstances #-}

data Undefined
data Fork x y = MkFork x y
data Leaf x = MkLeaf x

class Tree t l r | t -> l r where
    getString :: t -> String
    getLeft :: t -> l
    getRight ::  t -> r

instance Tree (Leaf String) Undefined Undefined  where
    getString (MkLeaf x) = x
    getLeft _ = undefined
    getRight _ = undefined

instance (Tree a c d, Tree b e f) => Tree (Fork a b) a b where
    getString x = getString (getLeft x) ++ getString (getRight x)
    getLeft (MkFork x _) = x
    getRight (MkFork _ y) = y

myTree = MkFork (MkLeaf "a") (MkLeaf "b")

main = do
    putStrLn $ getString myTree

However actually writing it, I don't think it has the advantages I thought it did. It still needs the instances for separate compilation to know the result types of getLeft/getRight. Like with ActorScript you can compile the instances separately from each other, but any code using the instances needs to be able to see all of them.

The best version for separate compilation seems to be this:

{-# LANGUAGE RankNTypes,
    FlexibleInstances,
    TypeFamilies #-}

-- Interface: must be visible to any client code.

data Fork x y = MkFork x y
data Leaf x = MkLeaf x

type family LeftType t
type instance LeftType (Fork l r) = l

type family RightType t
type instance RightType (Fork l r) = r

class Tree t where
    getString :: t -> String

class TreeFork t where
    getLeft :: t -> LeftType t
    getRight ::  t -> RightType t

-- Implementations: can be separately compiled.

instance Tree (Leaf String)  where
    getString (MkLeaf x) = x

instance (Tree a, Tree b) => Tree (Fork a b) where
    getString x = getString (getLeft x) ++ getString (getRight x)

instance TreeFork (Fork a b) where
    getLeft (MkFork x _) = x
    getRight (MkFork _ y) = y

-- Client code.

myTree = MkFork (MkLeaf "a") (MkLeaf "b")

main = do
    putStrLn $ getString myTree

Where we keep the type family in the interface separately from the type-class. Notice I have separate classes for Tree and TreeFork, so that leaves don't need to define getLeft and getRight any more. The main difference from the ActorScript now is that there is no "TreeLeaf" class. This is because Haskell does not allow ad-hoc overloading (uncontrolled overloading is seen as a bad thing), so you cannot define "getString" in two different type-classes, and you cannot define a function (like getString) with two different types. Type-classes / instances control overloading, so any given function must have a single type signature except where a type class permits overloading. This means "getString" has to go into a type-class common to both leaves and forks.

Now I have realised you don't have getLeft/getRight as part of the interface, then I can simplify this a lot by moving that into the type-specific implementation. We now get this much simpler Haskell version:

{-# LANGUAGE FlexibleInstances #-}

-- Interface: must be visible to any client code.

data Fork a b = MkFork {fork_left :: a, fork_right :: b}
data Leaf a = MkLeaf {leaf_terminal :: a}

class Tree t where
    getString :: t -> String

-- Implementations: can be separately compiled.

instance Tree (Leaf String)  where
    getString x = leaf_terminal x

instance (Tree a, Tree b) => Tree (Fork a b) where
    getString x = getString (fork_left x) ++ getString (fork_right x)

-- Client code.

myTree = MkFork (MkLeaf "a") (MkLeaf "b")

main = do
    putStrLn $ getString myTree

What is interesting is that we don't quite have an abstract datatype. We need to share the underlying types Leaf and Fork with the client code, so that the client code can construct a Tree. What is an interesting problem, is how to allow the client code to construct the tree entirely through the interface, so that the types "Leaf" and "Fork" can be moved into the implementation.

Edit: improved version using record syntax to look more like the ActorScript example.

The getLeft & getRight messages are signatures in implementation type Fork,

I called them fork_left and fork_right, and they are declared in the definition of the type Fork. It looks a lot simpler now.

Is this another pretzel?

Pretzels are tasty, especially the giant ones they make whilst you wait.

Being a pretzel means being tied in knots :-(

I think this Haskell implementation is every bit as elegant as the ActorScript version, and separates the concerns better. I will do a line-by-line comparison to show how little difference there actually is.


Comparison:

Interface Tree with getHash[] -> Integer

The differences are Haskell uses a Lisp like syntax for functions and types, so that "Tree<t>" is written (Tree t), and the function (message) type is written using arrow notation:

class Tree t where getHash :: t -> Int

Next defining the Leaf:

Actor Leaf<|t|>[terminal:t]

Note, in the Haskell I have given the constructor a different name from the type (MkLeaf), it doesn't look like you can do this in ActorScript. The Haskell also defines "getTerminal" in a nice compact format, so it doesn't need to be defined separately:

data Leaf a = MkLeaf {getTerminal :: a}

Implementing the Tree interface

   extends Tree<|t|> using
      getHash[] -> Hash<|t|>.[terminal]
      getTerminal[] -> terminal

As we defined getTerminal in the data declaration, we just need to implement 'getHash':

instance (Hash t) => Tree (Leaf t)  where
   getHash x = hash (getTerminal x)

Defining the types for Fork:

Actor Fork<|t|>[left:Tree<|t|>, right:Tree<|t|>]              

Again, very similar, but the get methods are defined inline:

data Fork a b = MkFork {getLeft :: a, getRight :: b}

Finally implementing the Tree interface for fork:

   extends Tree<|t|> using
      getHash[] -> Hash<|t|>.[left.getHash[], right.getHash[]]
      getLeft[]:Tree<|t|> -> left
      getRight[]:Tree<|t|> -> right

Again we just need to define getHash in the Haskell version, the code is very similar:

instance (Tree a, Tree b) => Tree (Fork a b) where
    getHash x = hash (getHash(getLeft x), getHash(getRight x))

I think it would be interesting to consider the Haskell syntax, with actor semantics instead of the usual lazy evaluation.

The example has been converted to using pattern matching below:

Structure Leaf◅aType▻[aTerminal:aType]
   extends Tree◅aType▻ using
      ⟦hash⟧:Integer → Hash.[aTerminal]▮

Structure Fork◅aType▻[aLeft:Tree◅aType▻, aRight:Tree◅aType▻]
   extends Tree◅aType▻ using
       ⟦hash⟧:Integer → Hash.[aLeft.⟦hash⟧, aRight.⟦hash⟧]▮

Note that the above define distinct branded implementation types (i.e. cannot be downcast or subtyped) that must be able to be upcast to the Tree interface type and conditionally downcast from Tree.

The following procedure makes use of the above:

Fringe◅aType▻.[aTree:Tree◅aType▻]:[aType*]  ≡ 
   aTree � 
     Leaf[aTerminal] ⦂ [aTerminal]
     Fork[aleft, aRight] ⦂ [⩛Fringe.[aLeft], ⩛Fringe.[aRight]]▮

where Hash is a polymorphic procedure and

Interface Tree◅aType▻ with ⟦hash⟧↦Integer▮

The conversion to pattern matching makes them more similar, although I wonder why you have so many different keyworks like 'Actor' and 'Structure' which seem almost identical. Really one of these is more general than the other, I don't see why you need both.


Comparison:

Fringe◅aType▻.[aTree:Tree]:[aType*]  ≡ 
   aTree � 
     ↓↓Leaf[aTerminal] ⦂ [aTerminal]
     ↓↓Fork ⦂ [⩛Fringe.[aLeft], ⩛Fringe.[aRight]]▮

So in Haskell we use the same type-class mechanism we used to define the Tree interface to do the "type-case" operation on the Fringe function. This re-use of one generic mechanism is what makes type-classes a more expressive abstraction.

class Fringe t where fringe :: Tree t -> [t]
instance Fringe (Leaf t) where fringe leaf = [getTerminal leaf]
instance Fringe (Fork t) where fringe fork = fringe (getLeft fork) ++ fringe (getRight fork)

So I don't see any pretzels, what I see is Haskell having a more powerful abstraction mechanism, that is it achieves more with one single mechanism.

For me Haskell wins at this point (note: so far this is only about pure actors with no state)

Fringe should be a procedure and not a class.

There is no getTerminal, getLeft, getRight.

Also you don't have the Hash procedure where a ⟦hash⟧ message can be sent to a Tree, Leaf, and Fork.

Fringe is a function, and it is independent of the previous definition. You call 'fringe x' the type class just determines which 'fringe' gets called based on the type. Note "Fringe" is the type-class "fringe" is the function.

getTerminal, getLeft and getRight still exist and work exactly as before. Hash still works on Tree exactly as before. We have extended wht previous program above with this single type-class and everything else is the same. So none of those criticisms are valid.

I can write the following main program:

main = do
    putStrLn (show (getHash myTree))
    putStrLn (show (fringe myTree))

The following procedures do not exist: getTerminal, getLeft, getRight.

The specification calls for using pattern matching.

Requiring both the type-class Fringe and the function "fringe" is a small cost to pay compared to the advantage of only having a single generic abstraction (type-classes).


Further the procedures 'getTerminal', 'getLeft' and 'getRight' all exist. Here are there definitions, which I already gave in the above code:

data Leaf a = MkLeaf {getTerminal :: a}

This defines the procedure 'getTerminal' to be the access function such that:

getTerminal (MkLeaf 0) == 0


data Fork a b = MkFork {getLeft :: a, getRight :: b}

This defines "getLeft" and "getRight" such that:

getLeft (MkFork 1 2) == 1
getRight (MkFork 1 2) == 2


'getTerminal', 'getLeft' and 'getRight' are contrary to spec :-(

Pattern matching must be used to match the specification interfaces.

I'm sorry I don't understand, what pattern matching?

The interface for Fork in the Haskell is the combination of the datatype-functions (getLeft and getRight), plus all the type-classes it is a member of, so "Tree" provides "getHash" and "Fringe" provides "fringe". We can carry on extending the set of messages that Fork will accept by adding instances for Fork to more type-classes.

'getLeft' and 'getRight': are not messages to a Fork in latest spec

I think because Haskell does not make the distinction between a pattern match and a message there is more room for the compiler to optimise, and it is a higher level description. I can focus on what I want (access to the 'left' fork, without having to decide if I want a pattern match or a message. This higher level of abstraction lets the compiler chose whichever is more efficient.

Specifications should not get involved in the mechanism (the how to do something) they should be focused on what needs to be done. That is the difference between a specification and an implementation.

Edit: On the other hand the equivalence makes me think I could see myself using ActorScript for some applications. I have concerns about ActorScript for systems programming, as inlining seems to be problematic, and it seems to require pervasive tagging of data with types, and garbage collection. The Haskell approach with type classes lends itself to better compile time optimisation, although I think parameterized types solve a problem I was having with universally quantified types.

Haskell lacks interfaces, pattern matching, messages, etc.

Inlining is easier with ActorScript than Java, C#, or C++.

ActorScript does not require any tagging of data. However, downcasting is conditional for discriminations and extensions.

Haskell clearly has interfaces (type-classes are interfaces) and pattern matching (Haskell's pattern matching with guards is as good as it gets). I think it's important for language designers to have experience of writing solutions to real world problems in as many languages (or classes of language) as possible. Haskell as "the lazy pure functional" language is definitely important, and should be studied.

Haskell has message passing (using channels), but what I was suggesting was changing the semantics of function calling in Haskell to use message passing like ActorScript. So the language remains the same, except each Haskell function becomes a single message actor, where we send a message with the arguments and wait for the response.

How does ActorScript implement discrimination without tagging? Does it send the message to the actor, and it throws an exception if its the wrong type? This is exactly what I was explaining elsewhere, discriminations can be implemented with interfaces and virtual functions. The same technique could be used when implementing Haskell discrimination types.

The other main use of tags is so the garbage collector knows the type of the thing it has to delete or relocate, and which parts are references to other things. How does actorscript handle garbage collection? How does it trace references and determine the size of actors at runtime?

Requiring both the type-class Fringe and the function "fringe" is a small cost to pay compared to the advantage of only having a single generic abstraction (type-classes).

What are the limitations of Haskell type classes as a foundation for mathematics including computation?

Haskell has too much cruft and too little expressiveness.

Maybe what is suitable for use as a foundation for mathematics is not a good programming language, and vice versa.

On the other hand, maybe type-classes could form a foundation for mathematics. I don't think much work has been done on it. I know type classes correspond to an order-sorted higher order logic, but whether they capture a sufficient part of higher order logic is an open question as far as I know.

Maybe what is suitable for use as a foundation for mathematics is not a good programming language, and vice versa.

Anything is possible.

Concurrency is the greatest lack in Haskell.

Claim: It is now impossible to do mathematical foundations of Computer Science without concurrency being central both for theory and practice.

Impossible to do mathematical foundations of Computer Science without concurrency both for theory and practice.

To a lot of readers I think that still sounds bombastic and now that I got the picture it sounds banal. It's weird, the non-linear backlash it gets.

1. Undergrad maths are, on average, shit -- hence the bafflement over such simple claims like the centrality of lists, sets, and maps.

2. Undergrad maths are, on average, shit -- hence the partial bafflement over categorical constructions, constructive types, non-deterministic as contrasted with categorical constructive math, etc.

3. Non-constructive type theory typical of, e.g., Haskell papers continuously ponders how easy and obvious things can be expressed against an awkward and problematic core. Guaranteed employment with a veneer of mathematical respectability.

4. Your critics are correct to the extent they say a decent Actor and DL pedagogical intro is sorely lacking (but time heals all wounds).

Thomas,

You have some good points.

At Stanford, it is being pondered that good introductions to Actors and Direct Logic are sorely needed in that the book Inconsistency Robustness is targeted mostly at experts though it is hoped that others can benefit from the preface and from introductions and summaries for the articles.

Would you like to try? Also, it would be good to have reviews on the Amazon website :-)

Would you like to try?

I will probably give it a shot, anyway.

I would glad to help. Also, others at Stanford are interested.

I see an MIT alumni email address for you. Right choice?

The alumni email address should work.

For a lot of problems a sequential computer can simulate "out-of-order" where necessary by having a message queues, and selecting the next message from a random position in the queue. So how foundational is concurrency? If 99% of problems can be expressed sequentially, and the other 1% we can implement a concurrency simulator, isn't the better solution to define the more complex in terms of the simpler. A foundational system is the simplest system from which all others can be defined.

As to your other points:

1. Set theory (ZF for example) is defined as an axiomatic system, so it is not foundational. Sets are useful in programming, but like in maths they can be defined in terms of a simpler core language. Keeping the core language as small as possible to aid (formal) verification is always important.

2. I could certainly do with working on this area a bit myself - its a bit outside of my interest area, but it would be good to know enough to tell if there is anything useful here. There seems to be a relationship between categorical axioms and type-classes.

3. I am not convinced the constructive approach is better than the universally-quantified type system approach. Type systems like Haskell's are able to distinguish between static and runtime polymorphism, whereas dependent type theories don't. How much of a problem this is I am not sure. A Haskell like type system could have parameterised types instead of universal quantification, but this would be more restrictive, and accept less 'correct' programs. Are any of the programs rejected useful? Probably not, but I'm not sure.

4. The book is not that hard to read, but not having a reference implementation to test programs in makes it hard to get a feel for programming in ActorScript. I also think you are going to get questions in any case. Like I said before, I think a better approach is to take each feature you want to discuss, and modify an existing language that is widely known with that feature. An example would be, what happens when you take System-F and replace universal quantification with parameterised types.

Claim: Massive concurrency is required for performance and robustness:
1) Concurrency can be exponentially faster that lambda calculus parallelism in practice
2) Concurrency is only way to avoid single points of failure.

1. Set theory (ZF for example) is defined as an axiomatic system, so it is not foundational.

That's a peculiar assertion.

There seems to be a relationship between categorical axioms and type-classes.

In the context of the thread: By "categorical construction", I mean finite construction rules for objects of some type accompanied by an axiom of categorical induction. An axiom of categorical induction asserts that a property can be proved true of all objects of the type under consideration by induction over the finite construction rules. Example: 0 is a natural number. If x is a natural number so it Succ(x) and x != Succ(x). Plus the axiom that if a proposition is true for 0 and if P(x) implies P(Succ(x)) then P is true of all natural numbers.

Such an axiom authorizes a fundamental proof technique and it rules out non-standard models (e.g., no infinite natural omega that is not the successor of any lesser natural).

If you *want* other models (perhaps, not for computer science) you can obtain them (for example) by adding axioms of trans-finite induction and additional rules of construction as needed. (E.g., define omega.)

Why is it peculiar to say set theory is not foundational? Depending on which set theory you are using it can be defined in first or second order logic. We know that natural numbers can be defined in second order logic. Isn't it obvious that logic is the foundational theory, and everything else can be defined in terms of it.

For example the Twelf proof assistant is based on lambda Prolog, a higer-order variant of Prolog. Coq uses CoC type-theory.

I think you can choose logic, type-theory or category theory as the foundations (due to computational trinitarianism) and I suspect that as the structure of those three are the same there is something interesting going on.

To clarify your description above, the axiom of categorical induction as you describe it sounds admissible in first order logic, but I thought it was only second order?

Peano/Dedekind typed categorical induction is not first-order logic.

Also, it is not second-order unless you redefine second-order to use types.

What is the problem with categorical induction and second order logic?

Edit: why do you have to redefine second order logic to use types. Is it that you specified "typed categorical induction" tautologically? Is second order logic okay for plain "categorical induction"?

Types make concepts from higher-order logic both rigorous and definitively categorical.

Why is it peculiar to say set theory is not foundational? Depending on which set theory you are using it can be defined in first or second order logic. Isn't it obvious that logic is the foundational theory, and everything else can be defined in terms of it.

A theory F is a foundation for a theory G if G can be expressed as definitions in theory F with no new axioms.

If we can do that, we know that G is at least no less consistent a theory than F, and that theory F is only as consistent as theory G.

Neither first or second order logic is a foundation for, say, ZF set theory because ZF set theory requires additional axioms.

In contrast: suppose that I want to make a mathematical theory of relations. Further, that I define relations as certain sets of ordered pairs in ZF. Now I know that that if ZF contains no paradoxes, then neither does my theory of relations. And conversely I know that if my theory of relations contains a paradox, then so does ZF. After all, my theory of relations is contained entirely within the axioms of ZF.

Logic is not a foundation for set theory because a paradox in set theory does *not* necessarily imply a paradox in logic. If a paradox arises in set theory and the paradox is not independent of set theory axioms, then that paradox is *not* a paradox of logic.

To clarify your description above, the axiom of categorical induction as you describe it sounds admissible in first order logic,

Each axiom of categorical induction is a new axiom. In Inconsistency Robust Direct Logic there is a single axiom of categorical induction over the natural numbers.

but I thought it was only second order?

Universal quantification from ordinary second order logic is not used.

Okay, so you are using foundational in a different way. So I don't want to be using the word foundational.

What I was trying to express is that as we can define the axioms of set theory in logic, logic is the basis of mathematics. None of the axioms can change the logic. The logic is like a programming language, and set theory is the program.

Some logics will not be sufficient to define set-theory, others will allow it to be defined but are more complex than necessary. What I am interested in, is the simplest logic (programming language) in which the axioms of all of mathematics can be expressed. If you have this set theory is just a program/library.

Okay, so you are using foundational in a different way.

That's right. So all of your responses to me on this point are non-responsive.

What I was trying to express is that as we can define the axioms of set theory in logic,

When you talk about math vaguely, you can generate lots of statements.

You introduced foundational as the reason sets need to be included in the language, which now looking at the meaning you intended is nonsense.. Foundational as you used it has nothing to do with whether sets should be included in the language. As I correctly asserted, if you can define sets in the language they don't need to be included in the definition. The meaning of foundational is a distraction.

You introduced foundational as the reason sets need to be included in the language,

No I did not.

Sorry, you are right, I re-read the thread, and I did use the word foundational first, but not in the sense you inferred. Then you said that was peculiar, which I admit makes sense considering the domain-specific meaning of foundation which I was not aware of. In any case this is again a diversion, because the statement I was making was about the ability to define set theory in a particular logic, not whether logic was foundational. So just ignore the word foundational.

The point was if you can define sets in the language you don't need to have them as part of the core language itself, they can be a program/library in the language. The same applies to mathematics, sets don't need to be built-into logic, if they can be defined axiomatically in that logic. Obviously foundational is not the right work to use. Maybe I can say sets are not a fundamental primitive instead?

The point was if you can define sets in the language you don't need to have them as part of the core language itself,

Duly noted?

Claim: The pure part Haskell has the same or more inherent concurrency as ActorScript.

This was the point I was making above that you seem to have missed. For stateless actors there is no point in grouping the messages together into an actor. Each message could be completely a completely independent 'function'.

On that basis, if you replace Haskell's function call implementation with a message passing implementation, then what you have is effectively equivalent to ActorScript, allowing for the use of type-classes to control overloading instead of type extension.

Then the only consideration is which syntax you prefer :-)

Claim: Interfaces are important for modularity and security because:
1) Group capabilities together for modularity
2) Provide a discrete bundle of capabilities for security

Claim: type classes can be resolved entirely statically, meaning all polymorphism is removed at compile time. This allows the type-class function to be in-lined, resulting in faster and better code.

Type-classes are not a security mechanism. You probably want to use existential types for that (which also permit runtime polymorphism, in a 'secure' container.

ActorScript does not impose limitations on in-lining implementations.

There are some types that are not known statically, and therefore cannot be inlined. Type classes guarantee the polymorphism is static and the actual type can be resolved at compile time. Actor interfaces do not make that guarantee.

Do you have any examples of where ActorScript imposes limitations on in-lining implementations?

Anything where polymorphism is at runtime, so for example a you have a queue of commands where the commands all implement some interface. If the commands are read from a file, or from user input, you cannot inline the commands.

If the commands come from a static list, known at compile time, then they can be inlined.

The problem of what can and cannot be inlined at compile time is not easy to solve with dependent types, and the programmer may not easily be able to tell whether something is going to cause a performance problem.

An important principle is that you should not pay for something you don't use, in this case it means you should not pay the performance cost for runtime polymorphism if you don't need it. It should be clear to the programmer reading the code if they are paying the cost or not. In C++ the "virtual" keyword serves this purpose.

For the kind of applications ActorScript is designed for, this may not be a problem, but clearly it cannot be a universal language for any purpose if it does not address this issue.

Implementations can be in-lined regardless of source.

Compilation can happen at any time just like any other execution.

Are you including the compiler in the runtime? I think this is not a practical solution, unless you are talking about a JIT compiled language? It's not something I am interested in. For my purposes compilation should happen before an application binary is distributed.

Computation can be done anywhere, anytime.

We are no longer doing batch processing ;-)

Requiring the compiler to be distributed with the runtime is not suitable for all applications. In particular low memory environments, and performance critical environments require static compilation. Also its not secure to distribute source with an application. I cannot imagine distributing proprietary source code, along with a compiler, to a customer. However it might be suitable for open source software.

Compiling is only necessary if there is something that needs to be compiled.

Are you saying ActorScript is only designed to be used with an interpreter?

ActorScript is designed to be compiled efficiently and never being required to look up a symbol at runtime.

So this statement is then false "Implementations can be in-lined regardless of source.". If the implementation to use depends on IO (file, network or user input), then you cannot know which function/actor to inline until runtime when the IO happens. If you want to inline this you have to have access to the compiler at runtime to recompile the actor with the correct inlined code. The other alternative is you cannot inline in these circumstances.

The compiler doesn't care where sources come from. It can inline them in any case.

Challenge: Show an ActorScript program that cannot inline an implementation.

In order to do that, I need to know how ActorScript handles IO. I can't find anything about it in the book index.

How do I read a string from the keyboard, or read a typed variable from a file? I will guess for now and define some actor to do so.

Interface Show with
   toString[] |-> String

Actor ActorA extends Show using
   toString[]:String -> ...

Actor ActorB extends Show using
   toString[]:String -> ...

readList[file]:List<Show> = case file.read[] of
   (x : Integer) (:) readList[file].push[ActorA[x]]
   (x : Float) (:) readList[file].push[ActorB[x]]
   otherwise (:) []

inlineThis[list]:String = if list.length[] > 0 then
    inlineThis[list.tail[]].push[list.head[].toString[]]
    else []
    

test[file]:String = inlineThis[readList[file]]

I am sure there are mistakes, and I am typing this on a mobile phone so I have tried to use the correct ascii, but I have no reference with me. The procedure you are trying to inline is toString[] when it is called on list.head[]. The reason you cannot is that you don't know whether you need to inline ActorA's version of toString or ActorB's, because you cannot predict at compile time which one will be placed in the list by readList.

Even worse, because with separate compilation, we don't know if arguments will depend on IO, you cannot inline anything that is callable from a separately compiled bit of code (let's call this a module). So any code callable from outside the module cannot inline interfaces that depend on arguments.

This kind of polymorphism where you don't know which actor you will find until runtime is called runtime-polymorphism or dynamic-polymorphism.

The kind of polymorphism you can inline, where the actor type is known at compile time is called static polymorphism.

You might want to clean up your code.

The procedure? readlist seems to be an infinite loop or something else :-(

file.read[] will return something that is neither and integer nor a float when you get to the end of file, which returns the empty list, that then gets all the other stuff pushed into it.

In any case you seem to be avoiding the point.

Edit: actually inlineThis seemed to be an infinite loop, not readList. I have fixed it, but I don't think it makes any difference to the inlining question.

I am sure there are mistakes, and I am typing this on a mobile phone so I have tried to use the correct ascii, but I have no reference with me.

Maybe you are rushing to write too many comments too quickly.

Changing the subject now? It's like you are trying to drown out any sensible comment I might have had with pointless posts. It wasn't even an infinite loop, so this whole sub-thread is now moving off the original point. Lets re-state it:

You cannot inline a function where the implementation depends on an actor the type of which is determined at runtime.

How about a comment on whether the call to "toString[]" can be inlined?

First the specific then the general.

You cannot inline a function a function where the implementation depends on an actor the type of which is determined at runtime.

There is no reliably meaningful way to interpret those words in the context of ActorScript.

One could guess, but experience suggests that won't help at this time.

1. I have an interface defining toString.

2. I get some input from the user, say from the keyboard.

3. Depending on that input I put either one of the two actors implementing toSting into the list.

4. At some point I call toString on the contents of the list. This call to "toString" cannot be inlined by the compiler, because the compiler does not know which version of toString it is, as this depends on what the user types at the keyboard, which happens after compilation.

So if you don't think that you can always inline all procedures, you must disagree with one of the above statements [1-4]?

You might like this book:

"Partial Evaluation and Automatic Program Generation" By Neil D. Jones, Carsten K. Gomard, Peter Sestoft

Thanks, Ill take a look at the book. I have looked at partial evaluation before, and it helps the compiler to evaluate statically defined constants and programs with static inputs at compile time. You cannot partially evaluate those bits that depend on runtime IO.

You cannot partially evaluate those bits that depend on runtime IO.

That is true in an irrelevant sense it does not advance your mistaken argument.

Okay, so if you accept that, you don't have far to go to realise the problem with inlining.

Okay, so if you accept that, you don't have far to go to realise the problem with inlining.

Hi.

You either don't or don't wish to understand what people are talking about.

Your strategy of hammer posting is failing to change that.

Stop, please.

Im trying to have an intelligent conversation. I have no strategy, why would I want one?

And yet again you are changing the subject. Shall I restate what we should be discussing again, rather than your personal attacks:

You cannot inline a call to an interface, where the implementation depends on IO, so the idea that you can inline any procedure must be false, or the language must not support IO.

Im trying to have an intelligent conversation. I have no strategy, why would I want one?

Out of respect for the people you are asking things of.

In order to efficiently accomplish the aim.

Sometimes we enter a situation thinking we know more about what is going on than we really do.

Indeed, and that can be applied to all of us. Do you understand the problem with inlining runtime polymorphic functions?

Yeah, yeah. Better than you think.

Anyway, "mirror" is a good word choice, in fact.

You remind me of my younger, less developed self. I hate how that guy could burble on well past his grasp.

Well if you understand the problem, then I have indeed been burbling on unnecessarily.

So you think all the issues are easily dealt with using conditional branches? Sometimes the number of possible types can be very large making branches less efficient than the indirect call in the first place. Its only worth inlining if it gains performance. There is also the issue with separate compilation, where you may not know all (or any) of the types that implement the interface, so you cannot construct the conditional branch.

So its the combination of runtime polymorphism and separate compilation that cause the biggest problems for inlining.

So if you don't think that you can always inline all procedures, you must disagree with one of the above statements [1-4]?

I believe that (1) it is possible to inline conditional branches to good effect; (2) you are trolling, please stop out of consideration for humanity.

(Thank you for editing your comment to change its meaning after you saw my earlier reply. It's a good reminder to me.)

I have tried to get my point across, but I guess I have wasted enough time on this. I'm sorry you don't get it, but I re-iterate, I never troll, I am not looking to get any kind of response from you, I am simply trying to point out something I think is important, and that the claim the any procedure can be inlined is false.

So, you have two procedures, and a run-time condition that decides which one to call. When you claim that the procedure cannot be inlined you seem to mean that the run-time check cannot be eliminated?

It is true that the run-time check cannot be eliminated. It is also true that the procedures can be inlined (and that in general any procedure can be inlined by a compiler). The calling sites for the procedures are inside the two branches of the conditional. Inlining the procedures in this case would produce in the residual:

if( dynamic check )
{
Body of procedure 1 / arguments rewritten for this context.
}
else
{
Body of procedure 2 / arguments rewritten for this context.
}

Roughly speaking this is what a partial evaluator would do upon realising that there are two regions with static binding time, inside a dynamically bound conditional. Unhelpfully this is called "The Trick" within the partial evaluation literature, and it is essentially a hack that says: two is small enough to make this work. It is somewhat unhelpful and opaque to point somebody towards the standard text on partial evaluation to discover this piece of folklore, although I seem to remember that it is in there somewhere. It is also true that you have been using the term "inline" in a sense that is not entirely strictly and literally accurate...

IIRC, "the trick" was a way of rewriting your code to make the inlining you describe more useful, not the inlining itself.

So for example if you had a variable b:Bool with late binding time, you can maybe improve your code by transforming:

f(b)

into

if b then f(true) else f(false)

Because then you get to inline true and false which, as constants, have very early binding time.

I just looked it up to check and your memory is indeed correct. There is a nice description in Eta Expansion Does The Trick. I was probably confused because the first time I came across it I was looking at value-set propagation and how it could be used to enable the trick automatically.

Except that does not work with separate compilation, where you don't know all the implementations when the module is compiled, or where the variety of objects is large, say a list with a size parameter in the type.

If implementation is known and recipient is local, then message send can be inlined.

Of course, it is not always desirable to inline ;-)

Yes, this seems correct, if by local you mean the same source file, or code block that is compiled separately from other source.

A recipient Actor is local to sender of message, if it is co-located in the same process.

Do you think a compiler should support separate compilation, so that one source file can be compiled into object code independently of other source files?

Do you think systems should support runtime dynamic loading (of shared objects) like DLLs in windows and .so files in Linux/Unix?

somewhat unhelpful and opaque to point somebody towards the standard text on partial evaluation to discover this piece of folklore

It was not to discover a particular piece of folklore.

I might be wrong but my perception is of K. commenting on the basis of an ad hoc understanding of inlining.

By an ad hoc understanding, I mean an understanding obtained from a few specific examples of inlining in particular compilers, plus perhaps some random selection of more theoretical discussions of what particular ad hoc compilation techniques can and can't do.

Conflating an ad hoc understanding of inlining with a more essential understanding leads to asking questions about Actorscript that have no helpful answer. (So the sentiment "Why don't you just answer the damn question!" stands for a mutual frustration.)

Ad hoc inlining and constant folding are, I think we can say, special cases of the general concept of partial evaluation, for which there is a beautiful and nicely worked theory (that in turn can guide actual practice).

Jones, Gomard, and Sestoff's book isn't directly and trivially applicable to ActorScript. After all, that work uses functional and procedural models of computation, not an actor model.

Nevertheless, working through that book to get the theory of partial evaluation in functional and procedural contexts should produce a good perspective for thinking about (e.g.) inlining in ActorScript.