haskell - LiquidHaskell: Trying to use assume keyword, but data type is not numeric -


i'm trying write specifications data.ratio module. far have:

module spec data.ratio  import ghc.real  data.ratio.denominator :: ghc.real.integral => r : ghc.real.ratio -> {x:a | x > 0}

the code i'm verifying is:

{-@ die :: {v:string | false} -> @-} die msg = error msg  main :: io () main =   let x = 3 % 5   print $ denominator x   if denominator x < 0     die "bad ending"     else putstrln "good ending"

the code judged safe, because denominator never returns negative value.

i found strange because have written x <= 0 postcondition, according documentation of data.ratio module impossible. apparently liquid haskell not compare postcondition implementation of denominator.

my understanding since function implementation not checked, i'm better off using assume keyword:

assume data.ratio.denominator :: ghc.real.integral => r : ghc.real.ratio -> {x:a | x > 0}

however, get:

 error: bad type specification  assumed type ghc.real.denominator :: (ratio a) -> {vv : | vv > 0}      sort error in refinement: {vv : a_a2kc | vv > 0}      unbound symbol a_a2kc  perhaps meant: papp5, papp3, papp4, head, papp2, papp7, papp6, papp1, tail   because sort a_a2kc not numeric

my questions are

  1. shouldn't lh force me use assume keyword in case if didn't verify correctness of refined type comparing function implementation?
  2. am right in thinking should use assume keyword?
  3. how come a not numeric? wasn't numeric when didn't use assume?

unfortunately 'numeric' literally means 'num' , not subclasses thereof. need extend lh support sub-classes in form describe above; create issue it, pointing out!

now, if specialize type to, e.g. int or integer lh throws error:

import ghc.real  {-@ assume denom :: r:ghc.real.ratio int -> {x:int | x >= 0} @-} denom :: ghc.real.ratio int -> int  denom = denominator  {-@ die :: {v:string | false} -> @-} die msg = error msg  main :: io () main =   let x = 3 % 5   print $ denom x   if denom x <= 0     die "bad ending"     else putstrln "good ending"

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

if make output type x > 0 safe again.

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

thanks again pointing out ratio issue!


Comments

Post a Comment

Popular posts from this blog

python - Best design pattern for collection of objects -

i have following architecture: +-----------------+ | collection | | | | | | | | | +-----------------+ | ^ | | create() | | | | v | getitem(b) +------------+ | | item | | | | | | +------+ | | +------------+ a class managing collection of items, creates items. , these items may need other items collection. the actual code in python, , collection passes parameter created item . see it, bad practice. improvement can see pass few functions of collection needed item , instead of whole instance. for example: class collection: getitem(self, id): ... createitem(self, id): item = item(id, self) # <-- pass self ... class item: __init__(self, id, col): ... col.getite...
Read more

go - serving up pdfs using golang -

Image
just wondering if guys can code. it works serving images not pdf brochure. in advance func main(){ http.handlefunc("/", func(w http.responsewriter, r *http.request){ filename := "/var/www/filedipenser/brochure.pdf" streampdfbytes, err := ioutil.readfile( filename ) if err != nil { fmt.println(err) os.exit(1) } b := bytes.newbuffer(streampdfbytes) w.header().set("content-type", "application/pdf") if _, err := b.writeto(w); err != nil { fmt.fprintf(w, "%s", err) } w.write([]byte("pdf generated")) }) err := http.listenandserve(":4111", nil) if err != nil { log.fatal("listenandserve: ", err) fmt.println(err) } } the code bit inefficient appears working. however, pdf viewers might sensitive extraneous output adding end of http response stream...
Read more

how to add preprocess loader in webpack 2 -

i trying add preprocess loader in webpack 3. have installed successfully. not working here's webconfing file var debug = process.env.node_env !== "production"; var webpack = require('webpack'); var path = require('path'); module.exports = { context: path.join(__dirname, "src"), devtool: debug ? "inline-sourcemap" : null, entry: "./js/app.js", module: { loaders: [ { test: /\.jsx?$/, exclude: /(node_modules|bower_components)/, loader: 'babel-loader!preprocess-loader?+debug', // query: { // presets: ['react', 'es2015'], // plugins: ['react-html-attrs', 'transform-class-properties', 'transform-decorators-legacy'], // } }, { test: /\.css$/, loader: "style-loader!css-loader!sass-loader" } ] }, output: { path: __dirname + "/src/", f...
Read more