3 ms·

Dimensions and Haskell: Singletons in Action

46 points by NaeosPsy 7y ago

kccqzy 7y ago
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 7y ago
  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.
shoo 7y ago
"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 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 https://eigen.tuxfamily.org/dox/TopicAssertions.html * (numpy, python) raising ValueErrors at runtime about shape misalignment
- NaeosPsy 7y ago
  http://hackage.haskell.org/package/singletons 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 7y ago
  I have to say that Eigen would have hard time being prior art: http://okmij.org/ftp/Haskell/number-parameterized-types.html http://okmij.org/ftp/Haskell/number-parameterized-types.html It's from 2007 and I think it is older than Eigen.
harpocrates 7y ago
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 7y ago
  There is a plan to add proper dependent types to GHC: https://gitlab.haskell.org/ghc/ghc/wikis/dependent-haskell https://gitlab.haskell.org/ghc/ghc/wikis/dependent-haskell. No exact timeline on when it will be ready though.

46 points by NaeosPsy 7y ago

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 7y ago
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.

shoo 7y ago

"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 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 https://eigen.tuxfamily.org/dox/TopicAssertions.html * (numpy, python) raising ValueErrors at runtime about shape misalignment

NaeosPsy 7y ago
http://hackage.haskell.org/package/singletons 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 7y ago
I have to say that Eigen would have hard time being prior art: http://okmij.org/ftp/Haskell/number-parameterized-types.html http://okmij.org/ftp/Haskell/number-parameterized-types.html It's from 2007 and I think it is older than Eigen.

harpocrates 7y ago

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 7y ago
There is a plan to add proper dependent types to GHC: https://gitlab.haskell.org/ghc/ghc/wikis/dependent-haskell https://gitlab.haskell.org/ghc/ghc/wikis/dependent-haskell. No exact timeline on when it will be ready though.