szynwelski / nlambda Goto Github PK

Hi,

Inference is broken. This might be my fault: when I added generic instances for the NominalType, I split the Ord/Nominal type classes, and added the constraint kind NominalType a = (BareNominalType a, Ord a), so that all the old code did not need to be changed...

The following does not compile, as the type of ns cannot be inferred to be ns :: NominalType a => [a] -> Set a.

module Main where

import NLambda
import qualified Prelude
import Prelude (print, Int, Char)

ns = fromList

main = do
  print (ns ['a' :: Char])
  print (ns [1 :: Int])

One solution is to move Ord as a context to NominalType again (like it was before). Then it'll be hard to write the generic instances.

Another option is to rewrite a bit, leaving Ord and NominalType separate classes, but then many functions need to change (as many depend on both).

More options? Maybe this is a feature we would like to have in ghc. I will try to make a small example where the same thing breaks.

When creating an atom with a number in the string, the SMT-parsing fails

> simplify $ atom "a0" `neq` atom "b" /\ atom "c" `neq` atom "d"
*** Exception: Fail to parse SMT Solver output:
- not parsed output: "(not (= a0 b))\n  (not (= c d))\n  :precision precise :depth 1)\n)\n"
- list of contexts in which the error occurred: [")"]
- error message: "Failed reading: satisfyWith"

CallStack (from HasCallStack):
  error, called at /home/joshua/Documents/Projects/popl-artifact-mod/nlambda-git/src/Nominal/Formula/Solver.hs:220:25 in main:Nominal.Formula.Solver

It would be useful (at least to me) to have a Read instance for Atom. I am planning to read constants (not variables), so that I can parse counter examples from an external teacher.

I want to know whether there was a reason to leave it out?

Implement three new functions:

• model :: Formula -> Map Variable Variable - for finding model of given formula,
• setElement :: Set a -> Maybe a - that returns some particular element of the set (or Nothing if set is empty),
• orbitRepresentatives :: Set a -> [a] - that returns some representatives of orbits of the set.

Hi!

I am using the setOrbitsRepresentatives function now, but I run into a problem where it returns Nothing (and I am not sure it should do that...)
I am printing some debug info in my algorithm, and this is what I get (first line is the set, second line are the representatives given by setOrbitsRepresentatives):

{[a₁,a₂,a₃] : a₁ = a₂ for a₁,a₂,a₃ ∊ 𝔸, [a₁,a₂,a₃,a₄] : a₁ ≠ a₂ ∧ (a₁ = a₃ ∨ a₂ = a₃) for a₁,a₂,a₃,a₄ ∊ 𝔸, [a₁,a₂,a₃,a₄,a₅] : a₁ ≠ a₂ ∧ a₁ ≠ a₃ ∧ a₂ ≠ a₃ for a₁,a₂,a₃,a₄,a₅ ∊ 𝔸}
{Nothing, Just [0,0,0], Just [1,0,0,0], Just [1,1,0], Just [2,3,2,2], Just [2,3,2,3], Just [2,3,3,2], Just [3,4,3,5], Just [3,4,4,5], Just [3,4,5,3,3], Just [3,4,5,3,4], Just [3,4,5,3,5], Just [3,4,5,4,3], Just [3,4,5,4,4], Just [3,4,5,4,5], Just [3,4,5,5,3], Just [3,4,5,5,4], Just [3,4,5,5,5], Just [4,5,6,4,7], Just [4,5,6,5,7], Just [4,5,6,6,7], Just [4,5,6,7,4], Just [4,5,6,7,5], Just [4,5,6,7,6], Just [4,5,6,7,7], Just [5,6,7,8,9]}

However, when I try to reproduce the bug in ghci, the set is represented differently internally, so it doesn't show the bug...

Prelude NLambda> let x = NLambda.filter (\[a,b,c] -> a `eq` b) (replicateAtoms 3) `union` NLambda.filter (\[a,b,c,d] -> a `neq` b /\ (a `eq` c \/ b `eq` c)) (replicateAtoms 4) `union` NLambda.filter (\[a,b,c,d,e] -> a `neq` b /\ a `neq` c /\ b `neq` c) (replicateAtoms 5)
Prelude NLambda> x
{[a₁,a₁,a₂] : for a₁,a₂ ∊ 𝔸, [a₁,a₂,a₃,a₄] : a₁ ≠ a₂ ∧ (a₁ = a₃ ∨ a₂ = a₃) for a₁,a₂,a₃,a₄ ∊ 𝔸, [a₁,a₂,a₃,a₄,a₅] : a₁ ≠ a₂ ∧ a₁ ≠ a₃ ∧ a₂ ≠ a₃ for a₁,a₂,a₃,a₄,a₅ ∊ 𝔸}
Prelude NLambda> setOrbitsRepresentatives x
{Just [0,0,0], Just [1,0,0,0], Just [1,1,0], Just [2,3,2,2], Just [2,3,2,3], Just [2,3,3,2], Just [3,4,3,5], Just [3,4,4,5], Just [3,4,5,3,3], Just [3,4,5,3,4], Just [3,4,5,3,5], Just [3,4,5,4,3], Just [3,4,5,4,4], Just [3,4,5,4,5], Just [3,4,5,5,3], Just [3,4,5,5,4], Just [3,4,5,5,5], Just [4,5,6,4,7], Just [4,5,6,5,7], Just [4,5,6,6,7], Just [4,5,6,7,4], Just [4,5,6,7,5], Just [4,5,6,7,6], Just [4,5,6,7,7], Just [5,6,7,8,9]}

I will try to find a smaller example.

My current work around is to simply ignore the Nothing, but I'm not sure that is the right way to go.

Write a function similar to replicateAtoms but with all different atoms.

>>> replicateDifferentAtoms 3
{[a₁,a₂,a₃] : a₁ ≠ a₂ ∧ a₁ ≠ a₃ ∧ a₂ ≠ a₃ for a₁,a₂,a₃ ∊ 𝔸}

In your talk at the Simons Institute, you say you want to use if ... then ... else like in normal Haskell programs. You actually can, you just need to enable RebindableSyntax and locally redefine ifThenElse. I have a simple solution here [https://github.com/SamuelSchlesinger/nlambda/blob/master/src/Nominal/If.hs].

I don't think you really have a need to get up inside the compiler itself, as there are plugins and other easier ways to change these things. Also, have you considered implementing the difference between ordered atoms and equality atoms as a type family or something of that sort? Is that a problem on the end of getting Z3 to behave with the two separate universes? As well, is the API referentially transparent? If so, how do you handle Z3 in the background to make it so?

Awesome work by the way, really excited to use/read it

Check whether set variables conflict names can be resolved more efficiently on the Haskell compiler level.