4 ms·

>When you can get a functional language to type check, it really does Just Work. Not all functional languages have static typing. Also type checking helps, bu

by synthc 6y ago

>When you can get a functional language to type check, it really does Just Work. Not all functional languages have static typing. Also type checking helps, but saying that if the types check out it just work it pushing it IMO. No type checker will catch this error: sqrt :: double -> double sqrt x = x sqrt 10

AnthonBerg 6y ago
Dependent types are able to express the constraints that prevent or catch this error. The types of the arguments to the function can have value constraints on it, and those constraints can be determined from a value that exists there: the name of the function.
- AlotOfReading 6y ago
  Not only do dependent types have huge decidability issues, it's my understanding that integrating them with side effects is still an area of active research.
  - AnthonBerg 6y ago
    I think fortunately those are orthogonal matters :) First, I don't know that dependent types have huge decidability issues that are an inherent obstacle in general; Idris for one has a very practical and elegant model of computation – things like totality checking, linearity rules and elimination of "scaffolding" types do a lot for us. Dependent types do allow telling the compiler about more dimensions to consider – in a way that allows for a computational explosion at compile time – but those were always an available to consider as part of the computation; Dependent types dont add that complexity, rather they allow us to address it in the type system. I see it such that we're in a stronger position to manage and navigate that complexity by allowing us to express it to the compiler in a succinct and clear way near the core context of desired action. Dependent types allow us to do less by allowing us to do more. And integrating purely functional mechanisms with side effects is a fun and interesting avenue of research, and I don't know that adding dependent types makes that more difficult; I'd think it makes it easier?
    - AnthonBerg 6y ago
      To continue the thought: This dependent type is expressible, trivially decidable, and has no additional side effect burden: "This function's type depends on its function name. If its function name is "sqrt", then {check some simple rules about square roots, like if x is 0 then output is 0, if x > 1 then output < x, etc.}" This one too: "This function's type depends on its function name. If its function name is "sqrt", then check that it calls and returns a formally verified square root function applicable to its input type that is known to be decidable and appropriate to the floating point math definitions we're operating in right now"
- WJW 6y ago
  What would be the dependent type you could use to prevent the bug in the given example though? There is nothing wrong with the function itself, there is just a discrepancy between what it does and how it is named. I don't know of any constraint that would fix that. In any case, the more code you put into the type system the higher the chance that your dependent type specification haS a bug in it.
  - AnthonBerg 6y ago
    In dependent types, types depend on values. Here, the type depends on the value that is the function name :) As far as I know, this is literally actually possible in Idris, right now. Wrote a bit more earlier: https://news.ycombinator.com/item?id=24716477 https://news.ycombinator.com/item?id=24716477 > the more code you put into the type system the higher the chance that your dependent type specification haS a bug in it. Unbounded infinity has infinite, uncountable bugs. A defined, bounded, well-constructed, proven type system has fewer bugs. Dependent types are not an axis of explosion, but rather a way to express useful bounds on multiple axes.
    - WJW 6y ago
      Reading your other comment, I'll concede that it's not impossible to encode these things into the type system. I don't think it will scale beyond toy examples (at least until AGI is a thing). There are plenty of function names that represent highly specific business processes (and jargon) and I don't see how any type system will have enough context for that. Less bugs does sound good, but after a minute thought there still seem to be uncountably infinite bugs even in the presence of dependent types. Just a few less than without. :)
      - AnthonBerg 6y ago
        We have a lllooootttt of work ahead of us! heh! (But yes: It's a good place to hook the AGI up!)
drdeca 6y ago
because it isn't a type error? Obviously if the spec says to create a word processor program, and you instead write a flight simulator, the compiler isn't going to correct that mistake.
- synthc 6y ago
  that is exactly my point, static type system help a lot, but saying that 'if the types check there are no bugs' is too much. There are many classes of errors that are beyond types, even dependant types.
ben509 6y ago
> Not all functional languages have static typing. Even the multi-paradigm, late-bound languages that are adding functional programming are adding static typing, e.g. TypeScript and mypy. > No type checker will catch this error... Sure, math is hard. In the domain of structural transformations, one's intuition combined with a decent type checker really does work, though. Especially, I've done large refactorings of complex transformations, tracked down the typing errors, and then been pleasantly surprised when my test-suites passed the first time. > sqrt :: double -> double I can use QuickCheck[1]: prop_Sqrt_Sqr n = sqrt n * sqrt n == abs n Because it can exploit the type system, it can then plug in various values of Double to see if squaring my square root squares properly. [1]: http://www.cse.chalmers.se/~rjmh/QuickCheck/manual.html http://www.cse.chalmers.se/~rjmh/QuickCheck/manual.html

by synthc 6y ago

AnthonBerg 6y ago

Dependent types are able to express the constraints that prevent or catch this error. The types of the arguments to the function can have value constraints on it, and those constraints can be determined from a value that exists there: the name of the function.

AlotOfReading 6y ago
Not only do dependent types have huge decidability issues, it's my understanding that integrating them with side effects is still an area of active research.
- AnthonBerg 6y ago
  I think fortunately those are orthogonal matters :) First, I don't know that dependent types have huge decidability issues that are an inherent obstacle in general; Idris for one has a very practical and elegant model of computation – things like totality checking, linearity rules and elimination of "scaffolding" types do a lot for us. Dependent types do allow telling the compiler about more dimensions to consider – in a way that allows for a computational explosion at compile time – but those were always an available to consider as part of the computation; Dependent types dont add that complexity, rather they allow us to address it in the type system. I see it such that we're in a stronger position to manage and navigate that complexity by allowing us to express it to the compiler in a succinct and clear way near the core context of desired action. Dependent types allow us to do less by allowing us to do more. And integrating purely functional mechanisms with side effects is a fun and interesting avenue of research, and I don't know that adding dependent types makes that more difficult; I'd think it makes it easier?
  - AnthonBerg 6y ago
    To continue the thought: This dependent type is expressible, trivially decidable, and has no additional side effect burden: "This function's type depends on its function name. If its function name is "sqrt", then {check some simple rules about square roots, like if x is 0 then output is 0, if x > 1 then output < x, etc.}" This one too: "This function's type depends on its function name. If its function name is "sqrt", then check that it calls and returns a formally verified square root function applicable to its input type that is known to be decidable and appropriate to the floating point math definitions we're operating in right now"
WJW 6y ago
What would be the dependent type you could use to prevent the bug in the given example though? There is nothing wrong with the function itself, there is just a discrepancy between what it does and how it is named. I don't know of any constraint that would fix that. In any case, the more code you put into the type system the higher the chance that your dependent type specification haS a bug in it.
- AnthonBerg 6y ago
  In dependent types, types depend on values. Here, the type depends on the value that is the function name :) As far as I know, this is literally actually possible in Idris, right now. Wrote a bit more earlier: https://news.ycombinator.com/item?id=24716477 https://news.ycombinator.com/item?id=24716477 > the more code you put into the type system the higher the chance that your dependent type specification haS a bug in it. Unbounded infinity has infinite, uncountable bugs. A defined, bounded, well-constructed, proven type system has fewer bugs. Dependent types are not an axis of explosion, but rather a way to express useful bounds on multiple axes.
  - WJW 6y ago
    Reading your other comment, I'll concede that it's not impossible to encode these things into the type system. I don't think it will scale beyond toy examples (at least until AGI is a thing). There are plenty of function names that represent highly specific business processes (and jargon) and I don't see how any type system will have enough context for that. Less bugs does sound good, but after a minute thought there still seem to be uncountably infinite bugs even in the presence of dependent types. Just a few less than without. :)
    - AnthonBerg 6y ago
      We have a lllooootttt of work ahead of us! heh! (But yes: It's a good place to hook the AGI up!)

drdeca 6y ago

because it isn't a type error? Obviously if the spec says to create a word processor program, and you instead write a flight simulator, the compiler isn't going to correct that mistake.

synthc 6y ago
that is exactly my point, static type system help a lot, but saying that 'if the types check there are no bugs' is too much. There are many classes of errors that are beyond types, even dependant types.

ben509 6y ago

> Not all functional languages have static typing. Even the multi-paradigm, late-bound languages that are adding functional programming are adding static typing, e.g. TypeScript and mypy. > No type checker will catch this error... Sure, math is hard. In the domain of structural transformations, one's intuition combined with a decent type checker really does work, though. Especially, I've done large refactorings of complex transformations, tracked down the typing errors, and then been pleasantly surprised when my test-suites passed the first time. > sqrt :: double -> double I can use QuickCheck[1]: prop_Sqrt_Sqr n = sqrt n * sqrt n == abs n Because it can exploit the type system, it can then plug in various values of Double to see if squaring my square root squares properly. [1]: http://www.cse.chalmers.se/~rjmh/QuickCheck/manual.html http://www.cse.chalmers.se/~rjmh/QuickCheck/manual.html