Dependent Types


 

 

10.2.1 Dependent Types

TBoS 261-262

We'll now look at types not readily formalised in some of the Hindley-Milner languages. In mainstream functional languages, terms to the left of : and types to the right of : are disjoint. In dependent types, types either incorporate terms or terms types. Here's an example; I want a dependently typed function myprog that takes a type as an input and enforces that type on the input. myprog does nothing special in this example; it simply returns the input.

(0-) (datatype my-prover-types

  P : Type;
  _______________________
  (myprog Type P) : Type;)
type#my-prover-types 

(1-)(define myprog
      Type P -> P)
(fn myprog)

(2-) (tc +)
true

(3+) (myprover symbol p)
p : symbol

(4+) (myprog number p)
type error
1. Introduction

2. License

3. History

4. The Core Language

4.1 Base Types
4.1.1 Symbols
4.1.2 Strings
4.1.3 Numbers
4.2 Function Applications
4.3 The Top Level
4.4 Arithmetic
4.5 Comments

4.6 Sequences

4.6.1 Lists
4.6.2 Tuples
4.6.3 Vectors

4.7 lambda and let
4.8 Global Assignments
4.9 Higher Order Functions
4.10 Lazy Evaluation
4.11 I/O
4.12 Loading Files
4.13 Streams
4.14 Exceptions
4.15 Hashing
4.16 Property Lists
4.17 Eval

5 Defining Functions

5.1 Partial Functions
5.2 List Handling Functions
5.3 String Handling Functions
5.4 Tuple Handling Functions
5.5 Vector Handling Functions
5.6 Guards
5.7 Backtracking
5.8 Writing in Kλ
5.9 Macros

6. Packages

7. Shen-YACC

7.1 Recognisor Generator
7.2 Semantic Actions

8. Shen Prolog

8.1 Sample Programs

9. Types

9.1 Types and Constructors
9.2 Functions and Types
9.3 Synonyms

10 Sequent Calculus

10.1 Recursive Types

10.2 Exotic Types

10.2.1 Dependent Types
10.2.2 Negative Types
10.2.3 Subtypes
10.2.4 The Type of All Sets

11 Glossary of Functions

12 The Syntax of Shen

Built by Shen Technology (c) Mark Tarver, September 2021