stelleg

Sometimes it would be nice if a type system could automatically "do it's best"
to restrict what a value will be. For example, the type `Bool` is the compiler
saying the value will either be `True` or `False`, but it doesn't know which.
What we want is the compiler to be able to be precise when possible, so instead
of always saying `Bool` (or "I don't know"), it could say `True`, `False`, or
`Bool`. This gist shows how Hindley Milner already has this capability that can
be exercised by using Church or Scott encodings of simple data types.

> {-# LANGUAGE RankNTypes #-}
> import qualified Data.Maybe as M

stelleg

module Expr
import Data.Vect
import Data.Fin

data Expr : Nat -> Type where
  Var : Fin n -> Expr n
  Lam : Expr (S n) -> Expr n
  App : Expr n -> Expr n -> Expr n

data Closure : Type where

stelleg

import Control.Monad

lorem = "Lorem ipsum dolor sit amet, consectetuer adipiscing elit. Donec \
\ hendrerit tempor tellus. Donec pretium posuere tellus. Proin quam \
\ nisl, tincidunt et, mattis eget, convallis nec, purus. Cum sociis \
\ natoque penatibus et magnis dis parturient montes, nascetur ridiculus \
\ mus. Nulla posuere. Donec vitae dolor. Nullam tristique diam non  \
\ turpis. Cras placerat accumsan nulla. Nullam rutrum. Nam vestibulum  \
\ accumsan nisl. \n"