Re: [Caml-list] coinductive data types

["François Pottier" <francois.pottier@inria.fr>]

Hello,

Le 30/08/2022 à 18:32, Aaron Gray wrote:
 > What I have gathered is that in order to have completeness of type
 > system and soundness you need the type system to be implemented as a
 > type lattice, there by underpinning the system on to a topological
 > space and thus being constructable and well founded.

I am not sure what you mean by "soundness and completeness of the system".

A type system is considered "sound" if a well-typed program cannot crash.

A type-checking or type inference algorithm is considered "sound and 
complete"
provided it declares a program well-typed if and only if this program is
indeed well-typed. (I am simplifying the statement a bit.) This implies that
the property of being well-typed is decidable.

It is not necessary in principle for the subtyping relation to be a lattice.
The lattice property can help (e.g. it can help simplify subtyping
constraints, when performing type inference in the presence of subtyping).

 > I don't know how accessible OCaML's, type system code is. I have had a
 > brief look, I am used to Haskell, and Haskell's type annotations in
 > order to get my bearings.
 >
 > Are there any papers on OCaML's type system proper at all please ?

The code of the OCaml type-checker is publicly available but is not easy
to read.

There are several papers covering several aspects of the type system, 
but I am
not sure which one would be most relevant here. Perhaps "GADTs Meet 
Subtyping"
by Gabriel Scherer and Didier Rémy, which discusses the combination of
*generalized* algebraic data types and subtyping.

I hope this helps,

--
François Pottier
francois.pottier@inria.fr
http://cambium.inria.fr/~fpottier/