What I had in mind is proof search. Given a type, which represents a theorem, synthesizing an argument of the type is like searching a proof for the theorem. Sometimes, a theorem has only one (natural) proof. In such a case, there is no ambiguity as to which proof should be used: There is only one.
On Friday, March 9, 2018 at 5:00:46 AM UTC-5, Brandon Barker wrote: > > My (likely incorrect) understanding from theory is that type families are > required for dependent types, or are even synonymous with dependent types. > When you said " the ability to synthesize an argument according to the type > of the argument", it sounds like a type family. And ATS has support for > dependent types, but maybe it is too restricted for this? -- You received this message because you are subscribed to the Google Groups "ats-lang-users" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To post to this group, send email to [email protected]. Visit this group at https://groups.google.com/group/ats-lang-users. To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/5f68212f-553a-4657-9fd4-5ec99e04ae6b%40googlegroups.com.
