Re: [cloud-haskell-developers] Does anyone have much experience generating Haskell from Coq?
On Mon, 10 Dec 2018, 09:30 Gershom B The other approach, which has been quite successful, by the penn team, > is using hs-to-coq to extract coq from haskell and _then_ verify: > https://github.com/antalsz/hs-to-coq Thank you! Someone else proposed that off list yesterday too. If we get our layering right, that could definitely be a viable alternative! I will do some more research. I generally think that https://deepspec.org/ is an awesome idea. :) ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users
Re: Equality constraints (~): type-theory behind them
On Mon, 10 Dec 2018 at 9:36 PM, Tom Schrijvers wrote:
> Maybe our Haskell'17 paper about Elaboration on Functional Dependencies
> sheds some more light on your problem:
>
> https://people.cs.kuleuven.be/~tom.schrijvers/Research/papers/haskell2017a.pdf
>
>
Thank you Tom, looks interesting and very applicable. It'll be a few days
before I can take a proper look.
I see you compare GHC vs Hugs: good, they differ significantly in the
details of implementation. I found Hugs well-principled, whereas GHC is far
too sloppy in what instances it accepts (but then you find they're
unusable).
Maybe I scanned your paper too quickly, but it looks like you insist on
non-overlapping instances (or that if instances overlap, they are
'confluent', in the terminology of the 2005~2008 work; or 'coincident' in
Richard E's work). And the 2006 CHRs paper takes the same decision. That's
a big disappointment: I think the combo of Overlap+FunDeps makes sense (you
need to use (~) constraints -- hence this thread), and there's plenty of
code using the combo -- including the HList 2004 paper (with `TypeCast`).
You can make that combo work with GHC, as did HList. But it's hazardous
because of GHC's sloppiness/bogusness. You can't make that combo work with
Hugs as released; but because it's a better principled platform, a
limited-scope tweak to the compiler makes it work beautifully. Documented
here: https://ghc.haskell.org/trac/ghc/ticket/15632#comment:2
AntC
> On Sat, Dec 8, 2018 at 6:42 AM Anthony Clayden <
> anthony_clay...@clear.net.nz> wrote:
>
>> On Fri, 7 Dec 2018 at 10:57 PM, Adam Gundry wrote:
>>
>>>
>>> Regarding inference, the place that comes to mind is Vytiniotis et al.
>>> OutsideIn(X):
>>>
>>
>> Thanks Adam for the references. Hmm That OutsideIn paper is formidable in
>> so many senses ...
>>
>> I'm not sure I grok your response on my specific q; to adapt your example
>> slightly, without a signature
>>
>> foo2 x@(_: _) = x
>>
>> GHC infers `foo2 :: [a] -> [a]`. That's not general enough. So I give a
>> signature with bare `b` as the return type, using the (~) to improve it:
>>
>> foo2 :: [a] ~ b => [a] -> b
>>
>> ... and GHC infers `foo2 :: [a] -> [a]`. Oh. Is that what I should expect?
>>
>> I'm chiefly concerned about improving bare tyvars under a FunDep. So to
>> take the time-worn example, I want instances morally equivalent to
>>
>> data TTrue = TTrue; data TFalse = TFalse
>>
>> class TEq a b r | a b -> r where tEq :: a -> b -> r
>>
>> instance TEq a a TTrue where tEq _ _ = TTrue
>> instance TEq a b TFalse where tEq _ _ = TFalse
>>
>> The FunDeps via CHRs 2006 paper tells me that first instance is supposed
>> to be as if
>>
>> instance (r ~ TTrue) => TEq a a r where ...
>>
>> but it isn't
>>
>> tEq 'a' 'a' :: TFalse -- returns TFalse, using the first pair of
>> instances
>> tEq 'a' 'a' :: TFalse -- rejected, using the (~) instance:
>> 'Couldn't match type TFalse with TTrue ...'
>>
>> The 'happily' returning the 'wrong' answer in the first case has caused
>> consternation amongst beginners, and a few Trac tickets.
>>
>> So what magic is happening with (~) that it can eagerly improve `foo2`
>> but semi-lazily hold back for `tEq`?
>>
>> Of course I lied about the first-given two instances for TEq: instances
>> are not consistent with Functional Dependency. So I need to resort to
>> overlaps and a (~) and exploit GHC's bogus consistency check:
>>
>> instance {-# OVERLAPPABLE #-} (r ~ TFalse) => TEq a b r where ...
>>
>> > ... like automatically inferring where `typeCast` needs to be placed
>>
>> Yes the non-automatic `TypeCast` version
>>
>> instance (TypeCast TTrue r) => TEq a a r where
>> tEq _ _ = TTrue -- rejected 'Couldn't match expected type
>> 'r' with actual type 'TTrue' ...'
>>
>> tEq _ _ = typeCast TTrue-- accepted
>>
>> Even though `typeCast` is really `id` (after it's jumped through the
>> devious indirection hoops I talked about).
>>
>> So what I'm trying to understand is not just "where" to place `typeCast`
>> but also "when" in inference it unmasks the unification.
>>
>>
>> AntC
>>
>>
>>> About your specific question, if a wanted constraint `a ~ b` can be
>>> solved by unifying `a` with `b`, then GHC is free to do so (in a sense,
>>> either parameter of (~) can be improved from the other). The real
>>> difference with `TypeCast` arises when local equality assumptions (given
>>> constraints) are involved, because then there may be wanted constraints
>>> that cannot be solved by unification but can be solved by exploiting the
>>> local assumptions.
>>>
>>> For example, consider this function:
>>>
>>> foo :: forall a b . a ~ b => [a] -> [b]
>>> foo x = x
>>>
>>> When checking the RHS of `foo`, a wanted constraint `[a] ~ [b]` arises
>>> (because `x` has type `[a]` and is used in a place where `[b]` is
>>> expected). Since `a` and `b` are universally quantified variables, this
>>> cannot be solved by unificat
Re: [cloud-haskell-developers] Does anyone have much experience generating Haskell from Coq?
The other approach, which has been quite successful, by the penn team, is using hs-to-coq to extract coq from haskell and _then_ verify: https://github.com/antalsz/hs-to-coq -g On Sat, Dec 8, 2018 at 7:05 AM Tim Watson wrote: > > So far I've been reading > https://www.cs.purdue.edu/homes/bendy/Fiat/FiatByteString.pdf. I'm interested > in the ideas presented in > https://github.com/DistributedComponents/verdi-runtime, which is OCaml based. > > My goal is to provide building blocks for verifying and testing Cloud Haskell > programs. I've been looking at existing frameworks (such as > quickcheck-state-machine/-distributed and hedgehog) for model based testing, > and ways of injecting an application layer scheduler for detecting race > conditions. The final bit of the puzzle is being able to apply formal methods > to verify concurrent/distributed algorithms, and generate some (if not all) > of the required implementation code. > > Any pointers to research or prior art would be greatly appreciated. > > Cheers, > Tim Watson > > -- > You received this message because you are subscribed to the Google Groups > "cloud-haskell-developers" group. > To unsubscribe from this group and stop receiving emails from it, send an > email to cloud-haskell-developers+unsubscr...@googlegroups.com. > To post to this group, send email to > cloud-haskell-develop...@googlegroups.com. > Visit this group at https://groups.google.com/group/cloud-haskell-developers. > For more options, visit https://groups.google.com/d/optout. ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users
Re: Equality constraints (~): type-theory behind them
Hi Anthony,
Maybe our Haskell'17 paper about Elaboration on Functional Dependencies
sheds some more light on your problem:
https://people.cs.kuleuven.be/~tom.schrijvers/Research/papers/haskell2017a.pdf
Cheers,
Tom
On Sat, Dec 8, 2018 at 6:42 AM Anthony Clayden
wrote:
> On Fri, 7 Dec 2018 at 10:57 PM, Adam Gundry wrote:
>
>>
>> Regarding inference, the place that comes to mind is Vytiniotis et al.
>> OutsideIn(X):
>>
>
> Thanks Adam for the references. Hmm That OutsideIn paper is formidable in
> so many senses ...
>
> I'm not sure I grok your response on my specific q; to adapt your example
> slightly, without a signature
>
> foo2 x@(_: _) = x
>
> GHC infers `foo2 :: [a] -> [a]`. That's not general enough. So I give a
> signature with bare `b` as the return type, using the (~) to improve it:
>
> foo2 :: [a] ~ b => [a] -> b
>
> ... and GHC infers `foo2 :: [a] -> [a]`. Oh. Is that what I should expect?
>
> I'm chiefly concerned about improving bare tyvars under a FunDep. So to
> take the time-worn example, I want instances morally equivalent to
>
> data TTrue = TTrue; data TFalse = TFalse
>
> class TEq a b r | a b -> r where tEq :: a -> b -> r
>
> instance TEq a a TTrue where tEq _ _ = TTrue
> instance TEq a b TFalse where tEq _ _ = TFalse
>
> The FunDeps via CHRs 2006 paper tells me that first instance is supposed
> to be as if
>
> instance (r ~ TTrue) => TEq a a r where ...
>
> but it isn't
>
> tEq 'a' 'a' :: TFalse -- returns TFalse, using the first pair of
> instances
> tEq 'a' 'a' :: TFalse -- rejected, using the (~) instance:
> 'Couldn't match type TFalse with TTrue ...'
>
> The 'happily' returning the 'wrong' answer in the first case has caused
> consternation amongst beginners, and a few Trac tickets.
>
> So what magic is happening with (~) that it can eagerly improve `foo2` but
> semi-lazily hold back for `tEq`?
>
> Of course I lied about the first-given two instances for TEq: instances
> are not consistent with Functional Dependency. So I need to resort to
> overlaps and a (~) and exploit GHC's bogus consistency check:
>
> instance {-# OVERLAPPABLE #-} (r ~ TFalse) => TEq a b r where ...
>
> > ... like automatically inferring where `typeCast` needs to be placed
>
> Yes the non-automatic `TypeCast` version
>
> instance (TypeCast TTrue r) => TEq a a r where
> tEq _ _ = TTrue -- rejected 'Couldn't match expected type
> 'r' with actual type 'TTrue' ...'
>
> tEq _ _ = typeCast TTrue-- accepted
>
> Even though `typeCast` is really `id` (after it's jumped through the
> devious indirection hoops I talked about).
>
> So what I'm trying to understand is not just "where" to place `typeCast`
> but also "when" in inference it unmasks the unification.
>
>
> AntC
>
>
>> About your specific question, if a wanted constraint `a ~ b` can be
>> solved by unifying `a` with `b`, then GHC is free to do so (in a sense,
>> either parameter of (~) can be improved from the other). The real
>> difference with `TypeCast` arises when local equality assumptions (given
>> constraints) are involved, because then there may be wanted constraints
>> that cannot be solved by unification but can be solved by exploiting the
>> local assumptions.
>>
>> For example, consider this function:
>>
>> foo :: forall a b . a ~ b => [a] -> [b]
>> foo x = x
>>
>> When checking the RHS of `foo`, a wanted constraint `[a] ~ [b]` arises
>> (because `x` has type `[a]` and is used in a place where `[b]` is
>> expected). Since `a` and `b` are universally quantified variables, this
>> cannot be solved by unification. However, the local assumption (given
>> constraint) `a ~ b` can be used to solve this wanted.
>>
>> This is rather like automatically inferring where `typeCast` needs to be
>> placed (indeed, at the Core level there is a construct for casting by an
>> equality proof, which plays much the same role).
>>
>> Hope this helps,
>>
>> Adam
>>
>>
>> On 06/12/2018 12:01, Anthony Clayden wrote:
>> > The (~) constraint syntax is enabled by either `GADTs` or `TypeFamilies`
>> > language extension.
>> >
>> > GADTs/Assoc Data Types/Assoc Type Synonyms/Type Families arrived in a
>> > series of papers 2005 to 2008, and IIRC the development wasn't finished
>> > in full in GHC until after that. (Superclass constraints took up to
>> > about 2010.)
>> >
>> > Suppose I wanted just the (~) parts of those implementations. Which
>> > would be the best place to look? (The Users Guide doesn't give a
>> > reference.) ICFP 2008 'Type Checking with Open Type Functions' shows
>> > uses of (~) in user-written code, but doesn't explain it or motivate it
>> > as a separate feature.
>> >
>> > My specific question is: long before (~), it was possible to write a
>> > TypeCast class, with bidirectional FunDeps to improve each type
>> > parameter from the other. But for the compiler to see the type
>> > improvement at term level, typically you also need a typeCast method and
>> > to
