Add let type to the language

[dhess]

Currently, we use let type in evaluation, but we don't make this binding available to the student. So far as we can tell, there seems to be no good pedagogical reason not to do this. There are some implementation issues to consider, however (e.g., good informational/error messages when a student-defined let type binding doesn't match the expected type of a hole), so we'll punt on this until post-Primer 1.0. Until then, this issue serves as a tracker.

[brprice]

One implementation issue I am worried about is what to show as "the type of the currently selected node". If this is somewhere under a lettype v = T, then it is hard to be consistent about showing v vs T in the displayed type.

In particular, there are three scenarios I have in mind (and possibly more if I thought for longer)

• user specifies v or T: in a situation like _ :: v or _ :: T we should obviously report "the type you need to fill this hole with is v" (or T, respectively). Although, it may be useful to also display the other option: what if we have (λx . f (_ :: v)) :: T -> Bool: then presumably we would say x :: T and _ :: v and it may not be obvious to the student that you can you x to fill the hole. (Also, we should consider what to say if we ask the mechanical question "what variables fit here" -- surely we want to report x. This would be fairly easy, but also easy to forget!)
• we happen to synthesise T (from whole cloth, rather than synthesising a v). Some examples
  • lettype N = Nat in Zero
  • lettype N = Nat in let x = Zero :: N in x (here when we recursively synthesise the type for x we may well get N directly, cf the above point)
  • lettype N = Nat in let x = Zero :: N in Succ x (I guess here we have Succ :: Nat -> Nat and x :: N. How to make it clear that these can compose, and what type to give to the result)
  • lettype T = Maybe Bool in Just False (Here we synthesise a Maybe Bool from whole cloth, but it just so happens to be equal to a locally-bound T)
• TC breaks it down then builds up: I'm sure there must exist situations where the user explicitly gives a locally-bound type T which happens to be composite and then the TC must decompose said type to do its job. Presumably it is possible for the eventually synthesised type to be created out of these decomposed pieces (and thus not mention T) but still be equal to T. This seems rather difficult to detect. Thus I expect that even if we had consistent rules for the above points (when to display the alias and when the original), we would not be able to be consistent all the time.

One possibility may be to take advantage of the interactivity and display (say) the expanded type, but highlight portions that are equal to some locally-bound type and then if the student clicks on such a highlight we could switch to displaying the alias. Note however that aliases can overlap/clash (at least in a nested fashion: lettype a = Nat; lettype b = List Nat).

See also #5 (comment) and the #5 (comment)

I'm sure there is prior work on this topic, but I am not familiar with it.

[georgefst]

One possibility may be to take advantage of the interactivity and display (say) the expanded type, but highlight portions that are equal to some locally-bound type and then if the student clicks on such a highlight we could switch to displaying the alias.

I'd certainly ideally like us to explore something like this, where the student can view both the alias and the expansion.

I guess it's quite a hard problem though. Witness GHC's unpredictable behaviour around whether type synonyms show up in error messages.