[PR-1091] Article about type inference #2
Conversation
Heimdell
requested review from
dcastro,
Haskell-mouse,
int-index,
NaeosPsy,
serokellcao and
sras
| </td> | ||
| <td> | ||
| the type of all types (including the `Type` itself) | ||
| </td> |
There was a problem hiding this comment.
Do we have a sort of TypeInType? Is it for simplicity? I would emphasise this moment in more detail.
There was a problem hiding this comment.
Yes, exactly. Otherwise I have to use either additional Box or a hierarchy, which requires Nat-s and their arithmetics to be somehow present.
| type Refeshes m :: Constraint | ||
|
|
||
| refresh :: Refreshes m => Name -> m Name | ||
| ``` |
There was a problem hiding this comment.
Do you have an implementation of refresh? Without that, the section looks a bit incomplete to me.
| Using that, we can return scope-correct programs right off the parser. | ||
|
|
||
| _Pro tip learned after a debug session_: Refreshing names of records field declarations in record literal is a bad idea. | ||
|
|
There was a problem hiding this comment.
To me, it's worth explaining why this is a bad idea in a couple of sentences. The reader might not get your point.
| We can construct the program. Before we're doing inference, we need an auxillary mechanism. It whill compare two types and either find a set of substitutions to convert both to the same type, or bail out with error if that isn't possible. This mechanism is called unification. | ||
|
|
||
| Usially, in Hindley-Milner inference, the type of unifier is | ||
|
|
There was a problem hiding this comment.
It's worth referring to some paper on Hindley-Milner inference to make the post more self-contained.
| unify (Lam n t b) (Lam m u c) = do | ||
| unify t u | ||
| unify b (subst (Bound m ==> Rigid n) c) | ||
| ``` |
There was a problem hiding this comment.
why do you repeat unify (Lam n t b) (Lam m u c) = do twice?
There was a problem hiding this comment.
unify (Pi n t b) (Pi m u c) = do
unify t u
unify b (subst (Bound m ==> Rigid n) c)
unify (Lam n t b) (Lam m u c) = do
unify t u
unify b (subst (Bound m ==> Rigid n) c)Where? The first clause is for Pi-types.
There was a problem hiding this comment.
They just appear to have the same unification procedure.
| axiom "True" Bool | ||
| axiom "True" Bool | ||
| axiom "Bool" Type | ||
| ``` |
There was a problem hiding this comment.
Are these something like inference rules for values?
There was a problem hiding this comment.
Yes, they are runtime constructor reps, with the type.
| ) | ||
| => AST | ||
| -> Sem m AST | ||
| ``` |
There was a problem hiding this comment.
An implementation detail - https://hackage.haskell.org/package/polysemy-1.6.0.0/docs/Polysemy.html#t:Sem
| infer t | ||
|
|
||
| let k = telescope args Star | ||
| check k Star |
There was a problem hiding this comment.
Wow, the key place. I would explain what telescope is.
There was a problem hiding this comment.
In a couple of words, ofc. There's no need to write a monograph about that.
| infer b | ||
| ``` | ||
|
|
||
| In case of mutually-recursive definitions, theor bodies (but not the types!) might depend on each other, so we have to bind the constructors to whatever is present in the declarations and do the inference only _after_ we enter the block context. |
| ## Conclusion | ||
|
|
||
| The presence of the typechecker not only allows you to "prevent programs from crashing", but also - if the type system is powerful enough - to partially shift your work onto compiler, by forcing it to implicity calculate some types and, potentially, generate code from them. | ||
|
|
There was a problem hiding this comment.
I guess the post requires a further reading section.
And mentioning our post written with Vlad :pled:
No description provided.