Dialogue Systems and Type Theory