Welcome to Omgili,
Omgili ( Oh My God I Love It ;) is a search engine for discussions. With Omgili you can find answers and solutions, debates, discussions, personal experiences, opinions and more... To learn more about Omgili click here.
This is a complete preview of the discussion as it was indexed by Omgili crawlers. Use this preview if the original discussion is unavailable.
Click here to view the original discussion.
 |
|
 |
|
Total Functional Programming [PDF] : programming
A place for all things programming.
Before making a self-post in /r/programming, please check the programming.reddit FAQ to see if it's there first
We're toying with the idea of blocking this reddit from advertisers and replacing the 300x250 ad unit with our redditjobs widget so you'll see new jobs instead of advertisements.
Check out our jobs board .
|
|
 |
|
 |
|
|
|
|
Page 1:
fib :: Nat->Nat
fib 0 = 0
fib 1 = 1
fib (n+2) = fib (n+1) + fib (n+2)
the last line doesn't seem too right.
|
|
|
|
|
|
|
|
|
Fortunately functional programming languages spot these errors, ..., or do they?
|
|
|
|
|
|
|
|
|
Total languages do: They readily detect that (n+2) isn't structurally smaller than (n+2) and tell you either that you've written an infinite loop, or ask you to prove that you haven't, or similar.
Haskell wouldn't detect that, but then its type checker is guaranteed to terminate...
At least by default, without any of the more esoteric language extensions.
|
|
|
|
|
|
|
|
|
Is that how Charity ensures termination?
Or is it different entirely?
|
|
|
|
|
|
|
|
|
Erm... I got some things messed up there:
The requirement of totality (including no bottom introduced by stuff that can't be reduced to normal form) arises from the fact that you want your type checker to terminate, and the reason it's failing to terminate, in the first place, is dependent typing: If you want to write functions like
head :: List (Succ n) a ->
A tail :: List (Succ n) a ->
List n a cons :: a ->
List n a -> List (Succ n a) append :: List n a ->
List m a -> List (Add m n) a
, you need a near-turing complete type system, allowing recursion and everything.
The benefit is that you have static guarantees never to call head or tail on an empty list.
The whole notion of total languages, read semantics as close to turing-complete as possible, but strongly normalising, is quite new and still under heavy research.
|
|
|
|
|
|
|
|
|
Can you provide any links to work on total languages?
I'm interested on learning more.
|
|
|
|
|
|
|
|
|
The main keyword to look for, regarding theoretical basics, is Curry-Howard isomorphism / Type theory;
The most recent calculus I know of is described in http://www.cs.nott.ac.uk/~txa/publ/pisigma.pdf .
If you are content with just a taste of dependent typing, but don't want to end up proving everything, you can try Haskell's functional dependencies.
Dependent languages aren't really much fun yet, as automatic theorem proving isn't yet as powerful as it's going to be, or should be: The obligation to prove termination can quickly become quite burdensome.
|
|
|
|
|
|
|
|
|
Agda is a total language that You Can Use Now .
|
|
|
|
|
|
|
|
|
Quite new? You mean hasn't been around more 30 years or so?
|
|
|
|
|
|
|
|
|
Much newer than lambda-calculus and turing equivalence, constructivism, or type theory, yes.
Not newer than Haskell, but new enough to be only partly included in extensions.
In other words, it's still not well-understood, even if some guy happened to write a paper about it ages ago.
|
|
|
|
|
|
|
|
|
Are there any real world (e.g.
With IO in some form) total languages?
|
|
|
|
|
|
|
|
|
Http://wiki.portal.chalmers.se/agda/
...honestly, I don't know anything about the run-time systems of other total languages, but agda has a full ffi to Haskell, so you get anything you can do with ghc, which is everything.
In fact, agda is just compiled down to Haskell, literally every expression wrapped in unsafeCoerce to pass Haskell's type checker.
|
|
|
|
|
|
|
|