This page how the various expression constructs in monad-embed behave during type inference. The first column shows an example of an expression. The second and third columns show the free variables and type-equalities that are created for the type inference system to solve.
| Expression | Free type vars | Type constraints |
|---|---|---|
x = \ arg -> body |
m :: * -> * a :: * b :: * |
x :: {m} (a -> {m} b);
arg :: (n :: * -> *)
=> {n} a;
body :: {m} b; |
x = fun arg |
m :: * -> * a :: * b :: * |
fun :: {m} (a -> {m} b);
arg :: {m} a;
x :: {m} b; |
x = \ [arg] -> body |
m :: * -> * n :: * -> * a :: * b :: * |
x :: {m} [{n} a] -> {m} b;
arg :: {n} a;
body :: {m} b; |
x = fun [arg] |
m :: * -> * n :: * -> * a :: * b :: * |
fun :: {m} [{n} a] -> {m} b;
arg :: {n} a;
x :: {m} b; |
1234567 |
m :: * -> * |
1234567 :: {m} Number; |
x = case subj of {
Con field -> value;
} where
data T = {
Con U;
}; |
m :: * -> * b :: * |
subj :: {m} T;
field :: (n :: * -> *)
=> {n} U;
value :: {m} b;
x :: {m} b; |
x = case subj of {
Con [field] -> value;
} where
data T = {
Con [{M} U];
}; |
n :: * -> * b :: * |
subj :: {n} T;
field :: {M} U;
value :: {n} b;
x :: {n} b; |
x = do {
var = value;
} then rest |
m :: * -> * a :: * b :: * |
value :: {m} a;
var :: (n :: * -> *)
=> {n} a;
rest :: {m} b;
x :: {m} b; |
x = do {
var =[] value;
} then rest |
m :: * -> * n :: * -> * a :: * b :: * |
value :: {n} a;
var :: {n} a;
rest :: {m} b;
x :: {m} b |
x = do {
thing;
} then rest |
m :: * -> * a :: * b :: * |
thing :: {m} a;
x :: {m} b; |