54: Dependent Types

We start with my addiction to programming books, and end with dependent types, that's a logical path, right?

yeah, so dependent types? > In computer science and logic, a dependent type is a type whose definition depends on a value. A "pair of integers" is a type. A "pair of integers where the second is greater than the first" is a dependent type because of the dependence on the value. It is an overlapping feature of type theory and type systems.

Terms:

Set:

An unordered collection of unique values

Parametric types:

Like parametric polymorphism. A function or data type that can be written generically so that it can handle values identically without worrying or knowing their types.

An example of this would be append or concat two lists together. append: [a] -> [a] -> [a] Now a while ago, I would have read that and thought, WTF. or maybe the Identity property because it keeps using the a over and over again. BUT with the bit of knowledge on the subject I have I know that append does not care what type you have in the list. A list of Int, or Strings, doesn’t matter, as long as they are the same type in both lists. And finally that it will always give you back a list of the same type as the first and second list arguments.

Total Function:

A function that maps all of it’s possible input values to an output value.

Opposite would be a partial function, NOT partial application which is immediately what I thought of. Simply a function that is defined for for all possible input values. It terminates and returns a value. So when would you want a partial function? When the exact domain is not known. (I have no idea what that means) Often used in Computability theory, also known as recursive theory. Picks Resources

Dependent Type

Little Typer

David Thomas’ Elixir Programming

Will Kurt’s “Get Programming with Haskell”

A Philosophy of Software Design 1st Edition by [John Ousterhou]

Elixir Outlaws

Geek Sublime

Reasoned Schemer

Follow

JavaScript to Elm

Twitter: @jstoelm
Email: [email protected]

Jesse Tomchak

Twitter: @jtomchak