Can NixString be the NAtom?

[Anton-Latukha]

Upon progressing with #509, in the current issue, I am wrestling with existential higher-rank type inference. And everything came into the one type level puzzle piece: Expected NAtom, actual type NixString.

And I thought why not both? It seems like it should be so.

It seems like Nix-native NixString ({Text, Hash}) indeed can be represented with an NAtom since it is a literal pun, and one of the Nix basic types.

In Strings.hs there is extract & create & modify and such:

hnix/src/Nix/String.hs

Lines 225 to 227 in 0305b52

	-- | Get the contents of a 'NixString' and write its context into the resulting set.
	extractNixString :: Monad m => NixString -> WithStringContextT m Text
	extractNixString (NixString s c) = WithStringContextT $ tell c >> return s

hnix/src/Nix/String.hs

Lines 201 to 208 in 0305b52

	-- | Create a NixString using a singleton context
	principledMakeNixStringWithSingletonContext
	:: Text -> StringContext -> NixString
	principledMakeNixStringWithSingletonContext s c = NixString s (S.singleton c)
	-- | Create a NixString from a Text and context
	principledMakeNixString :: Text -> S.HashSet StringContext -> NixString
	principledMakeNixString s c = NixString s c

And in Atom.hs everything seems welcoming it also:

hnix/src/Nix/Atoms.hs

Lines 21 to 50 in 0305b52

	-- | Atoms are values that evaluate to themselves. This means that
	-- they appear in both the parsed AST (in the form of literals) and
	-- the evaluated form.
	data NAtom
	-- | An integer. The c nix implementation currently only supports
	-- integers that fit in the range of 'Int64'.
	= NInt Integer
	-- | A floating point number
	| NFloat Float
	-- | Booleans.
	| NBool Bool
	-- | Null values. There's only one of this variant.
	| NNull
	deriving (Eq, Ord, Generic, Typeable, Data, Show, Read, NFData,
	Hashable)
	#ifdef MIN_VERSION_serialise
	instance Serialise NAtom
	#endif
	-- | Translate an atom into its nix representation.
	atomText :: NAtom -> Text
	atomText (NInt i) = pack (show i)
	atomText (NFloat f) = pack (showNixFloat f)
	where
	showNixFloat x
	| x `mod'` 1 /= 0 = show x
	| otherwise = show (truncate x :: Int)
	atomText (NBool b) = if b then "true" else "false"
	atomText NNull = "null"

At least that should help type system and me, simplify some type inference, and probably would allow to even better formalize the text & string functions.

Is this sane idea?

[Anton-Latukha]

To put my words more direcly:

String is an NAtom type in Nix language.

In Nix language, there is no such type as char (manual). And string can not be assembled from list of chars, only from other strings. The string is an atomic (primitive) base type in the Nix language.

[sorki]

So do you propose adding NString NixString to NAtom?

[Anton-Latukha]

Once more.

NAtom means Nix Atomic Types.

The source description of the initial author also belabors it:

 -- | Atoms are values that evaluate to themselves. This means that 
 -- they appear in both the parsed AST (in the form of literals) and 
 -- the evaluated form. 

It is Nix-native atomic types, they are as they are in AST and evaluate to themselves, at least the Strings evaluate into themselves.

I also had a pretty good nod from the type system that it should be in there.

[Anton-Latukha]

Actually great: f682907

[Anton-Latukha]

+====

As we know there were NixString in Strings.hs and NStrings in Expr/Types.hs.

For me it is interesting what data type version should be in NAtom:

NString 
  { nsContents :: !Text 
  , nsContext :: !(S.HashSet StringContext) 
  }

-- OR

NString r
  = DoubleQuoted ![Antiquoted Text r]
  | Indented !Int ![Antiquoted Text r]

---

1. I started from this NixString - because that was my old muddy knowledge telling me. I remember that even String was Nix a basic type - it was even weirder - it hold its around context for reasons.

---

2. And John had to do hacky* methods for it - that shown me that system tells that something was not data typed right around those methods.

---

3. And I got a direct nod from the type system that NixString really stringly wants to be an NAtom at the same time in the 2-3 level ranked type functions. I just could not get some very simple logical things done, because NixString was not a NAtom.

---

4. I remeber that String with context - is essentially not only String - it is a general type of all possible Nix expressions in Nix. And I remeber reading several explanations about that, that expressions always need to preserve a proper context to be understood, sorted where what goes and evaluated properly by interpreter.

---

5. For all expressions that are possible - there are:

• a context-free grammar to expressions that Noam Chomsky shown,
• and a contextual grammar

Only when they are both combined - there is a meaning in the expression.

The context bears rules How to apply the expression properly. As some physicians say - physics explains "How" (how it, world behaves), it does not concerned with "Why" until it collides with physics. Question How is perpendicular to Why.

If we talk to an alien - we would not understand each other right away, because we do not know the context, we do not know How to share information between.

Richard Feynman was also famous for his explanations that meaning&context is a dao thing.

He shows that simple "Why?" always changes and expands the context. And in the end where is no context we can grasp - you can never explain "Why?".

He often said that his father taught him: "Let us think/look at this like Martians (or mushrooms)", he used this method of thinking to find other ways of context&meaning to see other sides of the question, quite like in discussion everybody has a somewhat different context to share. But he had a contrary, perpendicular goal.

HNix NAtom and expression type (NString :: NAtom) - is a core specification for the mutual protocolled transmission of data through the different parts of the system.

---

6. HNix and Expr - are there to establish/follow a grammatical/contextual protocol - to transmit the most well known shared meaning of Nix Expr language through the system - so we preserve a share understandable context, so all Expr are understood and acted-on properly according to instructions of the context.

That is why any expression or language bear context. And Nix had one basic type for both Expression and String, and context of it.

---

7. Expr with context essentially embodies everything and the operations inside of it

Then Nix can manage anything literally, even the Expression that has String with literal Nix expressions inside of it (comment with code samples) - so it can for Nix be both String and Expression, depending on the context said to the interpreter.

So for example we can be explained by context to the interpreter - for example the whole Nixpkgs to be treated as NAtom - do not try to interpret any of it at any situation - just move it/clone it somewhere. And that is a basic instruction to the interpreter. The type and what single action to do - that is why Expr/NString is inside NAtom.

When/if Nixpkgs splits into Flakes - we see that those NAtom abilities become essential to move Flakes, compose them around.

Or if we do any actions with any two expressions, deliver some expression into the main expression - we see how is that smaller one should be the NAtom in AST for the interpreter - so interpreter would move the NAtom around and properly put it inside the main expression. And then/when context changes - & the interpreter allowed to evaluate it - it from NAtom becomes the readable expression to the interpreter, and so it is together composed.

---

I now do not properly remember where I remember it from, so many scattered Nix materials. I've read it somewhere in the past, maybe even NixPills. I also remember seeing/reading the basic types in Nix source code. I definitely remember there were 6 of the basic types and that String preserved context.

[Anton-Latukha]

I am on sides of it.

It seems logical.

But the other type also looks so simple, and without context.

I think we need not invent own stuff - because we would get headbumps and some processing details changes that would resolve in some discrepancies while we stay try to preserve proper Nix lang to evaluate Nixpkgs and bisimulate Nix. It just trying juggle too much.

I also think we should really bisimulate the type system of Nix first - then it is a way easier to rely on that to bisimulate the existing language and its meaning on top of it. If something - we always would be able to read the code how it is made.
And after that designed and behaves canonically - it would be road open to easy bisimulate the whole Nix stack. And that is the main goal of the project.

[sorki]

Looking at the code it's now clear to me what you've meant but I'm not really sure which approach is better.

Regarding hacky functions I've thought the reason for them was missing integration with hnix-store as they seem to require some store functionality, #554 tackles this a bit so maybe @layus can chime in as well.

For the reference I'll add http://blog.shealevy.com/2018/08/05/understanding-nix's-string-context/ by @shlevy who also authored the current string context handling.

[Anton-Latukha]

In NAtom Strings OR Expressions should be represented, basically, any Strings are also Expressions, they are really they are the same thing, in Nix moreover.

[Anton-Latukha]

Closing in favour of more gradual approach to the question: #657