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

networking - Vagrant-provisioned VirtualBox VM is not reachable from Ubuntu host -

this question exact duplicate of: puphpet/vagrant: unable access lamp vm ip address 1 answer i following basic vagrant tutorial , vagrant provisions box on ubuntu without complaining. moreover, can vagrant ssh vm. however, vm not reachable host: it's not possible ping it's ip address. what have achieved: installed virtualbox (5.1.24 r117012 (qt5.5.1)) , vagrant (1.9.7) onto ubuntu (16.04.2 lts) machine. provisioned vm vagrant up , vagrant finishes job , not complain. vagrant ssh works. i have manually installed lighttpd on guest vm , can ping/curl address: localhost within guest vm. this when trying reach guest vm host: ~/tmp/myfirstvagrantproject$ ping 172.22.22.22 ping 172.22.22.22 (172.22.22.22) 56(84) bytes of data. ... icmp_seq=4 destination net unreachable ... 171 packets transmitted, 0 received, +21 errors, 100% packet loss, time 173
Read more

c# - ASP.NET Core - There is already an object named 'AspNetRoles' in the database -

i'm receiving error applicationdbcontext database when trying update entity framework. i've googled, tried fixes here on so, no avail. i'm deleting database each time make change, once deploy, not option. here's error: pm> update-database -context applicationdbcontext system.data.sqlclient.sqlexception: there object named 'aspnetroles' in database. @ system.data.sqlclient.sqlconnection.onerror(sqlexception exception, boolean breakconnection, action 1 wrapcloseinaction) @ system.data.sqlclient.tdsparser.throwexceptionandwarning(tdsparserstateobject stateobj, boolean callerhasconnectionlock, boolean asyncclose) @ system.data.sqlclient.tdsparser.tryrun(runbehavior runbehavior, sqlcommand cmdhandler, sqldatareader datastream, bulkcopysimpleresultset bulkcopyhandler, tdsparserstateobject stateobj, boolean& dataready) @ system.data.sqlclient.sqlcommand.runexecutenonquerytds(string methodname, boolean async, int32 timeout, boolean
Read more

ruby on rails - ArgumentError: Missing host to link to! Please provide the :host parameter, set default_url_options[:host], or set :only_path to true -

i have built module in solidus , ruby on rails , try create tests. i trying create integration tests , have error: e error: prescriptionphotostest#test_/prescription_photos_post_endpoint_throws_an_error_when_wrong_params: argumenterror: missing host link to! please provide :host parameter, set default_url_options[:host], or set :only_path true test/integration/prescription_photos_test.rb:6:in `block in ' i read this , this , doesn't make difference. my code returning error on line: @user = factorygirl.create(:user) here code files. prescription_photos_rest.rb require 'test_helper' class prescriptionphotostest < actiondispatch::integrationtest setup spree::auth::config[:confirmable] = false @user = factorygirl.create(:user) end def authenticated_header token = knock::authtoken.new(payload: { sub: @user.id }).token { 'authorization': "bearer #{token}" } end test '/prescription_p
Read more