Type Inference for GADTs and Anti-unification

Abstract

Nowadays the support of generalized algebraic data types (GADTs) in extensions of Haskell allows functions defined over GADTs to be written without the need for type annotations in some cases and requires type annotations in other cases. In this paper we present a type inference algorithm for GADTs that is based on a closed-world approach to overloading and uses anti-unification and constraint-set satisfiability to infer the relationship between the types of function arguments and result. Through some examples, we show how the proposed algorithm allows more functions defined over GADTs to be written without the need for type annotations.

These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

1 Introduction

Generalized Algebraic Data Types (GADTs) constitute a powerful extension to algebraic data types of functional languages like Haskell and ML, and are nowadays widely used. A GADT is defined by giving an explicit type signature for each of its constructors. This allows functions to be defined by specifying equations that return expressions of distinct types, all instances of the GADT type. For example, the function eval, presented in e.g. [7, 12], evaluates an expression and returns a value of a type that varies according to the argument type (due to space reasons the Term constructor is presented in a shortened form):

The use of an algebraic data type would destroy the simplicity of the evaluator, by requiring a declaration of another algebraic data type with a distinct constructor (tag) for each possible distinct type of the result, with undesirable constructor tagging and untagging.

Type inference with GADTs is complex, mainly because of problems in identifying a principal type in many cases. Consider the following example, taken from [15]:

In the first alternative of test, the result type inferred for the expression $n~>~0$, ${ Bool}$, is associated with the type of constructor T1, and (T1 n) can be determined to have type T ${ Bool}$, with n of type ${ Int}$. In the second alternative of test, there is no explicit association between type T a, constructed by the use of T2, and the return type (the type of r), and thus in this case the type of the result should be unified with that of the first alternative (${ Bool}$). A relation between the GADT type and the type of the result could exist, and be explicitly annotated: the following type signatures are both accepted for the function test, but none is an instance of the other:

Several approaches have been proposed to deal with type inference for GADTs, most of them imposing several restrictions. GADTs are supported in GHC 7.10.1 [20] as described in [6], where type checking is based on type signatures explicitly given by the programmer. Recent work [15, 22] describes a type inference algorithm that can avoid type signatures in a restricted number of cases.

In this article we present another type inferencing algorithm that accepts the declaration of functions based on GADTs without the need for type signatures (Sect. 3). Examples where types can and cannot be inferred, and issues related to the existence or not of principal types, are also discussed in Sect. 3.

Our type inference algorithm uses anti-unification (defined in Sect. 2.1) to capture the relation between the types of the alternatives. Type variables that are not related to GADTs are unified as usual. Cases involving recursive calls can be polymorphic recursive, and are handled as if each alternative is an overloaded definition. In this case, a constraint is added to the type of the recursive call. Constraint-set satisfiability of these constraints is used to construct a substitution that is used for instantiating the type of the alternative, in a process similar to the handling of overloading in System CT [2]. A brief review of System CT is given in Sect. 2.

2 Preliminaries

In this section we introduce some basic definitions and notations. We consider that meta-variables defined can appear primed or subscripted.

Meta-variable usage is defined in the paper as follows: x, y denote term variables, C, D data constructors, $\alpha , \beta$ (a, b, ... in examples) type variables, T a type constructor, e a term, $\tau ,\rho$ simple types, $\kappa$ a constraint set, $x:\tau$ a constraint, $\sigma$ a type, $\varGamma$ a typing context, that is, a set of pairs written as $x:\sigma$, and S a substitution.

The notation $\overline{a}^{\,n}$, or simply $\overline{a}$, denotes the sequence $a_1,\ldots ,a_n$, where $n \ge 0$. When used in a context of a set, it denotes the corresponding set of elements in the sequence $\{a_1,\ldots ,a_n\}$.

A substitution is a function from type variables to simple type expressions (cf. Sect. 3.2). The identity substitution denoted by id. $S\sigma$ represents the capture-free operation of substituting $S(\alpha )$ for each free occurrence of $\alpha$ in $\sigma$.

We overload the substitution application on constraints, constraint sets and sets of types. Definition of application on these elements is straightforward. The symbol $\circ$ denotes function composition and $\textit{dom}(S)=\{\alpha \mid \ S(\alpha ) \ne \alpha \}$.

The notation $S[\overline{\alpha }\mapsto \overline{\tau }]$ denotes the updating of S such that $\overline{\alpha }$ maps to $\overline{\tau }$, that is, the substitution $S'$ such that $S'(\beta ) = \tau _i$ if $\beta = \alpha _i$, for $i = 1,...,n$, otherwise $S(\beta )$. Also, $[\overline{\alpha }\mapsto \overline{\tau }] = { id}[\overline{\alpha }\mapsto \overline{\tau }]$.

2.1 Anti-unification

A type $\tau$ is a generalization — also called (first-order) anti-unification [3] — of simple types $\overline{\tau }^{\,n}$ if there exist substitutions $\overline{S}^{\,n}$ such that $S_i(\tau )=\tau _i$, for $i=1,\ldots ,n$.

We call a function that gives the least generalization of a finite set of simple types the least common generalization (${ lcg}$).

An algorithm for computing the lcg of a finite set of types in presented in Fig. 1. The concept of least common generalization was studied by Gordon Plotkin [10, 11], that defined a function for constructing a generalization of two symbolic expressions.

Fig. 1.

Least common generalization

2.2 System CT

System CT is an extension of the Damas-Milner type system for dealing with overloading [1, 2, 13, 14]. Our initial view for the definition of system CT was to consider a simple extension where a name (or symbol) could have more than one type assumption in a typing context. This led to the adoption of a closed world approach for overloading [1, 2, 21]. However for efficiency reasons, we have changed our initial idea about the support of only a closed world approach to overloading, due to the need (in a closed world) of checking constraint-set satisfiability for each function application. Nowadays, our view, highly influenced by Haskell’s open world approach, is that an open world is the preferred approach for supporting overloading. We leave discussion of an optional, instead of mandatory, use of type classes, as well as a related motivation for changing Haskell’s ambiguity rule, to future work.

The principal type of overloaded symbols is defined in system CT by computing the anti-unification of the types of the available definitions of these symbols in the typing context, instead of requiring them to be explicitly annotated in a class declaration.

The least common generalization of the finite set of types of the definitions of an overloaded symbol in a given context is taken as the (principal) type of the overloaded symbol. In system CT a type is denoted by $\forall \bar{\alpha }.\,\kappa .\,\tau$, where $\kappa$ is a possibly empty constraint set and $\tau$ is a simple type (i.e. an unconstrained and unquantified type). A constraint in system CT is a pair $x:\tau$, where x is an overloaded symbol and $\tau$ is a simple type. For example, a typing context, $\varGamma _{\texttt {==}}$, in which the equality symbol is overloaded with types Int and Char contains the following type assumptions:

$$ \begin{array}{l} (\texttt {==}): { Int}\rightarrow { Int}\rightarrow { Bool}\\ (\texttt {==}): { Char}\rightarrow { Char}\rightarrow { Bool}\end{array} $$

In this case, the principal type of $(\texttt {==})$ in $\varGamma _{\texttt {==}}$ is obtained by the least common generalization of the two types of $(\texttt {==})$ in this typing context, and is given by:

Constraint $(\texttt {==}):a\rightarrow a\rightarrow { Bool}$ on this type is similar to Haskell’s constraint Eq a, where such type of $(\texttt {==})$ is annotated, the difference being essentially the abscence of a constraint on (/=) that is also available in type class Eq. The purpose of the constraint is the same as in Haskell: in this case, to allow instantiation of type variable a in $\varGamma _{\texttt {==}}$ only for types Int and Char. Type inference in system CT is a process similar to type inference in Haskell. In particular, the use of overloaded symbols in expressions for which overloading is not resolved causes a constraint to be included in the inferred type. For example, consider:

The type of insert in this typing context is inferred to be:

In general, in a constrained type $\forall \,\overline{a}^{\,n}.\,\kappa .\,\tau$, $\kappa$ is a set of constraints that restricts the set of types to which $\forall \,\overline{a}^{\,n}.\kappa .\,\tau$ may be instantiated: every instance must be such that the resulting constraint set must be satisfiable in the relevant typing context. Constraint set satisfiability is in general an undecidable problem [16, 17], but it can be made decidable without significantly affecting the set of typeable programs [14]. See also [2, 4, 5, 18].

During type inference, the substitution returned by the function — called sat — that computes a substitution that verifies (proves) satisfiability of a given constraint set in a given typing context — or, equivalently, that verifies whether the constraint set is entailed by a set of constraints on the types of definitions of symbols in the typing context — can be used to “improve” the constrained type. See e.g. [5, 13, 14] for definitions of sat and for the problem of constraint-set satisfiability (CS-SAT).

In a closed world, the substitution returned by sat is needed to improve the type of recursive functions. For example, consider the inference of the principal type of overloaded equality for lists, in context $\varGamma _{(\texttt {==})}$:

The (principal) type of $\texttt {(==)}$ is inferred by considering firstly the types of $\texttt {(==)}$ used in the recursive definition, initially given by:

$$\begin{aligned} \{ \texttt {(==):}a\rightarrow b\rightarrow { Bool}, \texttt {(==):[{ a}]}\rightarrow \texttt {[{ b}]}\rightarrow { Bool}\}. \,\texttt {[{ a}]}\rightarrow \texttt {[{ b}]}\rightarrow { Bool} \end{aligned}$$

(1)

The first constraint on the type above comes from a == b , and the second from x == y . Note that the type of (==) cannot be inferred from the lcg of the types of (==) in the typing context, because a new definition is being given, and this in general will modify the lcg. Function sat comes to the rescue, being able to compute a substitution that is used to improve the type of (==) to:

despite the existence of an infinite set of substitutions that can be used to instantiate the type (1) above:

The sat algorithm is defined in [2, 14].

Type inference for polymorphic recursion is treated in a similar way.

3 Type Inference

Let’s say that a GADT function is a function such that the type of a parameter or of the result is a GADT type. Type inference of a GADT function involves, in our approach, the generalization of the types used in the defining alternatives. The substitution returned by sat is used to improve the inferred type, using a process of type inference that has the following phases:

• 1. The type of each defining alternative is inferred, with a constraint (included in the constraint set) for each recursive use of the GADT function.

• 2. The type of each equation j is improved by the substitution given by ${ sat}(\kappa _j,\varGamma )$, where $\kappa _j$ is the constraint set on the type inferred for equation j and $\varGamma$ contains the type assumptions of used overloaded symbols together with the set $\{ x: \sigma _i \mid \ i=1,\ldots ,n\}$, where x is the name being defined and $\sigma _i$ is the type of the i-th equation in the definition of x that is not recursively defined.

• 3. Compute the lcg of the simple type of the alternatives.

• 4. Compute the substitution that is the most general unifier of the types of alternatives of the GADT function which do not involve a GADT constructor and apply this substitution to obtain the type of each alternative.

We present next some examples that illustrate the type inference process.

3.1 Examples

Example 1

Type Inference of function test

The types inferred for each alternative of the function test, presented in Sect. 1, are:

In cases such as this, where recursive calls do not occur, no restriction is generated, making the call to sat unnecessary. The lcg is then computed, taking the set of types of the alternatives as a parameter. The type obtained by lcg allows observation of the dependency that exists between the types of each alternative with those of the generalized type: types for which there is no association with the type of a GADT are unified. The generalization of the types of the alternatives in the definition of the function test yields:

Now, $b'$ is associated with a GADT, and $c',d'$ are not. Thus, phase (4) above specifies that a and c should be unified, as well as ${ Bool}$ and c, resulting in:

As discussed in Sect. 1, type $\forall a$. T $a \rightarrow a \rightarrow a$ could also serve as the type of test, and in that case expression ( test T2 ‘a’) would be type-correct.

In Haskell, type inference for the function testgenerates implication constraints [15, 22], given by (where $\sim$ is a type equality constraint and $\supset$ denotes an implication constraint):

Type equality constraint $(b\sim { Bool})$ is generated from ${ T1}\ n$, type equality constraint $(c\sim { Bool})$ is generated from the first alternative in the definition of test, type equality constraint ($c\sim e$) from the second alternative in the definition of test, where e is the type of r, which is in this case free to be unified ($\{e\mapsto c\}$). The meaning of an implication constraint can be understood by considering that, in this example, $(b\sim { Bool}\supset c\sim { Bool})$ indicates that if type variable b is instantiated to Bool then so must c. These constraints have substitution $\{c\mapsto { Bool}\}$ as a solution. Application of this substitution on the type of test yields type ${ T}\ b\rightarrow { Bool}\ \rightarrow { Bool}$, which is the same type inferred by our algorithm. However, type variable c is considered untouchable in the implication constraint, and then type inference fails. Type variables which occur in implication constraints are considered untouchable within these constraints, and can only be substituted as a result of applying substitutions obtained as a result of solving other constraints. In GHC 7.6.x type inference proceeds as outlined, but from version 7.8.1 a more restricted set of GADT functions for non-annotated types was adopted.

Example 2

Type Inference of function eval

In the definition of eval, presented in Sect. 1, recursive calls involving polymorphic recursion occur in some alternatives, while the type of eval has not been inferred yet. To handle such cases, constraints are generated from the type required for each recursive call. These constraints are subsequently used in the type improvement process.

The alternative with pattern on constructor If has recursive calls for all arguments of the constructor (l, e1 and e1). l has type Term Bool, and e1, e2 have type Term a. Constraints $\{{ eval}: { Term}\ a \rightarrow b, { eval}: { Term}\ { Bool}\ \rightarrow { Bool}\}$ are generated, and the type of the alternative is inferred also as ${ Term}\ a \rightarrow b$. Type inference for the constructor Pair proceeds in a similar way. The types inferred for each alternative are as follows:

After this, the types of the alternatives which contain constraints are subject to type improvement, which consists of the application of the substitution given by ${ sat}(\kappa ,\varGamma )$, where $\kappa$ is the possibly empty constraint set in the type of each alternative and $\varGamma = \{{ eval}: { Term}\ { Int}\ \rightarrow { Int}, { eval}: { Term}\ { Bool}\ \rightarrow { Bool}\}$. After type improvement the following types are inferred for each alternative:

The type inferred for eval is the lcg of the types of the alternatives, given by:

In this case, all types are associated with the GADT, what characterizes them as types that should not be unified, and, as in this case all types are associated to the GADT, we have that, in this case, the type inferred is the principal type.

Example 3

In some cases anti-unification does not capture the relationship between types of alternatives. Consider for example the following function, presented in [18]:

The generalization of the types of the alternatives in the definition of f is: $\textit{Erk}$ a b $\rightarrow$ c. Since type variable c is not associated to a GADT, types Int and Bool are unified, causing the definition of f to be rejected. However, for example with annotated type $\textit{Erk}$ a a $\rightarrow$ a this function can be given a proper type.

3.2 Term and Type Syntax

The context-free syntax of terms and types is presented in Fig. 2. For simplicity and following common practice, kinds are not considered in type expressions and type expressions which are not simple types are not explicitly distinguished from simple types. Type expression variables are called simply type variables. There is a distinguished type constructor that is written as an infix operator, $\tau \rightarrow \tau '$, as usual.

Fig. 2.

Syntax of terms and types

We use the following operations over typing contexts:

$$ \begin{array}{lcl} \varGamma (x) &{} = &{} \{\sigma \,\mid \,x : \sigma \in \varGamma \}\\ \varGamma ,x:\sigma &{} = &{} (\varGamma - \{ x: \sigma \mid \ \sigma \in \varGamma (x)\}) \cup \{x : \sigma \} \end{array} $$

We let: (i) ${ tv}(\sigma )$ denote the set of free type variables in $\sigma$, (ii) ${ gtv}(\sigma )$ denote the set of free type variables that occur in the type of a GADT type constructor, (iii) ${ gtc}(\tau )$ represent the set of GADT type constructors occurring in $\tau$ and (iv) ${ rtv }(\tau )$ denote the set of free type variables that occur in the type of a recursive algebraic data type, such as lists and trees (the set ${ rtv }(\tau )$ is used to avoid skolemization of type variables that occur in the type of the result of a generalized GADT function).

We use constraints to express a relationship between the return type of a function and its parameters, in case the type of parameters have a GADT constructor.

We also use the following notation to return the sets of constraints that contain types that mention GADT constructors:

$$ \kappa _x^\star = \{x : \tau \in \kappa \,\mid \,{ gtc}(\tau )\ne \emptyset \} $$

3.3 Algorithm Definition

For simplicity, we consider a language that is essentially core-ML extended with GADT functions — that is, we do not include inference of types of expressions with overloaded symbols. Readers interested in type inference for overloading are referred to [13].

The proposed algorithm is defined as a syntax-directed proof system, using formulas of the form $\varDelta \mid \varGamma \vdash e : (\kappa .\tau ,S)$, where $\varDelta$ is an environment of names of recursive function definitions that contains constraints to be used in the process of type improvement for case branches involving GADTs, $\kappa .\,\tau$ is the type inferred for e and S is a substitution (used to instantiate type variables for obtaining type $\kappa .\,\tau$). Notation $\delta (x,\tau ,\varDelta )$ associates, with a symbol x and a type $\tau$, constraint set $\{ x:\tau \}$, if x is a recursively defined symbol, otherwise an empty constraint set. It is defined as:

$$ \delta (x,\tau ,\varDelta ) = \mathtt{if}\ \,x \in \varDelta \ \mathtt{then}\ \{x : \tau \} \ \mathtt{else}\ \emptyset $$

Type inference rules are standard, with the exception of rules (VAR) and (CASE). The (VAR) rule generates a constraint for each symbol in $\varDelta$, used for improvement of types of GADT functions. Each variable x that is not in $\varDelta$ has a type with an empty constraint set (remember that, for simplicity reasons, overloading is not treated in this paper). The (CASE) rule is the main part of the algorithm. First, the type of case scrutinee e is inferred. Then, the type of each case alternative is inferred (in the textual order, but the order is not relevant). Finally, if the case expression involves GADT constructors, the type of the case expression is improved, by using a separate type improvement judgement (since case alternatives are not expressions). Distinct case alternatives for the same constructor must be unified, but in this paper we consider for simplicity that each case alternative has a distinct constructor.

In order to infer the type of a case alternative, we need to unify its constructor range type with the type inferred for the case scrutinee, producing a substitution that is used to instantiate the types of the parameters, and add them to the typing context to infer the type of the right-hand side of the alternative.

The judgement $\varGamma \Vdash _x \overline{(\kappa _i.\, \tau _i'\rightarrow \tau _i)} \leadsto (\tau ' \rightarrow \tau ,S)$ denotes the type improvement necessary for the inference of types of functions defined by pattern matching on a GADT function named x. Given a typing context $\varGamma$ and, for each alternative i, a set of constrained types $\kappa _i.\,\tau '_i\rightarrow \tau _i$, type improvement yields the improved type $\tau '\rightarrow \tau$. Note that only functions that have alternatives with polymorphic recursion generate constraints. ${ sat}(\kappa ,\varGamma )$ computes the improvement substitution S for a set of constraints $\kappa$, using type assumptions given by $\varGamma$. This judgement uses function ${ specialize}$ which computes a improvement substitution based on the types of the case alternatives and their generalization.

$$ \begin{array}{lcl} { specialize}(\tau ,\emptyset ) &{} = &{} id\\ { specialize}(\tau ,(\{\tau '\}\cup \mathbb {T})) &{} = &{} { unify}(\{\tau = \tau '\}) \circ { specialize}(\mathbb {T}) \end{array} $$

The type improvement judgement is defined as:

This judgement works as follows. For each equation i of a GADT function x, let $(\kappa _i)_x^\star$ be the set of constraints that mention GADT type constructors (in the constraint set of the type of the i-th equation) and let $S_i$ be the satisfiability substitution for this constraint set, in a typing context that contains type assumptions corresponding to all alternatives. Then, let $\tau _1 \rightarrow \tau _2$ be the ${ lcg}$ of all $\overline{S_i\,(\tau _i' \rightarrow \tau _i)})$. Now, we “skolemize” $\overline{\alpha }$ (i.e. treat them as non-unifiable), the set of type variables introduced by the generalization of types of parameters of a GADT. Type variables that occur in the return type of a function and also in the generalization of a parameter of a recursive algebraic type are not skolemized (for example, when the type [ a ] of the result is obtained from, say, the generalization of [ Int ] and [ Bool ]). The inferred types of case alternatives are then unified with non-skolemized type variables. The substitutions computed by satisfiability and unification are applied to the generalized type, which is then returned.

It is worth mentioning that the improvement judgement is conservative over non-GADT types, since $\kappa = \emptyset$ when alternative types do not involve GADTs, and no variable is skolemized, so all types must be unified.

3.4 GADT and Principal Type

In [22] Vytiniotis et al. argue that the principal type property offers fewer benefits than a guarantee of type safety (i.e. that well-typed programs will not cause an error at run-time). Consider for example the function eval, presented in Sect. 1, but now consider that it is declared with only the first alternative:

Our algorithm infers type (Term Int $\rightarrow$ Int) for eval, but in Haskell the following type annotations would be allowed for eval: $\forall a.$ Term $a \rightarrow a$ and $\forall a.\,$ Term $a \rightarrow { Int}$. None of these types is an instance of the other.

In our view, the type Term Int $\rightarrow$ Int is a good choice in this case, since it avoids expressions such as, for example, eval ( IsZ ( Lit 1)), for which there exists no alternative in the definition of eval. With the algorithm given in [22] the following implication constraint is generated during type inference:

Note that substitution $\{ c\mapsto { Int}\}$ is a solution to this implication constraint and application of this substitution leads to the inference of type Term $a \rightarrow { Int}$. However, in this constraint variable c is considered untouchable, and then type inference fails in GHC. Again, in GHC version 7.6.x, the function eval defined with only this alternative would have inferred type $\forall a.\,{ Term}\ a \rightarrow { Int}$; from version 7.8.1 type inference fails, due to type variable being considered untouchable.

On the other hand, by adding the alternative of constructor IsZ, where the type Term Bool is returned by the constructor, the type of eval becomes: $\forall a.\,$ Term $a \rightarrow a$, which is the same as the type inferred by our algorithm. It is important to point out that the type Term Int $\rightarrow$ Int, inferred by the alternative of constructor Lit, is an instance of this type, in contrast with the case of Term a $\rightarrow$ Int.

Back to type safety, it would be desirable that in this case the type inference algorithm restricts instances of a to either Int or Bool; however, this seems to need a special way of constraining polymorphic types.

In many cases, such as that of Example 1, a relation between the types of alternatives is not expressed by the code in these alternatives. In these cases there is no guarantee that the inferred type is the principal type.

4 Related Work

Peyton Jones et al. present an extension of Haskell’s type system for the support of GADTs [6, 7]. The verification of the types of GADT functions is done using type annotations. These types, called rigid types, are propagated to inner scopes by means of some specific rules. Pottier and Régis-Gianas [12] define a two-pass type inference algorithm, separating traditional Hindley-Milner type inference from the propagation of explicit type annotations. This separation makes the mechanism of type propagation more efficient.

The type inference algorithm used in [15, 22], called OutsideIn, extracts type constraints from expressions occurring in inner scopes and solves these constraints in the outermost scope, avoiding an ad hoc approach for the propagation of rigid types. Besides using a more natural mechanism for propagation of annotated types, this approach enables more helpful error messages and type inference in a restricted number of function declarations. In these cases a rather restrictive rule is adopted in the definition of untouchable variables, so that only the types of functions for which the existence of a principal type can be guaranteed are inferred. In [19] Sulzmann and Schrijvers introduce some ideas adopted in the OutsideIn algorithm.

Lin and Sheard present the Pointwise GADT type system [9], that uses a modified unification algorithm to support parametric instantiation and type indexing. In [8] Lin proposes algorithm $\mathcal {P}$, more restrictive than Pointwise, that does not require type annotations. The algorithm applies generalization only in patterns of alternatives and supports polymorphic recursion. Differently from our proposal, which handles polymorphic recursion similarly to overloading, algorithm $\mathcal {P}$ uses an approach similar to that used by an iteration limit to guarantee termination.

5 Conclusion

In this paper we have presented a type inference algorithm in the presence of GADTs. The ideas behind the algorithm are intuitive and easy to understand.

The presented algorithm handles alternative definitions of a defined symbol x as if they were overloaded definitions of x, in a closed world approach to overloading, with support for polymorphic recursion. The algorithm makes use of anti-unification to capture the relation between the types of distinct alternatives of a function that has a parameter or returns a GADT. Types which must not be unified are separated, before unifying the types of the alternatives. This enables type inference for functions that typically require type annotations in other implementations, such as that of GHC.

Further study in order to provide support for type annotations is necessary. When there is a relation from the types of arguments to the type of the result of a GADT function which is not made explicit in the code (e.g. Example 3), our type inference algorithm can reject expressions that could be considered type-correct.