package typedLambda.model.type;

/*
 * A Type object represents a simple type in lambda calculus.
 * 
 * A Type object is either the AnyType, either a FunctionType.
 * 
 * A Type object is invariant, like a  String object.
 */
public interface Type {

	/*
	 * Each predefined Type object is attached to a symbol.
	 * 
	 * No symbol is represented by (char) 0.
	 */
	public char getSymbol();
	
	/*
	 * Being predefined is equivalent to having a symbol.
	 */
	public boolean isPredefined();
	
	/*
	 * The root Type is said AnyType.
	 * 
	 * The AnyType symbol is 'o'.
	 */
	public boolean isAnyType();
	
	/*
	 * A FunctionType is defined by an ordered pair (Type -> Type).
	 * 
	 * The first Type is the argument Type.
	 * The second Type is the result Type.
	 */
	public boolean isFunctionType();
	
	/*
	 * Returns true if and only if the given Type is the same than this Type.
	 */
	public boolean isSameTypeThan(Type type);

	/*
	 * Returns true if and only if this Type is a sub-type of
	 * 	-or the same type than- the given type.
	 * 
	 * A sub-type may take the place of the type of an argument.
	 * 
	 * if a Term is typed by a sub-type of <T>
	 * 	then it is typed by <T>.
	 */
	public boolean isSubTypeOfOrSameTypeThan(Type type);
	
	/*
	 * Returns the length of this Type.
	 * 
	 * The length of AnyTpe is 1.
	 * The length of a function Type is the sum of the length of its argument Type
	 * 	and the length of its result Type.
	 */
	public int length();
	
	/*
	 * Returns a String representation of this Type.
	 * 
	 * if isCompact then uses the symbols of all the predefined types.
	 * if not isCompact then uses only the AnyType symbol.
	 */
	public String toString(boolean isCompact);
}