Course imparted by Robert Harper. I believe they are following the Homotopy Type Theory book. See also Harper's blog and the latest edition of his Practical Foundations for Programming Languages book. See also the "proof theory foundations" videos linked in the "So you want to learn type theory... but where to start?" page.
Showing posts with label types. Show all posts
Showing posts with label types. Show all posts
Monday, April 25, 2016
Friday, November 14, 2014
Pawn shops, refrigerators, and contravariant functors
Recently, I learned (by reading instance declarations in Haskell) that the composition of contravariant functors is covariant.
In this talk (around 27:30) Erik Meijer tells a colorful analogy for contravariance in subtyping. The analogy involves trashcans, which apparently are contravariant. I wonder if I can find a similar analogy for the case of composition, because I find it difficult to gain an intuition for it.
So, consider bananas. Bananas are a type of fruit.
Consider refrigerators as well. There are different types of refrigerators. Some have a technology advanced enough to freeze any fruit, but some are more modest and can only freeze bananas.
The refrigerators that can freeze any fruit are a subtype of the refrigerators that can freeze bananas. Because, any time you need to freeze a banana, you can freeze it in one of the refrigerators than can handle any kind of fruit.
In other words, refrigerators are contravariant.
Now consider pawn shops. Paws shops are contravariant as well: anything you can sell to a pawn shop that only takes rings, you can sell to a pawn shop that takes any jewelry. The pawn shops that take any jewelry are a subtype of the pawn shops that take rings.
There are also pawn shops for refrigerators. For example pawn shops for refrigerators that can freeze any fruit, or pawn shops for refrigerators that can freeze bananas. (Yes, they are quite specialized pawn shops, but bear with me.)
The pawnbrokers are very meticulous. Before accepting a refigerator for sale, they put inside it a viand of the type associated with the pawn shop, to check that the refrigerator indeed works.
Can you sell to the pawn shop of refrigerators that freeze bananas everything you could sell to the pawn shop of refrigerators that freeze any fruit? The answer is yes. You take the refrigerator that freezes any fruit to the pawn shop, the pawnbroker puts a banana on it, and it gets frozen. Deal!
So pawn shops for refrigerators are covariant on the type of viands that the refrigerators can freeze.
Whew, that was convoluted.
In this talk (around 27:30) Erik Meijer tells a colorful analogy for contravariance in subtyping. The analogy involves trashcans, which apparently are contravariant. I wonder if I can find a similar analogy for the case of composition, because I find it difficult to gain an intuition for it.
So, consider bananas. Bananas are a type of fruit.
Consider refrigerators as well. There are different types of refrigerators. Some have a technology advanced enough to freeze any fruit, but some are more modest and can only freeze bananas.
The refrigerators that can freeze any fruit are a subtype of the refrigerators that can freeze bananas. Because, any time you need to freeze a banana, you can freeze it in one of the refrigerators than can handle any kind of fruit.
In other words, refrigerators are contravariant.
Now consider pawn shops. Paws shops are contravariant as well: anything you can sell to a pawn shop that only takes rings, you can sell to a pawn shop that takes any jewelry. The pawn shops that take any jewelry are a subtype of the pawn shops that take rings.
There are also pawn shops for refrigerators. For example pawn shops for refrigerators that can freeze any fruit, or pawn shops for refrigerators that can freeze bananas. (Yes, they are quite specialized pawn shops, but bear with me.)
The pawnbrokers are very meticulous. Before accepting a refigerator for sale, they put inside it a viand of the type associated with the pawn shop, to check that the refrigerator indeed works.
Can you sell to the pawn shop of refrigerators that freeze bananas everything you could sell to the pawn shop of refrigerators that freeze any fruit? The answer is yes. You take the refrigerator that freezes any fruit to the pawn shop, the pawnbroker puts a banana on it, and it gets frozen. Deal!
So pawn shops for refrigerators are covariant on the type of viands that the refrigerators can freeze.
Whew, that was convoluted.
Monday, November 10, 2014
Two new "validation" applicatives
There exists an Either-like Applicative (usually called "Validation") that either collects all the errors, or returns a success. This is different from the Monad instance of Either, that stops at the first error encountered.
The type can be found at the validation package. However, that package incurs on a heavy lens dependency.
Recently, the type has cropped up without the lens dependency in both transformers (as the Errors type synonym) and either (as Validation).
The version in the either package has a more precise type, as it only requires the error values to form a Semigroup, but not necessarily a Monoid. So you can use a NonEmpty to accumulate errors.
The type can be found at the validation package. However, that package incurs on a heavy lens dependency.
Recently, the type has cropped up without the lens dependency in both transformers (as the Errors type synonym) and either (as Validation).
The version in the either package has a more precise type, as it only requires the error values to form a Semigroup, but not necessarily a Monoid. So you can use a NonEmpty to accumulate errors.
Friday, May 31, 2013
Haskell equivalents of some Clojure forms
While trying to learn Clojure, I keep confusing doall, dorun, and doseq. What are their differences, and when to use each one?
The functional language I know best is Haskell, so I will find what Haskell functions correspond to the Clojure ones, using Hoogle.
The documentation says:
In Haskell, values which are obtained through side effects are "tagged" with the IO monad, to distinguish them from pure values. A value of type IO a could be understood as "a description of a program that, when run, produces a value of type a".
We want a function with a type like this:
We put the signature in Hoogle, we find the following
The documentation says:
Let's then search for the signature
The documentation says:
So we must search Hoogle for something like
A good introduction to Haskell IO can be found here.
The functional language I know best is Haskell, so I will find what Haskell functions correspond to the Clojure ones, using Hoogle.
doall.
The documentation says:
When lazy sequences are produced via functions that have side effects, any effects other than those needed to produce the first element in the seq do not occur until the seq is consumed. doall can be used to force any effects. Walks through the successive nexts of the seq, retains the head and returns it, thus causing the entire seq to reside in memory at one time.Ok, we have a list where each element is produced through a side effect. Using doall we perform all these effects "up front" and get the whole list as a result.
In Haskell, values which are obtained through side effects are "tagged" with the IO monad, to distinguish them from pure values. A value of type IO a could be understood as "a description of a program that, when run, produces a value of type a".
We want a function with a type like this:
[IO a] -> IO [a][] is the type constructor for lists. -> means a function from some type to another. For simplicity, in this post we only deal with lists whose elements are all of the same type.
We put the signature in Hoogle, we find the following
sequence :: Monad m => [m a] -> m [a]
Evaluate each action in the sequence from left to right, and collect the results.The type is more general but, when m is IO, this is the function we are looking for.
dorun.
The documentation says:
When lazy sequences are produced via functions that have side effects, any effects other than those needed to produce the first element in the seq do not occur until the seq is consumed. dorun can be used to force any effects. Walks through the successive nexts of the seq, does not retain the head and returns nil.In Haskell, functions which are executed only for side effects return values of type (). There is only one such value, also named (). It's roughly similar to void in C and Java.
Let's then search for the signature
[IO a] -> IO ()We find
sequence_ :: Monad m => [m a] -> m ()
Evaluate each action in the sequence from left to right, and ignore the results.The trailing underscore is a notational convention. It means that this is a function that behaves like the one without the underscore, but ignores the return value.
doseq.
The documentation says:
Repeatedly executes body (presumably for side-effects) with bindings and filtering as provided by "for". Does not retain the head of the sequence. Returns nil.Ok, it seems that now the values in the input list are "pure", but we want to apply an effectful function to each one of them. And we do not care about the return value.
So we must search Hoogle for something like
[a] -> (a -> IO b) -> IO ()We find
forM_ :: Monad m => [a] -> (a -> m b) -> m ()So that's it. doall is sequence, dorun is sequence_, doseq is forM_. I won't confuse them anymore!
A good introduction to Haskell IO can be found here.
Subscribe to:
Posts (Atom)