But isn't this example similar to the idea of literal types?; defeating the need for such checks can avoid runtime costs as well as add specificity and safety to function signatures. Maybe I misunderstood some subtlety.
On Thu, Jul 2, 2020, 4:51 PM gmhwxi <[email protected]> wrote: > > Today, I encountered a very interesting issue involving dependent types. > > Say, I have a string "abcde". Then I can use the string to create a > predicate P: > > val P = fmemq("abcde"): bool > > Given a char x, P(x) returns true if and only if x appears in the string > "abcde". > > What is the type for P? > > In a non-dependent type system, P is usually given the type: (char) -> > bool. > > Given a sequence xs containing elements of type T, fmemq(xs) returns a > function > of type (T) -> bool. For the string "abcde", this T is precisely the type > for chars > ranging over "abcde". In other words, fmemq("abcde") is a function that > can be applied > to a char c only if c appears in "abcde". This defeats the very need for > fmemq("abcde"): > If it can ever be applied, then the application always returns true. > > Have fun! > > --Hongwei > > > > But in a dependent type system, > > -- > 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 view this discussion on the web visit > https://groups.google.com/d/msgid/ats-lang-users/61afb765-afe1-48be-a3fe-12e33b28b924o%40googlegroups.com > <https://groups.google.com/d/msgid/ats-lang-users/61afb765-afe1-48be-a3fe-12e33b28b924o%40googlegroups.com?utm_medium=email&utm_source=footer> > . > -- 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 view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/CAORbNRrQFH7hZtX17K9eEdjC2BQk85trMA8zm0_%2BZ7aGxpLGzw%40mail.gmail.com.
