Hacker News

NaeosPsy•6y

Dimensions and Haskell: Singletons in Action serokell.io

7 comments

harpocrates•6y
Safety in the form of tightly-fitting types is great, but the signatures definitely suffer a bit in readability (otherwise, Haskell signatures are generally quite helpful when deciphering a functions purpose). I understand why it needs to be this way, but this signature is nasty looking:
```
    makePCATypeSafe
      :: forall d x y. (AllConstrained SingI '[d,x,y], d <= x ~ 'True)
      => Proxy (d :: Nat) -> DimMatrix D y x Double -> TypeSafePCA
```
In (pseudo code), dependent types would really help out a lot:
```
    makePCATypeSafe
      :: forall (d :: Natural) (x :: Natural) (y :: Natural). d <= x
      => Proxy d -> DimMatrix D y x Double -> TypeSafePCA
```
It sometimes feels like GHC is a kitchen sink for type-level extensions. I wish the bar for entry for new extensions of this sort was higher and the language a bit more cohesive.
- logicchains•6y
  There is a plan to add proper dependent types to GHC: https://gitlab.haskell.org/ghc/ghc/wikis/dependent-haskell. No exact timeline on when it will be ready though.
shoo•6y
"singletons" in this context is apparently some mechanism applied here to type-check matrix dimensions... :
> we put dimensions of data types on the type level to avoid a large set of errors that might arise at the runtime stage. During the compile stage, one may check some properties of matrix dimensions expressed via type-level natural numbers and find out the reason of that error as a type error.
> In this part, we describe our approach to the matrix data type that is parameterised via its numbers of columns and rows
> In this approach, matrix dimensions are lifted to the type level with the use of the Singletons library. At first glance, our solution looks a bit sophisticated. Why? There remains a question about the way to make it less devious and more idiomatic. In other words, we have to recognise the restrictions of Haskell expressive opportunities. What about performance? Also, our approach helps to remove only errors that affect the dimensions of arrays. Can we track other array parameters to reduce a set of possible runtime errors even more?
... not the horrible "singleton" design pattern https://en.wikipedia.org/wiki/Singleton_pattern
Prior art for identifying errors due to mismatched array dimensions include:
* (Eigen, C++) support for compile-time static assertions in some situations: https://eigen.tuxfamily.org/dox/TopicAssertions.html
* (numpy, python) raising ValueErrors at runtime about shape misalignment
- NaeosPsy•6y
  http://hackage.haskell.org/package/singletons
  Singletons is a Haskell library. In this context, it is used to emulate dependent types which Haskell does not yet have.
- thesz•6y
  I have to say that Eigen would have hard time being prior art: http://okmij.org/ftp/Haskell/number-parameterized-types.html
  It's from 2007 and I think it is older than Eigen.
kccqzy•6y
Singletons are one of the ugliest things in Haskell. They require lots of extensions, implemented in a complicated way, and leaks implementation detail. Which makes debugging compile-time errors using them quite hard. I'd rather debug a runtime error with proper HasCallstack constraints.
- Haskell-mouse•6y
  Hi! I am one the author of this post. I agree that Singletons are ugly. But:
  1) Without them, creating a bridge between types and values became a real hell. 2) HasCallstack just gives you a place of an exception. It does not give you a cause. And part of errors even does not lead to exceptions at all.
  Just want to say, that idea described in the post arose only after hard debugging. And using singletons was much easies and more reliable. And we tried to explain and analyse our personal experience.