The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

Well, maybe.  This is one of those gross "look, my complicated type 
system accidentally contains feature X," whereas I'd be more interested 
in examples that have been designed to do lambda-cube-style stuff elegantly.

Thanks for the pointer to that blog post!

On 03/25/2014 12:06 PM, J. Ian Johnson wrote:
> Scala fits this bill, no? The shapeless library is a common tool in the 
> toolbelt, which does lots of type level computation. I can't say which 
> commercial entities are serious users of it off hand, however.
> This might be a question for Twitter, since there are a bunch of Scala 
> hackers there.
>
> Also see the actual simply typed lambda calculus in Scala's type system here 
> https://apocalisp.wordpress.com/2009/09/02/more-scala-typehackery/
> -Ian
> ----- Original Message -----
> From: "Adam 
> Chlipala"<adamc AT csail.mit.edu>
> To: 
> "coq-club"<coq-club AT inria.fr>
> Sent: Tuesday, March 25, 2014 11:21:45 AM GMT -05:00 US/Canada Eastern
> Subject: [Coq-Club] Commercial applications of dependent type theory?
>
> Does anyone have any pointers to lists of commercial systems that use
> dependent type theory?  I mean "type theory" in a fairly loose sense,
> but the core characteristic I'm interested in is a complete copy of
> simply typed lambda calculus, or something fancier, embedded in a static
> type language.  I think GHC Haskell doesn't qualify, because they don't
> really seem to have type-level lambdas that can be computed with in the
> usual way, to support predictable enough type inference.
>
> Thanks!
>