Hacker News Reader

Comment by weavie | Hacker News Reader

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) elem

only works because the compiler can know exactly what is going to happen to those parameters in the function. It can guarantee that there are no side effects that can randomly and non-deterministically come along and change the result. The `Vect n elem` input parameter is always going to be a parameter of n elements. If the function changed n to be (n + 1) then should the result be `Vect (n + 1 + m) elem` or still `Vect (n + m)`? Things get a lot harder to lock down!

View on HN

+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.

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.

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

    #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;
    }

Reply on news.ycombinator.com