Here is another way to see the issue I mentioned in my original message.
Say we have the following interface:
fun
<a:type>
fmemq(xs: list(a)): (a -> bool)
The function fmemq is supposed to turn a given list into a function that
checks if a given
element is in the given list.
Suppose that we do
val foo = fmemq(xs) where { val xs = 1::2::3::nil() }
Say we infer a dependent type list(T) for the list xs where T = [a:int |
a=1 || a=2 || a=3] int(a).
Note that T is the type precisely for the three integers 1, 2, and 3. Then
the function foo is of
the type (T -> bool), which make foo not a very useful function. Why?
Because foo is actually
a constant function that maps every integer in its domain to true. This is
just an interesting example
showing that inferring the "most accurate" types may not actually be what
the programmer really wants.
On Thursday, July 2, 2020 at 5:52:44 PM UTC-4, Brandon Barker wrote:
>
> 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 <...> 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/aff4fdba-4139-4fc9-9968-41f9087eba24o%40googlegroups.com.
