Use with Diminsional and an question

[Michael Thomas]

Thanks for accepting my request to join this group. I am currently working on a chemistry library as a side project (https://github.com/Michaelt293/isotope). It has been suggested that I should think about adding units with dimensional (https://hackage.haskell.org/package/units). I was wondering, will I run into problems if I try to use this library together with Liquid Haskell?

Finally, I have started adding liquid haskell annotations to types and have setup liquid haskell for use with stack (following the instructions in https://github.com/Gabriel439/slides/blob/master/liquidhaskell/slides.md). Below, I want to restrict AtomicNumber (a type alias of Int) in Element to accept only positive Int's. This however results in an error. It might be something stupid that I am doing but any help would be much appreciated.

{-@ type Pos = { n : Int | 0 < n } @-}

{-@
data Element = Element { atomicNumber' :: Pos
                       , elementName'  :: ElementName
                       , isotope'       :: Isotope
                       }
@-}
data Element = Element { atomicNumber' :: AtomicNumber
                       , elementName'  :: ElementName
                       , isotopes'     :: [Isotope]
                       } deriving (Show, Eq, Ord)

This gives the following error-

 src/Isotope/Base.hs:163:14: Error: Cannot parse specification:
 
 163 | data Element = Element { atomicNumber' :: Pos
                   
 
     unexpected "="
     expecting white space, "[" or "@-}"

[Ranjit Jhala]

​Hi Mi​chael -- 

(Apologies for the delay with the mailing list!)

Thanks for pointing this out! 

This looks like a terrible bug in the LH parser: 

it doesn't like field names with `'`, if you 

remove those it seems fine.

  http://goto.ucsd.edu:8090/index.html#?demo=permalink%2F1464279061_12094.hs

Sorry about that! (We're in the process of redoing the parser so this will

hopefully be a relic of the past!)

We haven't tried using LH with dimensional -- but I don't foresee any particular

problems. If you run into any please let us know!

Thanks!

- Ranjit.

--
You received this message because you are subscribed to the Google Groups "liquidhaskell" group.
To unsubscribe from this group and stop receiving emails from it, send an email to liquidhaskel...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.