3 ms·

I'm not sure how it would be possible to have dependent types in a non-pure language. A function such as append: Vect n elem -> Vect m elem -> Vect (n + m)

• ihm 8y ago
  +1. If the language is not pure it's unclear how type checking would work. To make things even clearer, consider the following example (in a hypothetical dependently typed language with mutable references): f : () -> Type f = let r = ref 0 in fun () -> let t = if !r = 0 then Int else String in r := r + 1; r x : f () x = 17 y : f () y = "foo" Should this program type check? I think there is a consistent way to talk about type checking here (if there is a canonical ordering of all definitions across all files) but it seems unlikely you'll get a system that's easy to understand.
• saurik 8y ago
  I don't understand the issue... it is trivial and in fact extremely common-place in impure languages to fundamentally disallow modifications to something's type. C++, which is definitely not pure but yet essentially has dependent types, is easily able to express this exact thought without problem, as your ability to modify things at runtime is extremely limited. (Of course, the place where C++ is limited is its inability to template over non-concrete values, but I see nothing about its model that fundamentally limits its ability to conceptualize such a thing. It is still technically a dependently typed language even without the ability to do this, of course.) [edit: matt-noonan has told me that I am wrong on that last comment :(... so not "of course".] #include <stdlib.h> template <size_t S, typename E> class Vect { private: E data[S]; public: const size_t size() const { return S; } E &operator [](size_t i) { return data[i]; } const E &operator [](size_t i) const { return data[i]; } }; template <size_t N, size_t M, typename E> Vect<N + M, E> append(const Vect<N, E> &l, const Vect<M, E> &r) { Vect<N + M, E> v; for (size_t i(0); i != N; ++i) v[i] = l[i]; for (size_t i(0); i != M; ++i) v[N+i] = r[i]; return v; } int main() { Vect<4, int> a; Vect<2, int> b; Vect<6, int> c = append(a, b); Vect<8, int> d = append(a, b); return 0; } test.cpp:36:18: error: no viable conversion from 'Vect<4UL + 2UL aka 6, [...]>' to 'Vect<8, [...]>' Vect<8, int> d = append(a, b); ^ ~~~~~~~~~~~~ test.cpp:4:7: note: candidate constructor (the implicit copy constructor) not viable: no known conversion from 'Vect<4UL + 2UL, int>' to 'const Vect<8, int> &' for 1st argument class Vect { ^ 1 error generated.
  • weavie 8y ago
    I wasn't aware that C++ could do this. It's come on a long way since I last looked at it! How far can it take these dependent types? Can you specify a function in the type signature that is called by the compiler that can determine the type of the parameter? Something like : stringOrInt:: Bool -> Type stringOrInt True = String stringOrInt False = Int doSomething:: x: Bool -> StringOrInt x -> String doSomething can then be called like : doSomething True "Ook" doSomething False 4
    • greydius 8y ago
      #include <iostream> template<bool B, typename T> std::string doSomething(T t); template<> std::string doSomething<true>(std::string s) { return "true!"; } template<> std::string doSomething<false>(int i) { return "false!"; } int main() { std::string foo {"foo"}; auto s1 = doSomething<true>(foo); auto s2 = doSomething<false>(42); std::cout << s1 << ", " << s2 << std::endl; return 0; }