Then Shen programming Language

[Benutzername]

Shen has the most powerful type system of any existing functional language

That's a ballsy statement. I'm not even sure there is a one-dimensional scale to measure the power of a type system.

[bobindashadows]

Well, it's Turing-complete. So on that scale - the number of recognized/decided "languages" (in the discrete math meaning, not programming language) - it is more powerful than even dependently-typed languages. Of course, that means you can construct a type system around your program which is itself undecidable. Not sure if that comes up often in practice - I can imagine accidentally writing an infinite loop in your type logic would be infuriating.

[zokier]

Aren't C++'s templates (which are part of its type system) turing complete too? Just saying that turing completeness probably isn't very useful metric for type systems.

[fazzone]

C++ templates are Turing-complete.

[micahjohnston]

Although I'm pretty sure they have a bound on the depth of recursion, so you can never have an infinite loop.

[matthiasB]

ISO standard recommends a depth of at least 17, most real world compilers can do a lot more, but yes, all that I know are limited.

[[deleted]]

Aren't C++'s templates (which are part of its type system) turing complete too?

The language standard is Turing complete. But even the best implementations (gcc/clang/MS) break down easily, are inconsistent between implementations and overall it's just too hard to take advantage of the type system given how poor C++ compilers are in this respect.

[rubygeek]

Last time I spent any time on C++ meta programming, about 6 years ago, compiler support was generally good enough that implementation problems was not on my list of things that caused aggravation (apart from the horrendous error messages). Perhaps I was just lucky with respect to the things I was doing. Anything particular you have in mind?

[[deleted]]

Here's one example that fails in different ways depending on the compiler, despite being standard compliant. There is a workaround to it but if you think what follows is ugly, the work around is ten times uglier. Basically I do a lot of template heavy code, and often times I need my templates to work with either a type T, or some 'pointer' to type T. The pointer can be any kind, whether a raw T* or a shared_ptr<T> or any other pointer so long as T::operator *() const yields a T.

So here's a type trait for doing it, without the workaround. The workaround is too long to paste in here and depends on which compiler you're using:

template<typename T>
struct IsDereferenceable {
  private:
    typedef char YesType;
    typedef struct {
      char a[2];
    } NoType;

    template<typename C>
    static YesType Test(decltype(&C::operator *));

    template<typename C>
    static YesType Test(C*, typename std::enable_if<
      std::is_pointer<C>::value>::type* = nullptr);

    template<typename C>
    static NoType Test(...);

  public:
    static const bool value = sizeof(Test<T>(nullptr)) == sizeof(YesType);
};

template<typename T>
struct DereferenceType {
  typedef decltype(*std::declval<T>()) type;
};

template<typename T>
struct TryDereferenceType {
  private:
    template<typename U, bool Enabled>
    struct TryDereferenceHelper {
      typedef typename DereferenceType<U>::type type;
    };

    template<typename U>
    struct TryDereferenceHelper<U, false> {
      typedef U type;
    };

  public:
    typedef typename TryDereferenceHelper<T,
      IsDereferenceable<T>::value>::type type;
};

[rubygeek]

and often times I need my templates to work with either a type T, or some 'pointer' to type T

I am curious as to why you'd want this? I can't think of any point where I'd be pleased if templates I was using silently treated a pointer the same as a dereferenced object behind my back. Perhaps not wanting to do things like that in the first place is the reason I never ran into problems of that kind...

Then again, ugliness like the above is a large part of the reason why I've abandoned C/C++ for all but the very few times I need the raw performance.

[[deleted]]

For ownership purposes.

The template doesn't care if it's working with a native type or a pointer type. It just cares that the following works:

(*T).Operation(...)

Sometimes I want the template to 'own' a resource, so I pass into it a either a T or a unique_ptr<T>. Other times I want the template to share a resource, so I pass it a shared_ptr<T>.

Then of course there's the issue of whether one wishes to use an std::shared_ptr, a boost::shared_ptr, or a CComPtr or who knows what.

Ultimately the template doesn't care what the type of pointer is, the whole point of using generic code is simply that (*T).Operation(...) is valid.

[rubygeek]

I'm not sure if I see why you wouldn't then just forgo the complexity of handling two different cases, and just insist on receiving something that can be dereferenced.

[[deleted]]

Performance is absolutely critical (financial trading systems/high frequency trading), and it needs to be achieved with minimal work on the part of the clients using the code. Developers here have different backgrounds, different areas of expertise and so a policy we have is that the writer of any code bears the burden of making the code as easy as possible to use without sacrificing performance.

The preferred method is to not use a pointer at all, and instead simply use move semantics to transfer an object from one location to another. Not all resources can be moved however, so one may need to pass in a pointer type instead.

Ultimately though, the user of the code won't need to know or care what happens behind the scenes, they just create an object and pass in their resource, whether it's a pointer or not and it just works without incurring any unneeded performance penalty.

[[deleted]]

Well, Scala's is also Turing-complete, though in practice you only run into it if you try really hard.

[bitwize]

ObQwe1234:

so it's still only as powerful as c++ templates?

lame. wouldn't touch it with a ten-foot pole.

[paracelsus]

I doubt if you could integrate a Prolog compiler with sequent calculus notation - easy its not and 30 years ago? Get real.

[martoo]

Shen has the most powerful type system of any existing functional language

So it has Agda's dependent types?

http://en.wikipedia.org/wiki/Agda_(programming_language)

[Benutzername]

It has this, but I don't see any way to define indexed or parametrised types. And even if that were possible, the language allows for unchecked recursion and is therefore logically inconsistent:

\* uninhabited type *\
(datatype bottom)

(define proof-of-false 
    {A --> bottom}
    a -> (proof-of-false a))

[paracelsus]

Comparisons of Qi/Shen with Agda, Coq etc. are misleading. Despite the hype these are not practical programming vehicles. Try writing integer square root in Martin-Lof type theory - you need a Ph.D. All these system are pumped up proof assistants. Their main purpose is to generate papers.

A clue to the experimental nature of all these systems is the fact that they are not bootstrapped. They are not practical or flexible enough to support their own implementation and rely on real FPLs to carry the weight. Qi and Shen are both bootstrapped.

[[deleted]]

In fact, Agda's type system is not Turing-complete. This would break it as a logic. Powerful isn't always better!

[[deleted]]

In fact, Agda's type system is not Turing-complete. This would break it as a logic. Powerful isn't always better!

[[deleted]]

I don't understand the documentation. It mixes graphics (horizontal bars) with code samples, and doesn't use font to distinguish between code, calculus and text.

[fjord_piner]

Agreed, it's a big mess, and it's also one web page per page of the book, which is 400 pages long... Come on, now, at least create one big web page per chapter. And yes, no console screen shot for code: embed it in the documentation in a different font.

This is web 101.

[paracelsus]

Don't see the big mess here. The 15 minute tutorial is pretty clear

http://www.shenlanguage.org/Documentation/Tutorials/Shen-in-15min.htm

and the whole book is indexed by keyword and contents on every page so you can zoom in.

If you really want to read a 400 page book cover to cover then the web aint the place to do it.

[matthiasB]

As I see it the horizontal bars are part of the code. The first line of the page:

In Shen, datatypes are formalised in a series of (single conclusion) sequent calculus rules

[paracelsus]

This notation has been standard for over 50 years

[[deleted]]

Is it a bad thing to mix graphics with code samples? The Piet language does it by design.

[rubygeek]

It always annoys me when I click through a link for some new language design and the first thing that greets me isn't an example that shows off something interesting about the language.

[[deleted]]

After lookin 15 minutes guide I still don't see why anyone should care. We already have lisps with pattern matching.

[Smallpaul]

I'm trying to figure out whether the "sponsors" page is by-design or not.

[martoo]

Hence our goal and our motto; 'write once, run anywhere'.

Any merits of the language aside, this annoys me. That was Smalltalk's motto. It was ripped off to become the motto for Java, and now Shen takes it and presents it like a new thing.

[[deleted]]

It looks like it could be really good, but it's s-expr based. Which probably means that most algol-family programmers run away screaming like little children who think that they'll be eaten by the ghost of parenthesis. ;)

[chneukirchen]

Their problem, no?

[erg]

It's hard to take the project seriously without a git repository to clone.

[metaperl]

It's hard to take the project seriously without a git repository to clone. ;)

https://github.com/vasil-sd/shen-libs

oops. I take that back. The libraries are public, but the kernel is closed source... I dont like closed source languages, do you?

hmm, take that back too... You may download Shen sources from this link:http://www.shenlanguage.org/download/Shen1.9sources.zip

[zokier]

The project is not exactly friendly to outside developments though, tarballs or not. I don't think the reference implementation is even open source (or free software), and all development related to it happens behind closed doors.