1
$\begingroup$

"Core language" refers to the exported well-typed terms that can be evaluated (or reduced).

In the core language of MiniAgda, a dependently-typed language, the parameter type of a lambda is not stored anywhere. So does in Mini-TT and Agda.

However, Idris does store lambda parameter type in its core language.

I wonder do we need/needn't to store parameter type (or, under what condition do we need/needn't to store it)? Because according the surface syntax of all these languages, they don't have lambdas with their parameters explicitly-annotated. For Idris here's a link showing that Idris does not have lambda with type annotation.

$\endgroup$
  • 1
    $\begingroup$ MiniTT uses a bidirectional type system. The lambda abstraction case is always in type checking mode, so the system assumes that the type of the lambda expression is given. Note that declarations always include a type annotation. $\endgroup$ – frabala Jun 2 at 10:02
1
$\begingroup$

In general, type inference for dependent types is undecidable. This means that when checking a function, we need some way to know what type its argument has.

In the case of Idris, they simply annotate lambdas with parameter types. This is very common in type theory, since it makes your type system syntax directed in a very simple way. When you do this, you can usually view the typing judgment as having the type as an output parameter (i.e. given the input term, you can determine its type).

I don't know what MiniAgda does in particular, but the other main way is to treat the type as an input to the checking judgment. So in this case, you don't need to store the type of the function in the AST, but when typechecking, you will use the context in some way to get the type of the function (i.e. from an annotation).

Generally this is done using bidirectional typechecking. This paper and this post both give excellent overviews of how this can be done in practice.

$\endgroup$
  • $\begingroup$ But Idris does not have type annotation for lambdas syntactically, just like Agda/MiniAgda/MiniTT. They're only different in their core language representation. This falsifies "it makes your type system syntax directed in a very simple way". $\endgroup$ – ice1000 Jun 2 at 5:26
  • $\begingroup$ I should update the question -- this sounds like something necessary for people who are not familiar with these languages to understand my question. $\endgroup$ – ice1000 Jun 2 at 5:27
  • $\begingroup$ @ice1000 "This falsifies..." No it doesn't, because Idris's type system is defined by its core language. An expression is well typed if it elaborates to a well typed core term. You want your core language to be simple and facilitate easy checking, which is why they include the types in the core but not in the surface language, where they get the types from annotations. It's about separation of concerns: getting types from context is done in elaboration, so that when the core is typechecked, all the necessary information is already there. $\endgroup$ – jmite Jun 2 at 21:08
  • $\begingroup$ I got it, thanks. $\endgroup$ – ice1000 Jun 3 at 1:16

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.