3 ms·

Isn't this handled by 'purity' of functions? It seems like the big idea here is that Int->Int always, no errors, faults, 'impact by extra data'. Isn't that al

Isn't this handled by 'purity' of functions? It seems like the big idea here is that Int->Int always, no errors, faults, 'impact by extra data'. Isn't that all also solved by pure functions? And is incorporated into functional languages at this point?

gpderetta 3y ago
the big Idea is that the language is non-Turing complete and termination can be proven (and co-data is used for non-terminating programs).
- zarathustreal 3y ago
  I’ve had an idea for a language like this for a while now that wouldn’t exactly “type check” in the sense that the unification finishes but that the “type checking” would be continuously running in the background as you’re programming. This co-data approach seems interesting toward that goal
  - anon291 3y ago
    Isn't this just Idris, Haskell, Agda, etc with LSP integration? IIRC, Agda has always had excellent editor integration, and Idris too.
    - zarathustreal 3y ago
      I’m not too familiar with any of those languages but I’m guessing the difference is that type checking does eventually “finish” in those languages and that to accomplish this, the type systems are necessarily not Turing-complete, whereas I’m suggesting the alternative. Type checking in my idea would actually produce artifacts that you’d store with your code essentially saving the state of type checking up to whatever bounds had been reached since the last code change. Kind of like a combination of type checking and unit testing that takes advantage of pure functional programming
      - anon291 3y ago
        Agda and Idris have undecidable type systems (in certain circumstances). But otherwise, if you're using the 'safe' versions of those languages, then I believe the language itself is not Turing complete. Regardless, Haskell has turing complete type evaluation (if you turn on UndecidableInstances) and thus potentially non-terminating compilation. > Type checking in my idea would actually produce artifacts that you’d store with your code essentially saving the state of type checking up to whatever bounds had been reached since the last code change. The incrementality would be new.
      - zozbot234 3y ago
        But "type checking" that's Turing complete is not type checking at all, it's just a phase distinction. It's no different than choosing whether to run code at "compile" vs. "run" time, except that in practice, we don't even want to have fully Turing-complete compile workflows that might, e.g. not terminate. Dependently typed languages implement this phase distinction via program extraction: you "extract" the code to be fed into the "runtime" phase of execution.
tromp 3y ago
No; purity is an orthogonal notion. Haskell functions are pure in that given the same arguments, a function always produces the same output. But Haskell functions can be partial; for some arguments there is no output, or the output is undefined. Turner proposes a language for pure total functions.
anon291 3y ago
> It seems like the big idea here is that Int->Int always, no errors, faults, 'impact by extra data'. Well no. This is computer science 101. Anything that can compute anything useful (ie. Turing complete or lambda-calculus-complete... they're equivalent) cannot be said to produce an answer in finite time (or at all really). In FP parlance, we say that such functions are a 'bottom' value. The notation 'Int -> Int' in a language like haskell is a function that takes an Int and returns an Int, if it terminates. In a total language, you're guaranteed to have an Int after invoking the function within a finite amount of time, even if that time is greater than the age of the universe. But it will eventually return an answer. Whereas a haskell program may truly never terminate. Here is an example of a haskell program that is syntactically correct and well-typed but is actually a bottom, despite the type signature claiming in returns Int f :: Int -> Int f x = f x
- FrustratedMonky 3y ago
  Guess, that is what I was asking. If you take any current functional language, and add the criteria that it must only use pure functions, then Int->Int is the same as described in the Total Language. Because if there are no outside interactions inside the function, it's 'pure', then the Int->Int is guaranteed. Doesn't using only pure functions, equate to this Total Functions.
  - deleted 3y ago
    [deleted]
  - FrustratedMonky 3y ago
    This might be one of those 'sloppy' definitions. From random search, seems like some people assume this : Pure=Total "A pure function must be total Firstly, a function must be total, this means that for each input that is provided to the function there must be a defined output."
  - anon291 3y ago
    > If you take any current functional language, and add the criteria that it must only use pure functions, then Int->Int is the same as described in the Total Language. The function above is pure. In fact, all functions in Haskell are, even those returning IO.
lynx23 3y ago
No. Haskell has this notion of what they call "bottom", more easily remembered as what happens if you call undefined. The issue is, your function can be as pure as it wants, as long as you are able to write "f :: T -> T; f = undefined" all your purity based analysis goes to hell.
- FrustratedMonky 3y ago
  Think original question I had, was if you make "f = undefined" be Pure. Don't leave undefined. It has a defined signature Int->Int. Then "f" should return Int every time guaranteed, and would be equivalent of the Total Functional case.
  - lynx23 3y ago
    Even if undefined were not allowed, you'd still be able to write "f :: Int -> Int; f x = f x" which would never return an Int. Totality is about getting a grip on these cases. As mentioned more elquently then I could in this thread, it has been proven long time ago that termination-analysis is impossible to achieve. What Idris for instance does is to use proofs, adn to an extend heuristcs, to stil decide in special cases that a function is total, IOW terminates. Thats a pretty cool part of CS, since we're basically knowing something is impossible but still make small steps towards tackling the issue at least for some cases we care about.
- justincredible 3y ago
  [dead]

gpderetta 3y ago

the big Idea is that the language is non-Turing complete and termination can be proven (and co-data is used for non-terminating programs).

zarathustreal 3y ago
I’ve had an idea for a language like this for a while now that wouldn’t exactly “type check” in the sense that the unification finishes but that the “type checking” would be continuously running in the background as you’re programming. This co-data approach seems interesting toward that goal
- anon291 3y ago
  Isn't this just Idris, Haskell, Agda, etc with LSP integration? IIRC, Agda has always had excellent editor integration, and Idris too.
  - zarathustreal 3y ago
    I’m not too familiar with any of those languages but I’m guessing the difference is that type checking does eventually “finish” in those languages and that to accomplish this, the type systems are necessarily not Turing-complete, whereas I’m suggesting the alternative. Type checking in my idea would actually produce artifacts that you’d store with your code essentially saving the state of type checking up to whatever bounds had been reached since the last code change. Kind of like a combination of type checking and unit testing that takes advantage of pure functional programming
    - anon291 3y ago
      Agda and Idris have undecidable type systems (in certain circumstances). But otherwise, if you're using the 'safe' versions of those languages, then I believe the language itself is not Turing complete. Regardless, Haskell has turing complete type evaluation (if you turn on UndecidableInstances) and thus potentially non-terminating compilation. > Type checking in my idea would actually produce artifacts that you’d store with your code essentially saving the state of type checking up to whatever bounds had been reached since the last code change. The incrementality would be new.
    - zozbot234 3y ago
      But "type checking" that's Turing complete is not type checking at all, it's just a phase distinction. It's no different than choosing whether to run code at "compile" vs. "run" time, except that in practice, we don't even want to have fully Turing-complete compile workflows that might, e.g. not terminate. Dependently typed languages implement this phase distinction via program extraction: you "extract" the code to be fed into the "runtime" phase of execution.

tromp 3y ago

No; purity is an orthogonal notion. Haskell functions are pure in that given the same arguments, a function always produces the same output. But Haskell functions can be partial; for some arguments there is no output, or the output is undefined. Turner proposes a language for pure total functions.

anon291 3y ago

> It seems like the big idea here is that Int->Int always, no errors, faults, 'impact by extra data'. Well no. This is computer science 101. Anything that can compute anything useful (ie. Turing complete or lambda-calculus-complete... they're equivalent) cannot be said to produce an answer in finite time (or at all really). In FP parlance, we say that such functions are a 'bottom' value. The notation 'Int -> Int' in a language like haskell is a function that takes an Int and returns an Int, if it terminates. In a total language, you're guaranteed to have an Int after invoking the function within a finite amount of time, even if that time is greater than the age of the universe. But it will eventually return an answer. Whereas a haskell program may truly never terminate. Here is an example of a haskell program that is syntactically correct and well-typed but is actually a bottom, despite the type signature claiming in returns Int f :: Int -> Int f x = f x

FrustratedMonky 3y ago
Guess, that is what I was asking. If you take any current functional language, and add the criteria that it must only use pure functions, then Int->Int is the same as described in the Total Language. Because if there are no outside interactions inside the function, it's 'pure', then the Int->Int is guaranteed. Doesn't using only pure functions, equate to this Total Functions.
- deleted 3y ago
  [deleted]
- FrustratedMonky 3y ago
  This might be one of those 'sloppy' definitions. From random search, seems like some people assume this : Pure=Total "A pure function must be total Firstly, a function must be total, this means that for each input that is provided to the function there must be a defined output."
- anon291 3y ago
  > If you take any current functional language, and add the criteria that it must only use pure functions, then Int->Int is the same as described in the Total Language. The function above is pure. In fact, all functions in Haskell are, even those returning IO.

lynx23 3y ago

No. Haskell has this notion of what they call "bottom", more easily remembered as what happens if you call undefined. The issue is, your function can be as pure as it wants, as long as you are able to write "f :: T -> T; f = undefined" all your purity based analysis goes to hell.

FrustratedMonky 3y ago
Think original question I had, was if you make "f = undefined" be Pure. Don't leave undefined. It has a defined signature Int->Int. Then "f" should return Int every time guaranteed, and would be equivalent of the Total Functional case.
- lynx23 3y ago
  Even if undefined were not allowed, you'd still be able to write "f :: Int -> Int; f x = f x" which would never return an Int. Totality is about getting a grip on these cases. As mentioned more elquently then I could in this thread, it has been proven long time ago that termination-analysis is impossible to achieve. What Idris for instance does is to use proofs, adn to an extend heuristcs, to stil decide in special cases that a function is total, IOW terminates. Thats a pretty cool part of CS, since we're basically knowing something is impossible but still make small steps towards tackling the issue at least for some cases we care about.
justincredible 3y ago
[dead]