text:
# How far can a golf ball travel on the moon?

## Homework Statement

If you can hit a golf ball 180m on Earth, how far can you hit it on the Moon?

## The Attempt at a Solution

Since this question deals with range;

sx = [vxi^2 sinΘ]/g

My problem is that I do not have the velocity at which the golf ball is being hit. As for the launch angle, I could make a probable assumption that the golf ball is launched at a 45°.
Would I be valid to make the assumption the ball would travel 6x further on the Moon than on the Earth given the gravitational pull on the Moon is 1/6 that of Earth?

Last edited:

tiny-tim
Homework Helper
hi negation!
Would I be valid to make the assumption the ball would travel 6x further on the Moon than on the Earth given the gravitational pull on the Moon is 1/6 that of Earth?

negative!

work it out!!
As for the launch angle, I could make a probable assumption that the golf ball is launched at a 45°.

yes, maximum range (for fixed speed) is at 45°

1 person
rude man
Homework Helper
Gold Member
You should calculate the range based on the different values of g on Earth and on the Moon.
Assume arbitrary velocity v and angle theta.

You will find out when you finish your calculations whether the velocity and/or angle impact the answer to the question.

1 person
haruspex
Homework Helper
Gold Member
sx = vxi^2 sinΘ
You've left a very important term of that equation.
(It's obviously wrong because the dimensions don't match. You have a distance on one side and the square of a velocity on the other.)

You've left a very important term of that equation.
(It's obviously wrong because the dimensions don't match. You have a distance on one side and the square of a velocity on the other.)

I carelessly left out the time variable, t.

haruspex
Homework Helper
Gold Member
I carelessly left out the time variable, t.

No, that's not what's missing. Check where you got that equation from.

No, that's not what's missing. Check where you got that equation from.

It has been corrected: sx = [vxi^2 sinΘ]/g after having derived it from the trajectory equation.

hi negation!

Negative!

work it out!!

yes, maximum range (for fixed speed) is at 45°

you should calculate the range based on the different values of g on earth and on the moon.
Assume arbitrary velocity v and angle theta.

You will find out when you finish your calculations whether the velocity and/or angle impact the answer to the question.

you've left a very important term of that equation.
(it's obviously wrong because the dimensions don't match. You have a distance on one side and the square of a velocity on the other.)

haruspex
Homework Helper
Gold Member
It has been corrected: sx = [vxi^2 sinΘ]/g after having derived it from the trajectory equation.
Right, and from that you can see that the distance is inversely proportional to the strength of gravity. So your guess was right: one sixth the gravity means 6 times the distance.

1 person
ehild
Homework Helper
Since this question deals with range;

sx = [vxi^2 sinΘ]/g

The equation is wrong.

ehild

haruspex
Homework Helper
Gold Member
The equation is wrong.

ehild
Ah yes, good catch. There's a 2 missing, right?

Ah yes, good catch. There's a 2 missing, right?

I noticed. It ought to be sin^2θ

haruspex
Homework Helper
Gold Member
I noticed. It ought to be sin^2θ
Not quite.

ehild
Homework Helper
The time of flight is t=2viy/g=2visin(θ)/g. The horizontal displacement during that time is sx=vicos(θ)t= 2vi2cos(θ)sin(θ)/g=[vi2sin(2θ)]/g. With a given initial speed, maximum range is at θ=45°.

Do not use vix in the formula for sx.

ehild

Not quite.

Are you sure?

I managed to obtain the right answer. I have poor memorizing abilities and as such I derive equations I require(very time consuming).

The formula I derived is x = [2vxi^2sin45°]/g

This enables me to obtain vxi. After which I use the above formula to determine the x-displacement on the moon.

ehild
Homework Helper
I wonder how you got that formula...

ehild

I wonder how you got that formula...

ehild

it works fine...

I have used my own arbitrary label of the variables but they essentially implies the same thing.
In my formula, I determine the time taken for the particle to travel from xi to xf.
The time taken for particle to be displaced from xi - xf can be substituted into the y-displacement equation to determine the displacement of the particle along the y-axis-this allows me to determine the x and y coordinate of the particle at a given time.
Simplifying the equation where t = sx/ vicosΘ into the y = visinΘ-0.5gt^2 produces a quadratic equation which allows me to determine the 2 possible x-coordinate of the particle where y = 0 since the trajectory has a parabolic characteristic.

In simplifying further, I obtain x = 2vi^2sinΘ/g; given 3 known variables, I can find the one unknown.

I saw the reasoning in the link you provided. The reasoning in the link begins by using the y-displacement equation to determine the time taken for the particle to be displaced from yi to yi. Then it subs that amount of time into the x-displacement equation to determine the horizontal range the particle travels in that same amount of time.

As for the formula I used, I begin with determining the time taken for the particle to be displaced from xi -xf.

Last edited:
ehild
Homework Helper
I have used my own arbitrary label of the variables but they essentially implies the same thing.

So what are vx and vy (or vxi and vyi) in your derivation?

In my formula, I determine the time taken for the particle to travel from xi to xf.
The time taken for particle to be displaced from xi - xf can be substituted into the y-displacement equation to determine the displacement of the particle along the y-axis-this allows me to determine the x and y coordinate of the particle at a given time.
Simplifying the equation where t = sx/ vicosΘ into the y = visinΘ-0.5gt^2 produces a quadratic equation which allows me to determine the 2 possible x-coordinate of the particle where y = 0 since the trajectory has a parabolic characteristic.

That is correct.

In simplifying further, I obtain x = 2vi^2sinΘ/g;

That is still wrong.

ehild

haruspex
Homework Helper
Gold Member
View attachment 65737

it works fine...
The line that start "sx = 0 V" is fine (except for a spurious extra θ), but in going from there to the next line you dropped a cos(θ).
There is an easier way: forget sy, compute the flight time. Time to reach apex is vy/g.

The line that start "sx = 0 V" is fine (except for a spurious extra θ), but in going from there to the next line you dropped a cos(θ).
There is an easier way: forget sy, compute the flight time. Time to reach apex is vy/g.

I saw that. It was a typo but, admittedly, I was lazy to have it changed.
I went through the link again, understood the reasoning, and I must say it has more clarity.

So what are vx and vy (or vxi and vyi) in your derivation?

ehild

Understood.

haruspex
Homework Helper
Gold Member
I saw that. It was a typo but, admittedly, I was lazy to have it changed.
OK, but that's why you got this wrong formula: x = 2vi^2sinΘ/g
What formula do you get now?

OK, but that's why you got this wrong formula: x = 2vi^2sinΘ/g
What formula do you get now?

I got this: x = vi^2sin[2Θ]/g

I made a careless mistake by overlooking the trig identity where 2cos(x)sin(x) = sin(2x):

Last edited:


text:
2 added 7 characters in body

I've asked a question like this before, but now I'm more interested in counting the number of covers.

We suppose given the following data.

1. A positive integer $d$

2. A finite set of closed points $B= ( b_1,\ldots,b_n )$ in $\mathbf{P}^1_\mathbf{C}$

3. Branch types $T_1,\ldots, T_n$.

Question. How many branched covers of $\mathbf{P}^1_\mathbf{C}$ exist which are branched only over $b_i$ (with branch type $T_i$ over each $b_i$)?

The answer lies within the Hurwitz number for $(T_1,\ldots,T_n)$. This translates the problem to combinatorial group theory.

Now, for my main question:

Q1. Can one count'' covers of $\textrm{Spec} \mathbf{Z}$ as above? That is, can one count the number of finite field extensions $$\mathbf{Q}\subset K$$ of given degree $d=[K:\mathbf{Q}]$ which are unramified outside a given set of prime numbers $p_1,\ldots,p_n$ with ramification types $T_1,\ldots,T_n$?

I know that one can use Minkowski's Geometry of Numbers to give some nontrivial bounds on the discriminant. Is this the best we can do?

1

# Counting branched covers of the projective line and Spec Z

I've asked a question like this before, but now I'm more interested in counting the number of covers.

We suppose given the following data.

1. A positive integer $d$

2. A finite set of closed points $B= ( b_1,\ldots,b_n )$ in $\mathbf{P}^1_\mathbf{C}$

3. Branch types $T_1,\ldots, T_n$.

Question. How many branched covers of $\mathbf{P}^1_\mathbf{C}$ exist which are branched only over $b_i$ (with branch type $T_i$ over each $b_i$)?

The answer lies within the Hurwitz number for $(T_1,\ldots,T_n)$. This translates the problem to combinatorial group theory.

Now, for my main question:

Q1. Can one count'' covers of $\textrm{Spec} \mathbf{Z}$ as above? That is, can one count the number of field extensions $$\mathbf{Q}\subset K$$ of given degree $d=[K:\mathbf{Q}]$ which are unramified outside a given set of prime numbers $p_1,\ldots,p_n$ with ramification types $T_1,\ldots,T_n$?

I know that one can use Minkowski's Geometry of Numbers to give some nontrivial bounds on the discriminant. Is this the best we can do?

format: plain


text:
# 12.4 Magnetic field of a current loop

 Page 1 / 1
By the end of this section, you will be able to:
• Explain how the Biot-Savart law is used to determine the magnetic field due to a current in a loop of wire at a point along a line perpendicular to thep lane of the loop.
• Determine the magnetic field of an arc of current.

The circular loop of [link] has a radius R , carries a current I , and lies in the xz -plane. What is the magnetic field due to the current at an arbitrary point P along the axis of the loop?

We can use the Biot-Savart law to find the magnetic field due to a current. We first consider arbitrary segments on opposite sides of the loop to qualitatively show by the vector results that the net magnetic field direction is along the central axis from the loop. From there, we can use the Biot-Savart law to derive the expression for magnetic field.

Let P be a distance y from the center of the loop. From the right-hand rule, the magnetic field $d\stackrel{\to }{B}$ at P , produced by the current element $I\phantom{\rule{0.2em}{0ex}}d\stackrel{\to }{l},$ is directed at an angle $\theta$ above the y -axis as shown. Since $d\stackrel{\to }{l}$ is parallel along the x -axis and $\stackrel{^}{r}$ is in the yz -plane, the two vectors are perpendicular, so we have

$dB=\frac{{\mu }_{0}}{4\pi }\phantom{\rule{0.2em}{0ex}}\frac{I\phantom{\rule{0.2em}{0ex}}dl\phantom{\rule{0.2em}{0ex}}\mathrm{sin}\phantom{\rule{0.1em}{0ex}}\theta }{{r}^{2}}=\frac{{\mu }_{0}}{4\pi }\phantom{\rule{0.2em}{0ex}}\frac{I\phantom{\rule{0.2em}{0ex}}dl}{{y}^{2}+{R}^{2}}$

where we have used ${r}^{2}={y}^{2}+{R}^{2}.$

Now consider the magnetic field $d{\stackrel{\to }{B}}^{\prime }$ due to the current element $I\phantom{\rule{0.2em}{0ex}}d{\stackrel{\to }{l}}^{\prime },$ which is directly opposite $I\phantom{\rule{0.2em}{0ex}}d\stackrel{\to }{l}$ on the loop. The magnitude of $d{\stackrel{\to }{B}}^{\prime }$ is also given by [link] , but it is directed at an angle $\theta$ below the y -axis. The components of $d\stackrel{\to }{B}$ and $d{\stackrel{\to }{B}}^{\prime }$ perpendicular to the y -axis therefore cancel, and in calculating the net magnetic field, only the components along the y -axis need to be considered. The components perpendicular to the axis of the loop sum to zero in pairs. Hence at point P :

$\stackrel{\to }{B}=\stackrel{^}{j}\underset{\text{loop}}{\int }dB\phantom{\rule{0.2em}{0ex}}\mathrm{cos}\phantom{\rule{0.1em}{0ex}}\theta =\stackrel{^}{j}\frac{{\mu }_{0}I}{4\pi }\underset{\text{loop}}{\int }\frac{\mathrm{cos}\phantom{\rule{0.1em}{0ex}}\theta \phantom{\rule{0.2em}{0ex}}dl}{{y}^{2}+{R}^{2}}.$

For all elements $d\stackrel{\to }{l}$ on the wire, y , R , and $\mathrm{cos}\phantom{\rule{0.1em}{0ex}}\theta$ are constant and are related by

$\mathrm{cos}\phantom{\rule{0.1em}{0ex}}\theta =\frac{R}{\sqrt{{y}^{2}+{R}^{2}}}.$

Now from [link] , the magnetic field at P is

$\stackrel{\to }{B}=\stackrel{^}{j}\frac{{\mu }_{0}IR}{4\pi {\left({y}^{2}+{R}^{2}\right)}^{3\text{/}2}}\underset{\text{loop}}{\int }dl=\frac{{\mu }_{0}I{R}^{2}}{2{\left({y}^{2}+{R}^{2}\right)}^{3\text{/}2}}\stackrel{^}{j}$

where we have used $\underset{\text{loop}}{\int }dl=2\pi R.$ As discussed in the previous chapter, the closed current loop is a magnetic dipole of moment $\stackrel{\to }{\mu }=IA\stackrel{^}{n}.$ For this example, $A=\pi {R}^{2}$ and $\stackrel{^}{n}=\stackrel{^}{j},$ so the magnetic field at P can also be written as

$\stackrel{\to }{B}=\frac{{\mu }_{0}\mu \stackrel{^}{j}}{2\pi {\left({y}^{2}+{R}^{2}\right)}^{3\text{/}2}}.$

By setting $y=0$ in [link] , we obtain the magnetic field at the center of the loop:

$\stackrel{\to }{B}=\frac{{\mu }_{0}I}{2R}\stackrel{^}{j}.$

This equation becomes $B={\mu }_{0}nI/\left(2R\right)$ for a flat coil of n loops per length. It can also be expressed as

$\stackrel{\to }{B}=\frac{{\mu }_{0}\stackrel{\to }{\mu }}{2\pi {R}^{3}}.$

If we consider $y\gg R$ in [link] , the expression reduces to an expression known as the magnetic field from a dipole:

$\stackrel{\to }{B}=\frac{{\mu }_{0}\stackrel{\to }{\mu }}{2\pi {y}^{3}}.$

The calculation of the magnetic field due to the circular current loop at points off-axis requires rather complex mathematics, so we’ll just look at the results. The magnetic field lines are shaped as shown in [link] . Notice that one field line follows the axis of the loop. This is the field line we just found. Also, very close to the wire, the field lines are almost circular, like the lines of a long straight wire.

## Magnetic field between two loops

Two loops of wire carry the same current of 10 mA, but flow in opposite directions as seen in [link] . One loop is measured to have a radius of $R=50\phantom{\rule{0.2em}{0ex}}\text{cm}$ while the other loop has a radius of $2R=100\phantom{\rule{0.2em}{0ex}}\text{cm}.$ The distance from the first loop to the point where the magnetic field is measured is 0.25 m, and the distance from that point to the second loop is 0.75 m. What is the magnitude of the net magnetic field at point P ?

## Strategy

The magnetic field at point P has been determined in [link] . Since the currents are flowing in opposite directions, the net magnetic field is the difference between the two fields generated by the coils. Using the given quantities in the problem, the net magnetic field is then calculated.

## Solution

Solving for the net magnetic field using [link] and the given quantities in the problem yields

$\begin{array}{ccc}\hfill B& =\hfill & \frac{{\mu }_{0}I{R}_{1}{}^{2}}{2{\left({y}_{1}{}^{2}+{R}_{1}{}^{2}\right)}^{3\text{/}2}}-\phantom{\rule{0.05em}{0ex}}\frac{{\mu }_{0}I{R}_{2}{}^{2}}{2{\left({y}_{2}{}^{2}+{R}_{2}{}^{2}\right)}^{3\text{/}2}}\hfill \\ \hfill B& =\hfill & \frac{\left(4\pi \phantom{\rule{0.2em}{0ex}}×\phantom{\rule{0.2em}{0ex}}{10}^{\text{−7}}\text{T}\cdot \text{m/A}\right)\left(0.010\phantom{\rule{0.2em}{0ex}}\text{A}\right){\left(0.5\phantom{\rule{0.2em}{0ex}}\text{m}\right)}^{2}}{2{\left({\left(0.25\phantom{\rule{0.2em}{0ex}}\text{m}\right)}^{2}+{\left(0.5\phantom{\rule{0.2em}{0ex}}\text{m}\right)}^{2}\right)}^{3\text{/}2}}-\phantom{\rule{0.05em}{0ex}}\frac{\left(4\pi \phantom{\rule{0.2em}{0ex}}×\phantom{\rule{0.2em}{0ex}}{10}^{\text{−7}}\text{T}\cdot \text{m/A}\right)\left(0.010\phantom{\rule{0.2em}{0ex}}\text{A}\right){\left(1.0\phantom{\rule{0.2em}{0ex}}\text{m}\right)}^{2}}{2{\left({\left(0.75\phantom{\rule{0.2em}{0ex}}\text{m}\right)}^{2}+{\left(1.0\phantom{\rule{0.2em}{0ex}}\text{m}\right)}^{2}\right)}^{3\text{/}2}}\hfill \\ \hfill B& =\hfill & 5.77\phantom{\rule{0.2em}{0ex}}×\phantom{\rule{0.2em}{0ex}}{10}^{\text{−9}}\text{T}\phantom{\rule{0.2em}{0ex}}\text{to the right}.\hfill \end{array}$

## Significance

Helmholtz coils typically have loops with equal radii with current flowing in the same direction to have a strong uniform field at the midpoint between the loops. A similar application of the magnetic field distribution created by Helmholtz coils is found in a magnetic bottle that can temporarily trap charged particles. See Magnetic Forces and Fields for a discussion on this.

Check Your Understanding Using [link] , at what distance would you have to move the first coil to have zero measurable magnetic field at point P ?

0.608 meters

## Summary

• The magnetic field strength at the center of a circular loop is given by $B=\frac{{\mu }_{0}I}{2R}\phantom{\rule{0.2em}{0ex}}\text{(at center of loop)},$ where R is the radius of the loop. RHR-2 gives the direction of the field about the loop.

## Conceptual questions

Is the magnetic field of a current loop uniform?

What happens to the length of a suspended spring when a current passes through it?

The spring reduces in length since each coil with have a north pole-produced magnetic field next to a south pole of the next coil.

Two concentric circular wires with different diameters carry currents in the same direction. Describe the force on the inner wire.

## Problems

When the current through a circular loop is 6.0 A, the magnetic field at its center is $2.0\phantom{\rule{0.2em}{0ex}}×\phantom{\rule{0.2em}{0ex}}{10}^{\text{−4}}\text{T}.$ What is the radius of the loop?

0.019 m

How many turns must be wound on a flat, circular coil of radius 20 cm in order to produce a magnetic field of magnitude $4.0\phantom{\rule{0.2em}{0ex}}×\phantom{\rule{0.2em}{0ex}}{10}^{\text{−5}}\text{T}$ at the center of the coil when the current through it is 0.85 A?

A flat, circular loop has 20 turns. The radius of the loop is 10.0 cm and the current through the wire is 0.50 A. Determine the magnitude of the magnetic field at the center of the loop.

$6.28\phantom{\rule{0.2em}{0ex}}×\phantom{\rule{0.2em}{0ex}}{10}^{\text{−5}}\text{T}$

A circular loop of radius R carries a current I . At what distance along the axis of the loop is the magnetic field one-half its value at the center of the loop?

Two flat, circular coils, each with a radius R and wound with N turns, are mounted along the same axis so that they are parallel a distance d apart. What is the magnetic field at the midpoint of the common axis if a current I flows in the same direction through each coil?

$B=\frac{{\mu }_{o}I{R}^{2}}{{\left({\left(\frac{d}{2}\right)}^{2}+{R}^{2}\right)}^{3\text{/}2}}$

For the coils in the preceding problem, what is the magnetic field at the center of either coil?

#### Questions & Answers

Is it possible to find the magnetic field of a circular loop at the centre by using ampere's law?
Is it possible to find the magnetic field of a circular loop at it's centre?
yes
Brother
The density of a gas of relative molecular mass 28 at a certain temperature is 0.90 K kgmcube.The root mean square speed of the gas molecules at that temperature is 602ms.Assuming that the rate of diffusion of a gas in inversely proportional to the square root of its density,calculate the density of
A hot liquid at 80degree Celsius is added to 600g of the same liquid originally at 10 degree Celsius. when the mixture reaches 30 degree Celsius, what will be the total mass of the liquid?
what is electrostatics
Study of charges which are at rest
himanshu
Explain Kinematics
Two equal positive charges are repelling each other. The force on the charge on the left is 3.0 Newtons. Using your notes on Coulomb's law, and the forces acting on each of the charges, what is the force on the charge on the right?
Using the same two positive charges, the left positive charge is increased so that its charge is 4 times LARGER than the charge on the right. Using your notes on Coulomb's law and changes to the charge, once the charge is increased, what is the new force of repulsion between the two positive charges?
Nya
A mass 'm' is attached to a spring oscillates every 5 second. If the mass is increased by a 5 kg, the period increases by 3 second. Find its initial mass 'm'
a hot water tank containing 50,000g of water is heated by an electric immersion heater rated at 3kilowatt,240volt, calculate the current
what is charge
product of current and time
Jaffar
Why always amber gain electrons and fur loose electrons? Why the opposite doesn't happen?
A closely wound search coil has an area of 4cm^2,1000 turns and a resistance of 40ohm. It is connected to a ballistic galvanometer whose resistance is 24 ohm. When coil is rotated from a position parallel to uniform magnetic field to one perpendicular to field,the galvanometer indicates a charge
Using Kirchhoff's rules, when choosing your loops, can you choose a loop that doesn't have a voltage?
how was the check your understand 12.7 solved?
Who is ISSAAC NEWTON
he's the father of 3 newton law
Hawi
he is Chris Issaac's father :)
Ethem
how to name covalent bond
Who is ALEXANDER BELL
LOAK


text:
Opened 18 months ago

Closed 16 months ago

# Milner-Mycroft failure at the kind level

Reported by: Owned by: ekmett goldfire normal 7.10.1 Compiler (Type checker) 7.8.2 ekmett@…, dimitris@…, sweirich@… Unknown/Multiple Unknown/Multiple GHC rejects valid program polykinds/T9200 polykinds/T9200b #9427

### Description

This is a reduction of a problem that occurs in real code.

{-# LANGUAGE PolyKinds #-}
class D a => C (f :: k) a
class C () a => D a

Typechecking complains:

    The first argument of ‘C’ should have kind ‘k’,
but ‘()’ has kind ‘*’
In the class declaration for ‘D’

This program should be accepted, but we're not generalizing enough.

A slightly less reduced version of the problem arises in practice in:

{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE PolyKinds #-}

import Control.Category

class (Category c, Category d, Category e) => Profunctor
(p :: x -> y -> z)
(c :: x -> x -> *)
(d :: y -> y -> *)
(e :: z -> z -> *)
| p -> c d e

-- lens-style isomorphism families in an arbitrary category
type Iso (c :: i -> i -> *) (s :: i) (a :: i) = forall (p :: i -> i -> *).
Profunctor p c c (->) => p a a -> p s s

class Category e => Cartesian (e :: z -> z -> *) where
type P e :: z -> z -> z
associate :: Iso e (P e (P e a b) c) (P e a (P e b c))

This typechecks, but if I replace the line

class (Category c, Category d, Category e) => Profunctor

with

class (Category c, Category d, Cartesian e) => Profunctor

to say that you can only enrich a category over a monoidal category (using Cartesian in the approximation here), then it fails because a more baroque version of the same kind of cycle as the minimal example above as Profunctor references Cartesian which references an Iso which mentions a Profunctor.

I'm supplying explicit kind variables in the signature of the class, so we should be able to use those like we do with function signatures a universe down. =/

### comment:1 Changed 18 months ago by ekmett

• Cc ekmett@… added; ekmett removed

### comment:2 Changed 18 months ago by goldfire

Yes, this absolutely should be able to work but it currently doesn't, perhaps by design. Happily, I believe this one is actually quite easy to solve. See this comment. I believe if we changed the kind-checking strategy for classes from ParametricKinds to NonParametricKinds, this problem would be solved. I also believe that this change would allow only more programs to type-check, and would thus be fully backward compatible. Indeed, in my branch where I'm implementing a merged type/kind language, I've gotten rid of ParametricKinds.

Tracing this design through history, I think it came from work on the patch described in #6093. There, Simon proposed (and heard no complaints about) allowing polymorphic recursion if and only if a "complete user-supplied kind signature" ("cusk") is given. See section 7.8.3 of the manual. However, a cusk is not possible for classes, giving Edward no way to proceed here.

At the end of the comment trail of #6093, Simon asks for a better design. Here goes: allow recursive instantiations of a kind variable to vary if and only if that kind variable is mentioned in a type. I'm being quite literal here in my meaning of mentioned -- the kind variable must simply appear syntactically in the code. By appearing in the source, GHC can know to generalize over the kind variable "early on" and then can deal with the polymorphic recursion. With this design, the need for cusks goes away.

I think the initial reason that cusks came about in the first place is from a perceived need to either allow polymorphic recursion or to disallow it. In terms, this is straightforward: there is either a type signature or there isn't. In types, however, Haskell syntax allows for various forms of partial kind signatures. But, we had the desire for a simple "yes" or "no" answer about polymorphic recursion, and so the cusk was born. What I'm proposing here is to embrace the gray area between "yes" and "no" and permit some polymorphic recursion -- specifically, over those kind variables that are mentioned in the source.

Is this history accurate, from those involved (that is, mostly, Simon)? Do we see code that would be accepted under my proposal that would be surprising to users? Happily, implementing my proposal is dead easy -- just twiddle kind-inference strategies, as my proposal is called NonParametricKinds there.

As some context, here is an example from closed type families (the one place where NonParametricKinds is used) that is confusing:

type family LooksLikeId (x :: k) :: k where
LooksLikeId x = Bool
LooksLikeId x = Maybe

The kind of LooksLikeId surely looks like that of an identity function: k -> k. But, because type families are not parametric (hence the name NonParametricKinds), we can inspect the kind and branch on it. Note that the equations above do not overlap, as they are distinguished by their kind parameters. The definition above would fail to type-check without the k annotation, as that is necessary for GHC to know to generalize over the kind instead of just solve for it.

Thoughts on any of this? Am I deeply misunderstanding some properties of type inference here?

### comment:3 Changed 18 months ago by simonpj

That's very interesting Richard. I had not followed this particular aspect of your implementation of closed type families.

## The new proposed strategy

I would explain the strategies rather differently to you.

Baseline strategy (BASELINE), originally due to Mark Jones. Here is the strategy that we currently follow for ordinary, recursive term-level functions, and for recursive data types. I'll describe it for data types, with this example:

   data S f a b = MkS (T a f) (S f a b)
data T (a::k) (f::k -> *) :: * where
MkT :: f a -> S f a Maybe -> S f a Int -> T a f

1. Identify which type constructors have Complete User Type Signatures (CUSK). In this example, T does. Extend the environment with these, fixed, kinds:
       T :: forall k. k -> (k->*) -> *

2. Perform strongly-connected component analysis on the non-CUSK decls, ignoring dependencies on a type constructor with a CUSK. In our example, we get a single recursive component, containing S.
1. For each s-c component in turn:
• Bind the type constructor to a fresh meta-kind variable:
        S :: kappa0

• Kind-check all the declarations of the component in this environment. This will generate some unifications, so in the end we get
        kappa0 ~ (kappa1 -> *) -> kappa1 -> kappa2 -> *

The kappa1 arises from instantiating T at its call site in S
• Generalise. So we get
        S :: forall k1 k2. (k1->*) -> k1 -> k2 -> *

2. Extend the environment with these generalised kind bindings, and kind-check the CUSK declarations.

The Key Point is that we can kind-check S without looking at T's definition at all, because we completely know T's kind. That in turn means that we can exploit inferred polymorphism for S when kind-checking T. As we do here: T uses S in two different ways (S f a Maybe) and (S f a Int).

Richard's strategy (RICHARD). The key idea is that all polymorphism is declared, so nothing gets to be kind-polymorphic unless you say so. But the payoff is that you can give partial kind signatures. I'm not going to call it NonParametric becuase I think that's a terrible name. Here's the strategy.

1. Sort the declarations into strongly-connected components. No special treatment for CUSKs.
1. For each declaration, extend the environment with a kind binding that has a forall for each explicit user-written kind variable, but meta-kind variables otherwise. For example
      data Foo (a :: k1 -> k1) b c = ...

would get a kind binding
      Foo :: forall k1. (k1->k1) -> kappa1 -> kappa2 -> *

Our earlier example would give
      T :: forall k. k -> (k->*) -> *
S :: kappa3 -> kappa4 -> kappa5 -> *

1. Kind-check the declartions in this environment. At a call of Foo, say, we'd instantiate the forall k1 with a fresh meta-kind variable, but would share kappa1, kappa2 among all calls to Foo.
1. Default any unconstrained meta kind variables to *

That's it! No generalisation step. The only polymorphism is that declared by the user.

So our earlier S/T example would be rejected because it relies on S being polymorphic in its third parameter. If you want the S/T example to work you could write

   data S f (a::k1) (b::k2) = MkS (T a f) (S f a b)
data T (a::k) f where
MkT :: f a -> S f a Maybe -> S f a Int -> T a f

     S :: forall k1 k2. ...blah...
T :: forall k. ...blah...

## Type signatures

Another place that we currently (i.e. using (BASELINE)) do kind generalisation is in type signatures. If you write

f :: m a -> m a
f = ...

then the type signature is kind-generalised thus:

This user-written signature
f :: m a -> m a
means this (BASELINE)
f :: forall k (a:k) (m:k->*). m a -> m a

And f's RHS had better be that polymorphic.

Under (RICHARD) it would be consistent to say this:

This user-written signature
f :: m a -> m a
means this (RICHARD)
f :: forall (a:*) (m:k->*). m a -> m a

If you want the kind-polymorphic one, you'd have to write thus

This user-written signature
f :: forall k (a:k) (m:k->*). m a -> m a
means this (RICHARD)
f :: forall k (a:k) (m:k->*). m a -> m a

## Declarative typing rules

Happily (RICHARD) has a nice declarative typing rule.

Here is what the conventional declarative typing rule, in the absence of polymorphism for a single self-recursive function looks like:

        G, f:t |- e:t
G, f:t |- b:t'
---------------------------
G |- letrec f = e in b : t'

Here the "t" is a monotype (no foralls) that the declarative typing rules clairvoyantly conjures up out of thin air.

Once you add Hindley-Milner style polymorphism, the rule gets a bit more complicated

        G, f:t |- e:t
G, f:gen(G,t) |- b:t'
---------------------------
G |- letrec f = e in b : t'

where 'gen' is generalising.

The (RICHARD) rule might look like this:

        t = forall vs. sig[t1..tn/_]
G, f : t |- e : forall vs.t
G, f : t |- b:t'
---------------------------
G |- letrec f :: forall vs. sig; f = e in b : t'

Here I'm expressing the user-specified knowledge as a signature forall vs.sig, with '_' for bits you don't want to specify.

       f :: forall a. _ -> a -> _

Then the rule intantiates each '_' with a clairvoyantly guessed monotype (which might mention the 'vs', or 'a' in this example), and off you go.

## Reflection

I think we could reasonably switch to (RICHARD) throughout.

As Richard's comments in TcHsType point out, we don't want maximal polymorphism. His example is:

    type family F a where
F Int = Bool
F Bool = Char

We could generate

   F :: forall k1 k2. k1 -> k2

so that (F Maybe) is well-kinded, but stuck. But that's probably not what we want. It would be better to get F :: * -> *

    type family G a f b where
G Int  f b = f b
G Bool f b = Char -> f b

You could just about argue that the programmer intends

   F :: forall k. * -> (k->*) -> k -> *

It's quite similar to this:

  data PT f a = MkPT (f a)

which today, using (BASELINE), we infer to have kind

  PT :: forall k. (k->*) -> k -> *

But I'd be perfectly happy if PT got a monomorphic inferred kind, which is what (RICHARD) would do:

  PT :: (*->*) -> * -> *

If you want the poly-kinded PT, use a signature:

  -- Any of these would do
data PT f             (a :: k) = MkPT (f a)
data PT (f :: k -> *) a        = MkPT (f a)
data PT (f :: k -> *) (a :: k) = MkPT (f a)

One oddity is that we'd do (BASELINE) for terms and (RICHARD) for types. But perhaps that's ok. They are different.

• Terms ought to be as polymorphic as possible but arguably not types. Examples above. Also, since kind polymorphism is still in its infancy, maybe it's no bad thing if all kind polymorphism is explicitly signalled every time a kind-polymorphic binder is introduced.
• Terms have well-established separate type signatures, but we don't have a syntax for separate kind signatures of types and classes.

If we moved from (BASELINE) to (RICHARD), some programs that work now would fail:

• the original S/T example above
• a data type like PT where the user did actually want the kind-polymorphic version.

But that might be a price worth paying for the simplicity, uniformity, and predictability you'd get in exchange.

Last edited 18 months ago by simonpj (previous) (diff)

### comment:4 Changed 18 months ago by ekmett

Just a thought, in our compiler for Ermine we use a strategy very close to Mark P Jones' strategy with CUSKs.

However when we have a type that is not fully what you'd call a CUSK because at least one of the type variables are unannotated we actually allow it to participate in a binding group SCC like any other type.

We instantiate just those unannotated positions in the type with fresh kind variables not all.

Then we run through the binding group checking subsumption for each, letting those checks accrete constraints on the unannotated types before we generalize over the whole SCC.

A universe level down the code looks like:

At the kind level the code is in a local branch and I'll push it out to github soon.

This lets us fit somewhere in the middle between Mark P Jones' strategy and Richard's.

Unannotated variables participate in cycles and unify out to whatever they must, while kind variables supplied explicitly annotated types can't be forced to unify with them without yielding skolem escapes.

The rule then becomes that if you annotate some types with a kind involving explicit kind variable in a class declaration all kinds that unify with that kind variable will need to be annotated, but other kinds can be left untouched.

In exchange you don't get more specific kinds than you ask for #9201, we can handle partially annotated polymorphic recursion like occurs here, and existing code so long as it doesn't rely on #9201 would still typecheck.

### comment:5 Changed 18 months ago by goldfire

I think Simon got one key detail in (RICHARD) wrong: I do propose to generalize after kind-checking all the declarations, not defaulting to *.

The way I see it is this: there is "good" polymorphism and "bad" polymorphism.

Here is "good":

type family IsJust x where
IsJust Nothing = False
IsJust (Just x) = True

Without any annotation, I would want to infer forall k. Maybe k -> * as the kind for IsJust. This goes against Simon's conclusion that all kind polymorphism should be annotated. I actually would argue that the genie about this sort of polymorphism is out of the bottle, and that Simon's proposal would be too big a breaking change.

type family F x where
F Bool = True
F Maybe = False

It is perfectly reasonable to infer forall k. k -> * for the kind of F. Indeed, this could even be implemented without too much trouble. (I think I did implement this behavior along the way to the current behavior for closed type families!) But, I think most users would prefer to get a kind error in this case. If they want this polymorphism, use an annotation.

What's the difference between "good" and "bad" polymorphism? "Good" is parametric and "bad" is non-parametric. Hence the name NonParametricKinds.

The examples above come from type families. Extending these ideas to datatypes is awkward because datatypes don't (currently) support kind-indexing (essentially, being GADT-like in kind parameters) in the right way. The closest we can really get is to think about polymorphic recursion, which is where this all started. Thus, in the context of datatypes and classes, I agree that the name NonParametricKinds is bogus.

What this all leads to is this: we want to allow "good" polymorphism without an annotation but to allow "bad" polymorphism only if specifically requested. This is exactly the story with closed type families today. And, if I'm understanding all the details correctly, in the datatype/class world, this means that we get non-polymorphic recursion to work all the time, but polymorphic recursion only when requested. After all, if you cross your eyes, polymorphic recursion can look a little like non-parametric polymorphism: both are cases when a type parameter is used inconsistently in a definition.

I think the strategy I'm outlining is not unlike the behavior Edward describes in Ermine. The only difference I can spot is that my strategy allows unification variables to unify with skolems, where Ermine's seems to avoid this. For example:

type family G x (y :: k) :: Constraint where
G x y = (x ~ y)

Here, the kind of x must be k, but that's acceptable. Would that fail in Ermine? I could certainly see that failure here could be reasonable.

As a small aside, I wonder how any of this interacts with the coming partial type signatures at the term level. How do those interact with polymorphic recursion?

### comment:6 Changed 18 months ago by ekmett

Currently we'd reject that, but if you can come up with a story that allows it I'd happily switch.

We can (and do) use it for partial type signatures by combining it with HMF style "some" annotations, but since we disallow the partial types from referencing the quantified ones (since some can only occur in an Annot, outside of the type) it is perhaps less useful than a design that can do what you want could be.

### comment:7 Changed 18 months ago by goldfire

What's insufficient about the algorithm I've described here? The G above is accepted by today's GHC. I don't see where a skolem escape would fail.

### comment:8 Changed 18 months ago by dolio

Ermine's algorithm for this effectively has an additional quantifier, some. Your G definition is effectively equivalent to:

u : a -> a -> T

g : some a. forall b. a -> b -> T
g x y = u x y

'some' is effectively a quantifier for unification variables. So for instance, if I wrote:

h : some a b. a -> b -> T
h x y = u x y

checking would succeed, with h : a -> a -> T. Also, some cannot occur arbitrarily in a type. It can only occur outer-most in a type ascription.

The reason ermine rejects g right now is that the metavariable a is at an outer level of binding. They cannot be generalized over until the entire SCC is done being checked, while g is expecting to be polymorphic in b. This is the kind of check that would fail for an example like:

g : some a. forall b. a -> b -> T
g x y = h x y

h y x = g x y

We could try to be more intelligent, and do additional generalization as long as skolems wouldn't flow into other types in the binding group, or something, but we haven't gotten that fancy yet.

### comment:9 Changed 18 months ago by dolio

Having thought about this some, I realized that there's no reason to fail due to skolems 'escaping' into other types of the binding group, since we're about to generalize all the types anyway. So I've tweaked our algorithm to not care about that. Now the equivalent of your G example checks, and so does my example above:

g : some a. forall b. a -> b -> T
g x y = h x y
h y x = g x y

yields:

g : forall b. b -> b -> T
h : forall b. b -> b -> T

This seems sensible to me, and sounds like your proposal.

### comment:10 Changed 18 months ago by simonpj

• I'm afraid that I do not understand how you distinguish "good" from "bad" polymorphism. Examples are not enough!
• I'm afraid I do understand Ermine's algorithm.

Could I ask you to write a section on the wiki page that describes as clearly, as you possibly can, the designs you have in mind? That would make sure we are all talking about the same thing.

By the same token, if you don't understand anything in the designs I have described there, please say so and I'll clarify.

I'm adding Stephanie and Dimitrios in cc

Simon

### comment:11 Changed 18 months ago by goldfire

Added some comments (delineated with Richard: ... End Richard) to the wiki page. I believe the (PARGEN) option you describe there agrees with my proposal. I also believe that my proposed algorithm now (with dolio's changes to Ermine) matches Ermine's.

### comment:12 Changed 18 months ago by dolio

Having thought some more, I feel like there is potential weirdness with the changes I mentioned earlier, even if it works nicely for some simple examples. For instance, consider:

u : a -> a -> a

f : some a b. a -> a -> b
f x y = u (g x y) (h x y)

g : some c b. forall a. c -> a -> b
g x y = f x y

h : some c b. forall a. c -> a -> b
h x y = f x y

Now, since f takes two arguments of the same type, this requires each of g and h to do the same. But, to ensure g and h are sufficiently polymorphic, we need to skolemize. These skolems then flow into the c unification variables, which in turn are unified due to f. So this will cause a skolem mismatch.

So, I'm not sure it's a good idea for these sorts of examples to work, even if they could in some cases. It seems like it could easily be confusing when similar examples happen to work or not work depending on where skolems flow. So I guess I'm back to thinking that it's better for your G example to not check:

u : a -> a -> T

g : some c. forall k. c -> k -> T
g x y = u x y

simply because it's due to a less confusing rule.

Ermine has, of course, always generalized unification variables that are still free after this process; that is what is expected for types. I think it's handy for kinds as well (probably excepting the 'bad polymorophism' examples).

### comment:13 Changed 18 months ago by dolio

Having conferred with Ed, I guess GHC uses a different strategy that doesn't involve (proper) skolem variables, so it might not be subject to my complaint. Using some kind of after-the-fact distinctness check instead of proper skolems seems not to arbitrarily rule out certain definitions in a confusing manner, which was my main concern.

### comment:14 Changed 18 months ago by simonpj

Richard, I have tried to address your questions on the wiki page. Better now?

I still don't know what the difference between bad and good polymorphism is, but maybe it doesn't matter now, since you say that it is "tangential".

You say "Because open type families do not have a body, they would still need their own kind inference story, where unconstrained meta-variables default to *." but I don't understand that. Add a subsection for it? (Open type families simply have their own, complete, kind signature, no?

I'm happy with (PARGEN) if you are happy with the typing rule including the side condition.

Simon

### comment:15 Changed 18 months ago by goldfire

Happily, I think everyone here has converged on (PARGEN) with the critical side condition that we do not unify a meta-variable with a kind containing a skolem. I realized yesterday that the side condition was necessary but didn't have the chance to write it up.

In any case, I think we can end the design phase here and move onto the implementation phase. Most of (PARGEN) should be easy, as (PARGEN) is exactly what is implemented by NonParametricKinds, except for the side condition. To implement the side condition, I propose a new disjunct for MetaInfo named NonSkolemTv which is like TauTv but cannot unify with a type containing a skolem. The unifier, in TcUnify, would just check this condition at the appropriate point. Sound reasonable?

### comment:16 Changed 18 months ago by goldfire

And, yes, open type families keep their complete kind signature.

### comment:17 Changed 18 months ago by simonpj

I'm not quite ready to declare victory. Some technical questions:

• See T1a and T4 under (PARGEN). These are unexpected failures. The tricky side condition means that you must declare all the polymorphism involving k, or none, but nothing in between.
• What is the rule for non-recursive bindings? Specifically:
data NR f (a::k) = MkNR (f a)

Is this accepted (as now), or rejected by the "tricky side condition". If the former that gives an uncomfortable difference between recursive and non-recursive bindings.
• I'd like to see a rule written down for closed type families, and a sketch of the accompanying algorithm.

And finally, at a non-technical level, I'm not convinced that (PARTIAL) is untenable.

• Yes, people using kind polymorphism might need to add some kind signatures, but that would arguably improve their code.
• We could issue a warning for one release cycle.
• The tricky side condition becomes simple: all kind polymorphism must be declared.
• And sometimes kind polymorphism might even trip you up:
foo :: forall f a. f a -> f a
foo = ...
where
g :: f Int -> Int

This will, I think, fail. Because foo's signature actually means
foo :: forall k. forall (f:k->*) (a:k). f a -> f a

so the (f Int) application is ill-kinded.

Edward is an example of a high-end kind-polymorphism user. How bad would (PARTIAL) be?

Implementation. Re NonSkolemTv, I'd hate to pollute MetaInfo for such a corner case. We can simply test the side condition at the end, just as the rule suggests. Generating a helpful error message is quite a challenge!

### comment:18 Changed 18 months ago by goldfire

• I agree that (PARGEN) is a breaking change. But, I'll quote Simon's comment from the wiki page, which I fully agree with:

So moving from (BASELINE) to (PARGEN) would be a breaking change, but only in rather obscure circumstances. I am intensely relaxed about that particular backward-compatibility problem!

• Non-recursive bindings should behave the same as recursive ones. This means that NR would be rejected due to the side condition.

## Closed type families

(PARGEN) (including the side condition) should work out just fine. Here would be the declarative typing rule:

k2 = forall fkv(k1). k1[k'1 .. k'n/_]
fkv(k1) \not\in k'j
forall i: G, F:k2 |- (F ps_i = t_i) ok
k3 = gen(G, k2)
---------------------------------------------------
G |- type family F :: k1 where { F ps_i = t_i } : k3

This is very similar to the declarative typing rule for letrec given on the wiki page. Here, I am ignoring issues with arity/saturation and using a syntax where the kind signature of a type family is given as k1 with blanks, instead of the tyvarbndr syntax used in source code.

This is in fact an improvement over the current state of affairs, which is essentially this rule without the side condition. Because of the omitted side condition, we don't have principal types! For example,

type family X (a :: k) where
X True = False

X could be X :: k -> k or X :: k -> Bool. Neither is more general than the other. GHC chooses X :: k -> Bool, but it's not principled. This is what I get for implementing kind inference for closed type families without writing out declarative rules! In any case, the solution to this problem (closed type families) seems to be the same as the solution for datatypes and classes, quite happily: add the side condition.

## Using (PARTIAL)

I'm still quite strongly against (PARTIAL). Let's ignore the backward compatibility problem, for now. With (PARTIAL), we have a very different story about kind polymorphism than we do about type polymorphism. GHC tries to be as polymorphic as possible with types: writing foo x = x gives foo :: forall a. a -> a, not foo : () -> (). It seems very odd to me to not do the same in kinds. Yet, (PARTIAL) would say that data Foo x = MkFoo (Foo x) would get Foo :: * -> * instead of Foo :: forall k. k -> k. Especially as we're inching toward dependent types, this seems like a step backward.

And, though I defer to Edward's experience, I tend to think the backward compatibility problem would be annoying for what may seem like a dubious benefit (polymorphic recursion in the presence of partial kind signatures).

## Conclusion

I am worried that (PARGEN) has a strange surface area, and I think that any error messages that the side condition produces should include a URL for further reading. (I actually think that links to further reading would helpful in several error messages!) But, if this surface area is deemed too bumpy, I personally would prefer to go back to (BASELINE) than to go to (PARTIAL).

### comment:19 Changed 18 months ago by goldfire

Hold the phone! This is all wrong!

## Interaction with partial type signatures

I just ended a great discussion with Iavor and with David Darais about this whole issue, and we came to the conclusion that (PARGEN) is a bad idea. The problem isn't that (PARGEN) doesn't work (I still think it does work) but that it paints us into a corner.

We looked at PartialTypeSignatures, which describes an upcoming feature to allow wildcards in type signatures of terms, in case the programmer does not want to write down an entire type. With partial type signatures, wildcards can unify with lexically-quantified variables, contrary to the side condition debated in this ticket. And, the feature looks useful, as types get more complicated and the burden of writing out a full signature increases.

There is no discussion (that I saw) of polymorphic recursion w.r.t. partial type signatures, so I don't know what the term-level plan is on that issue.

## A change of heart

Looking at all of this (now back at the type level), I see that we have two, mutually exclusive options: 1) Allow polymorphic recursion in the presence of a partial kind signature via (PARGEN) + side condition. 2) Allow more flexible partial kind signatures.

I think (2) is of greater benefit to users than is (1). As a further bonus, (2) is much simpler than (1) -- indeed, it is what we have today.

## A new proposal

Thus, I propose a radically different solution to the original problem: come up with a syntax for a CUSK for classes. Call this proposal (NEWCUSK). Specifically:

A class or datatype is said to have a CUSK if and only if all of its type variables are annotated. Otherwise, like (BASELINE).

As with (BASELINE), polymorphic recursion is possible only in the presence of a CUSK. Under (NEWCUSK), Edward's original example will not work, but adding an annotation to a (presumably, (a :: k2)) would make it work.

(NEWCUSK) means that a declaration like data Foo a b :: * will not have a CUSK. This would be a breaking change if a programmer used :: * to force other variables to have kind * and/or used polymorphic recursion. Note that in the case where a user puts the :: right after the datatype name, there are no type variables, so every one is vacuously annotated -- no breakage here.

If we are opposed to making this breaking change, the (NEWCUSK) proposal still works while also having a top-level :: indicate a CUSK. I just think that the top-level :: syntax is a strange bump in the language design. (Though, to be fair, I couldn't think of something better at the time.)

In continuing to think about all this, I have come to realize that (PARGEN) is quite strange, indeed. Let's consider some more familiar territory:

data G a where
GBool :: G Bool

foo GBool = True

GHC rightly rejects the code above saying, essentially, that foo does not have a principal type. foo :: G a -> a and foo :: G a -> Bool are both very reasonable candidates and are not comparable. (The error message, of course, discusses untouchables... but it's really talking about principal types.)

But, if we apply the (PARGEN) philosophy to type-checking GADT pattern-matches, we would decide that foo :: G a -> Bool is the principal type. This is because the (PARGEN) philosophy would say to prevent the inferred result type from mentioning any type variables refined in the pattern match. I am playing a little fast and loose here talking about the un-articulated "(PARGEN) philosophy", but I'm hoping readers can understand my concern. A perhaps tighter way of saying this is: I conjecture that the over-permissiveness of the type system in Fig. 10 (p. 25) of OutsideIn (as discussed in Sec. 4.4) might be fixed by adding a side condition to the Case rule, essentially saying that any type variables refined in a local equality assumption cannot then appear in other types discovered by using constraints generated by the case. To make this meaningful, the type system would have to be re-written in a bidirectional manner, so we can know which types come "from" the case vs. which types go "to" the case. I leave the exact formulation as future work, but I'd be very curious to read a response to this conjecture.

## Conclusion

What do others think of (NEWCUSK) and the points I've brought up here? It seems to solve the original problem (no polymorphic recursion available in classes) while not upsetting too much else. And, it seems to have nicer theoretical properties and is easier to explain to users.

### comment:20 Changed 18 months ago by dolio

This example:

foo :: forall f a. f a -> f a
foo = ...
where
g :: f Int -> Int

just seems like bad policy to me. The top signature is a partial signature, the missing pieces (the kinds) should be solved, and it is not sufficient to only look at the signature of foo to do that solving. I can construct similar examples in Ermine, although it is a bit convoluted due to our currently meager tooling:

:type
let { f : forall f a. f a -> f a
; f x = x
} in f

forall {k} (f : k -> *) (a : k). f a -> f a

:type
let { f : forall f a. f a -> f a
; f x = x where
{ z = g x
; g : some f a b. f a -> f b -> b
; g _ _ = ""
}
} in f

forall (f : * -> *) (a : *). f a -> f a

Effectively, this signature is the same as (for us)

some k1 k2. forall (f : k1) (a : k2). f a -> f a

although we don't currently handle some-bound kinds; unspecified kinds act similarly, though.

The problem with this example seems to be deciding on things too early, not generalizing. For instance, doesn't PARTIAL error if you apply the same kind of policy to:

foo :: forall f a. f a -> f a
foo = ...
where
g :: f Maybe -> f Maybe

f will be defaulted to * -> *, but that is wrong for application to Maybe.

### comment:21 Changed 18 months ago by simonpj

OK, so (NEWCUSK) is precisely (BASELINE) with a slightly expanded definition of CUSK (c.f. the current definition in the user manual). I'm all for that; I quite liked (BASELINE): it's pretty simple and lines up precisely with the term-level story (a la Mark Jones).

Just to check, though, let's be sure we agree:

data T1 f a = MkT1 (f a)
-- No CUSK
-- Gets T1 :: forall k. (k->*) -> k -> *
-- The generalisation takes place in the third bullet of step 3 of (BASELINE)

data T2 a b :: *    -- Presumably a nullary data type
-- No CUSK
-- Gets T2 :: forall k1 k2. k1 -> k2 -> *
-- Very similar to T1

I have no idea what you mean by "2) Allow more flexible partial kind signatures" in comment:19.

Could you update the wiki page with:

• (NEWCUSK) (= (BASELINE) + revised defn of CUSK)
• the typing rules for closed type families

Thanks!

Simon

### comment:22 Changed 18 months ago by goldfire

By "2) Allow more flexible partial kind signatures", I meant that, under (NEWCUSK), the kind of un-annotated type variables can unify with lexically-scoped kind variables, allowing the following to type-check:

data Q f (a :: k) where
MkQ :: f a -> Q f a
-- fails under (PARTIAL) and (PARGEN)
-- succeeds under (BASELINE) and (NEWCUSK)

If partial type signatures on terms are so useful (and I think they will be), then partial kind signatures, like the one on Q, would be, too.

Yes, I am agreed with the examples in comment:21.

(NEWCUSK) description was already on wiki page, and I have now added rules for closed type families. These rules are a breaking change from today's closed type families, but a "good" breakage, in that it tightens up the specification from the current wonky state of affairs. See the example from comment:18, which would no longer type-check.

### comment:23 follow-up: ↓ 24 Changed 18 months ago by dolio

I don't have a particular dislike for NEWCUSK, I think. Anything that allows you to do polymorphic recursion with sufficient annotation is at least tolerable.

However, I don't really understand what the problem with PARGEN is that caused the added restrictions that make it less desirable. Is the entire problem closed, partially annotated type families that are non-parametric, and therefore act like GADT definitions and lack principal types? And is the motivation to then have a uniform rule for both these and everything else that doesn't require detecting situations that would fail to have a principal type?

You (goldfire) and I discussed what we're doing in Ermine, which is now quite a lot like the (original) PARGEN strategy. It seems to work for the sort of partially specified type signatures we have, and it works for polymorphic recursion, including polymorphic recursion with partial signatures. For instance:

let { u : a -> a -> a
; u x _ = x
; f : some b c. forall a. a -> b -> c
; f x y = let { z = u x y } in g x y
; g _ y = f () y
} in f

Without the signature on f the inferred type is () -> () -> c, but with it the inferred type is b -> b -> c.

Anyhow, I'm not particularly adamant about your choice of (original) PARGEN vs. NEWCUSK. But I'd like to understand what exactly the objections were, and whether they're tied to GADTs and type families.

### comment:24 in reply to: ↑ 23 Changed 18 months ago by goldfire

Is the entire problem closed, partially annotated type families that are non-parametric, and therefore act like GADT definitions and lack principal types?

Not just these. Also partially annotated datatypes and classes will lack principal kinds. Here is the example:

data W f (a :: k) where
MkW :: W Maybe Int -> W f a

Do we have W :: (k -> *) -> k -> * or W :: (* -> *) -> k -> *, among others? Both seem reasonable, though the latter is certainly easier to infer. To eliminate ambiguity, we have to add the restriction to (PARGEN). This makes it clear that the second kind is the only allowable one.

And is the motivation to then have a uniform rule for both these and everything else that doesn't require detecting situations that would fail to have a principal type?

Yes, that's my understanding.

You (goldfire) and I discussed what we're doing in Ermine, which is now quite a lot like the (original) PARGEN strategy.

From my understanding, your original implementation was like (PARGEN) + side condition. Only after discussing did you (effectively) remove the side condition.

It seems to work for the sort of partially specified type signatures we have, and it works for polymorphic recursion, including polymorphic recursion with partial signatures. For instance:

let { u : a -> a -> a
; u x _ = x
; f : some b c. forall a. a -> b -> c
; f x y = let { z = u x y } in g x y
; g _ y = f () y
} in f

Without the signature on f the inferred type is () -> () -> c, but with it the inferred type is b -> b -> c.

I believe the original (PARGEN) "works", in that it is sound, for an appropriate definition of sound. However, it can infer non-principal types, which seems bad. I don't think it's very wrong for Ermine to adopt (PARGEN) - side condition, but I have to say I don't think it's very right, either.

I believe that the example you give has a principal type, which is inferred correctly.

Anyhow, I'm not particularly adamant about your choice of (original) PARGEN vs. NEWCUSK. But I'd like to understand what exactly the objections were, and whether they're tied to GADTs and type families.

I would say that the problems are wholly independent of GADTs and type families. There is a problem with closed type families that is closely related, but the fundamental problem is independent.

### comment:25 Changed 18 months ago by dolio

This example:

data W f (a :: k) where
MkW :: W Maybe Int -> W f a

is just another Milner-Mycroft problem. The inferred kind is (* -> *) -> k -> *.

The principal kind is k0 -> k -> *, but it can't be inferred. Just like

data W f a = W (W Maybe Int)

will have inferred kind (* -> *) -> * -> *, even though k0 -> k -> * is valid and strictly more general.

From my understanding, your original implementation was like (PARGEN) + side condition. Only after discussing did you (effectively) remove the side condition.

Yes, but this is because we were using skolem variables, which can lead to confusing rejection of partially annotated mutual definitions. When we started basing our algorithm on something closer to GHC, using what I think you called SigTvs, plus a per-signature distinctness check, that objection was no longer valid.

I believe the original (PARGEN) "works", in that it is sound, for an appropriate definition of sound. However, it can infer non-principal types, which seems bad.

Hindley-Milner infers non-principal types (so does GHC, of course).

I don't think it's very wrong for Ermine to adopt (PARGEN) - side condition, but I have to say I don't think it's very right, either.

I still don't think we have an example that doesn't involve GADTs or type families.

### comment:26 Changed 18 months ago by simonpj

I have edited the wiki page so that the beginning part says what we actually plan to do. See if you agree with it.

Simon

### comment:27 Changed 17 months ago by goldfire

• Owner set to goldfire

Agreed. I'll fix this soon.

### comment:28 Changed 16 months ago by simonpj

On Tuesday I promised Richard I'd write up the two variations of our proposed consensus, on the wiki page. I have now done so.

A couple of questions labelled Simon are in the text. Over to Richard.

Simon

Simon

### comment:31 Changed 16 months ago by simonpj

Responses from Simion

### comment:32 Changed 16 months ago by goldfire

Response from Richard.

### comment:33 Changed 16 months ago by simonpj

Simon: I agree that, since type syononyms can't be recursive except via a data type, if you use "A possible variation" below, then you can get away with saying that type synonyms cannot have CUSKs. It seems a bit non-orthogonal; and could occasionally be tiresome. Imagine

data T1 a b c = ...S...
data T2 p q r = ...S...
data T3 x y q = ...S...
type S f g h = ...T1...T2...T3...

Then, since you can't decorate S with a CUSK, you might need to annotate all of T1, T2 and T3 with CUSKs.

It would not be hard to say what a CUSK for a type synonym was: just wrap the whole RHS in a kind signature:

type T (a::k1) (b::k1->k2) = b a :: k2

I think I'd argue mildy for that, just to make the design orthogonal.

### comment:34 Changed 16 months ago by goldfire

type S (a :: k) = Proxy (T (Just a))
data T a = MkT (S a)

Does that S have a CUSK? If it does, the code should be accepted, I think. Or, would a user have to put in a totally-superfluous :: * at the end of S's RHS? Regardless of the kind of T, a proxy is always in kind *.

### comment:35 Changed 16 months ago by simonpj

Is it ok to remove the para about "non-parametric" equations?

Re your question, no that S doesn't have a CUSK, any more than

data T a b = MkT (T a b) a b

does. It's "obvious" that S's RHS has kind *, but only because you have mentally done kind inference on S's right hand side.

Of course, the example you give would be accepted in fact. Neither has a CUSK, but normal inference and generalisation suffices. There is no polymorphic recursion.

Simon

### comment:36 Changed 16 months ago by goldfire

OK. wiki page updated, including type synonym CUSKs as described. I still find that a little wonky, but just in the concrete syntax, not the semantics.

For what it's worth, my example in comment:34 does seem to require at least one CUSK -- at least, it does in 7.8.

In any case, I think we're in agreement here about what to do, no?

### comment:37 Changed 16 months ago by simonpj

Yes, I think we're in agreement. Over to you when you have a moment.

Simon

### comment:38 Changed 16 months ago by Richard Eisenberg <eir@…>

Test #9200. (polykinds/T9200)

### comment:39 Changed 16 months ago by Richard Eisenberg <eir@…>

Change definition of CUSK for data and class definitions (#9200).

Now, a CUSK is when (and only when) all type variables are annotated.
This allows classes to participate in polymorphic recursion.

### comment:40 Changed 16 months ago by Richard Eisenberg <eir@…>

Added more testing for #9200. (polykinds/T9200b)

### comment:41 Changed 16 months ago by Richard Eisenberg <eir@…>

Change treatment of CUSKs for synonyms and families (#9200).

### comment:42 Changed 16 months ago by Richard Eisenberg <eir@…>

Remove NonParametricKinds (#9200)

This commit also removes 'KindCheckingStrategy' and related gubbins,
instead including the notion of a CUSK into HsDecls.

### comment:43 Changed 16 months ago by Richard Eisenberg <eir@…>

Update manual (#9200).

### comment:44 Changed 16 months ago by Richard Eisenberg <eir@…>

Testsuite wibbles around #9200

### comment:45 Changed 16 months ago by goldfire

• Milestone set to 7.10.1
• Resolution set to fixed
• Status changed from new to closed
• Test Case set to polykinds/T9200 polykinds/T9200b

The above patches implement much of what was discussed here. They do not implement the "possible variation" part from the wiki page, as I ran out of time and the plumbing became a little challenging. See ticket #9427 to track the implementation of that piece.

This is a user-facing, breaking change (in obscure circumstances) and should not be merged for 7.8.4.

### comment:46 Changed 12 months ago by Richard Eisenberg <eir@…>

Test #9151 in typecheck/should_compile/T9151.

This test case should pass right now -- the bug is fixed,
presumably by #9200.
Note: See TracTickets for help on using tickets.


text:
# Regression with Logistic-Distribution errors (NOT Logistic Regression)

I was wondering if anyone ever tried to do a regression where the errors, instead of normal, would be assumed to be from the Logistic Distribution.

I don't mean Logistic Regression, as I don't assume that the $$y$$'s are coming from a Bernoulli distribution whose mean is dependent on some covariates, but rather that the $$y$$'s come from a symmetric Logistic distribution, whose pdf is:

$$f_Y(y;\mu) = \frac{e^{(y-\mu)}}{(1+e^{(y-\mu)})^2},\,\,-\infty\lt y\lt \infty$$

(Unless the models are some how equivalent and I missed that)

Yes, I have done this. You can trick the "survreg" function in the "survival" package of R into doing it by assigning all the censoring values to "1" (uncensored) and then requesting the logistic distribution. Here is an example.

library(survival)

n= 1000
set.seed(12345)
x = rnorm(n)
y = 2 + 5*x + rnorm(n)
observed = rep(1,n)

fit.normal   = survreg(Surv(y, observed) ~ x, dist = "gaussian")
fit.logistic = survreg(Surv(y, observed) ~ x, dist = "logistic")
summary(fit.normal)
summary(fit.logistic)

The normal model fits better here (Log Likelihood = -1426 vs. -1436.9 for logistic), which is not surprising since the data are generated from the normal model.

• cool, I have done so numerically now in python. Do you know if there's any benefits of doing so? Any papers/etc. ? – Maverick Meerkat Feb 22 at 15:20
• This is a good answer, but I find it slightly surprising you demonstrate it by using rnorm() to generate your errors instead of rlogis(). – gung - Reinstate Monica Feb 22 at 15:31
• There is a lesson either way. Exercise for the reader. – BigBendRegion Feb 22 at 15:34

I've done so now, check Numerical implementation in Python (Jupyter Notebook).

Can't say that there's much difference from fitting a regression to it vs. a normal regression. I also tried with different scale parameter, and both regressions seem to be quite close (though of course the log-likelihood is slightly better for the Logistic which generated the data).

So maybe there is no necessity for it, as normal regression fits just as good, and is easier to compute.


text:
library(logrx)

The purpose of the logrx package is to generate a log upon execution of an R script which enables traceability and reproducibility of the executed code.

## Log attributes

The following attributes are recorded in the log:

• metadata: The logrx package information
• user and file information: The user that generates the log, file name and path of the R script
• session_info: The R session information
• packages: List all available packages in the environment
• external_software" Lists all external software
• masked_functions: The functions masked by packages
• start_time, end_time, and run_time: The start, end, and run times
• used_packages_functions: Any packages and functions used in the R script
• unapproved_packages_functions: Any packages and functions used in the R script that are not part of that approved packages and functions list
• errors: The errors generated when running the R script
• warnings: The warnings generated when running the R script
• messages: The messages generated when running the R script
• result: The result generated when running the R script
• output: The output generated when running the R script
• log_name, log_path: The name and path of the log

## Generating a log

The log can be generated according in two ways:

• Using the axecute() function

• Using the log_*() functions

### axecute()

axecute() enables the command line submission of a program. A log is set-up around the program, and its code is run safely and loudly (using safely() from the purrr package).

axecute("my_script.R")

### log_*() functions

Use the log_*() functions:

• log_init() to create the environment log.rx

• log_config() to add the core elements of the log to the environment, and basic elements that are available at the time of configuration

• run_safely_loudly() to execute the program code, and capture errors, warnings, messages, output, and result

• log_write() to generate and format the log

log_config("my_script.R")
run_safely_loudly("my_script.R")
log_write()

## Scripting with logrx

While logrx is built around creating a log for a program it can just as easily be used when running an entire set of programs. The axecute() function has been built with both single file execution and scripted file execution in mind. With the use of simple functions such as lapply() scripting is easy. Below is some sample code of how lapply() can be used with axecute().

lapply(c("file.R", "otherfile.R"), axecute)

If your scripting needs to work on the contents of a directory instead of a pre-defined list, functions such as list.files can be used to obtain a list of files to use. Below is an example of how this can be applied in practice by getting all files ending in ‘.R’ in the current working directory using a regular expression, and then using lapply() to run the files using axecute().

r_script_list <- list.files(path = ".", pattern = "\\.R\$")
lapply(r_script_list, axecute)


text:
Thank you for visiting nature.com. You are using a browser version with limited support for CSS. To obtain the best experience, we recommend you use a more up to date browser (or turn off compatibility mode in Internet Explorer). In the meantime, to ensure continued support, we are displaying the site without styles and JavaScript.

# Giant phonon anomalies in the proximate Kitaev quantum spin liquid α-RuCl3

## Abstract

The Kitaev quantum spin liquid epitomizes an entangled topological state, for which two flavors of fractionalized low-energy excitations are predicted: the itinerant Majorana fermion and the Z2 gauge flux. It was proposed recently that fingerprints of fractional excitations are encoded in the phonon spectra of Kitaev quantum spin liquids through a novel fractional-excitation-phonon coupling. Here, we detect anomalous phonon effects in α-RuCl3 using inelastic X-ray scattering with meV resolution. At high temperature, we discover interlaced optical phonons intercepting a transverse acoustic phonon between 3 and 7 meV. Upon decreasing temperature, the optical phonons display a large intensity enhancement near the Kitaev energy, JK~8 meV, that coincides with a giant acoustic phonon softening near the Z2 gauge flux energy scale. These phonon anomalies signify the coupling of phonon and Kitaev magnetic excitations in α-RuCl3 and demonstrates a proof-of-principle method to detect anomalous excitations in topological quantum materials.

## Introduction

In correlated quantum materials, the nature of electronic interactions and their ground state topology is intimately linked to the geometry of the underlying lattice1,2,3,4,5,6. The low-energy excitations arising from pure electronic degrees of freedom inevitably interact with the crystal lattice, leaving behind their fingerprints in the phonon spectrum. Hitherto, the interactions of phonons with “conventional” quasiparticles of either Bose–Einstein or Fermi–Dirac statistics, such as magnons in magnets7, phasons and amplitudons in density waves8,9,10 and Bogoliubons in superconductors11, have been explored extensively. In contrast, the coupling between phonons and fractional excitations, including spinons in one-dimensional magnets1,2,3,12,13,14,15, and Majorana fermions (MFs) and Z2 gauge fluxes that are thought to exist in the Kitaev quantum spin liquids (QSL)16,17,18,19,20,21,22,23,24,25, have remained elusive. The discovery of such fractional-excitation-phonon coupling (FPC) is of fundamental importance, as they carry key information of the intertwined quantum state12,13,14,15. In particular, the coupling of phonons to the itinerant MFs has been predicted to play a pivotal role in the realization of the field-induced quantum thermal Hall effect in α-RuCl326,27,28,29, which is a signature of quantum entanglement in Kitaev-QSLs30,31,32.

Numerous studies have shown that the low-temperature phase of α-RuCl3 is a promising Kitaev-QSL candidate17,18,19,20,21,22,23,24,30,31,32. As displayed in Fig. 1a, the edge-sharing Ru–Cl octahedra form an effective spin-1/2 honeycomb network. The destructive quantum-interference through the close-to-90° Ru–Cl–Ru bonds significantly suppresses the Heisenberg magnetic exchange interaction, yielding a dominant Ising-type interaction (J) perpendicular to the Ru–Cl–Ru plane33 (Fig. 1b). Figure 1c schematically depicts the phase diagram of α-RuCl3. At zero magnetic field, the low-energy excitations in the paramagnetic phase are primarily determined by the Kitaev term3,4,17,18,19,20,21,22,23,24,30,31,32

$$H=\mathop{\sum}\limits_{\gamma ,\, <\, i,j \,> \, }{J}_{K}^{\,\gamma }{S}_{i}^{\gamma }{S}_{j}^{\gamma }$$
(1)

Here $${J}_{K}^{\,\gamma }\,$$($$\gamma =X,Y,Z$$) is the bond-dependent coupling parameter, and $$< i,j >$$ stands for nearest-neighbor pairs of spins at one of the X, Y, or Z bonds. The two characteristic energy scales are shown in Fig. 1d for the isotropic limit ($${J}_{K}^{\,\gamma }={J}_{K}$$). Below the Kitaev temperature scale $${T}_{k} \sim {J}_{K}$$, the low-energy excitations of Eq. (1) start to fractionalize into itinerant MFs and fluctuating Z2 gauge fluxes34. The former features a continuum that peaks broadly near JK, while the latter is a local excitation with an energy around 0.065 JK16,20,25,34. Below TN = 7 K, non-Kitaev interactions such as remnant Heisenberg magnetic exchange couplings, stabilize zigzag antiferromagnetic order that is suppressed under magnetic field35,36,37,38,39. Above B ~7 T, a quantized thermal Hall conductivity (red region in Fig.1c) is observed, indicating strongly an entangled topological phase30,31,32. However, unlike the quantum Hall effect of electrons, it has been theoretically predicted that the quantum thermal Hall effect can only be approximate and requires strong FPCs26,27,28,29. Here we report experimental signature of the FPC in α-RuCl3 by uncovering two-types of phonon anomalies at zero magnetic field: a 35% enhancement of the phonon spectral weight near the Kitaev energy JK, and a giant phonon softening of ~15% below 2 meV26,27,28,29.

## Results

Figure 2a shows the imaginary part of the dynamical phonon susceptibility $$\chi {\prime\prime} ({\bf{Q}},\omega )$$ along Γ1(6, −3, 0)−M(6, −2.5, 0)−Γ2(6, −2, 0) in reciprocal lattice units (r.l.u.) at room temperature (see Supplementary Note 6 for first-principles calculations of phonon dispersion). The dynamical susceptibility is given by the fluctuation-dissipation theorem via $$\chi {\prime\prime} ({\bf{Q}},\omega )=S({\bf{Q}},\omega )\times (1-{e}^{-\omega /{k}_{B}T})$$, where $$S({\bf{Q}},\omega )$$ is the dynamical phonon structure factor that is directly measured by inelastic x-ray scattering (IXS). The total momentum transfer Q = q + G, is composed of the reduced momentum transfer in the first Brillouin zone q and the reciprocal lattice vector G. The elastic contribution at ω = 0 was subtracted by fitting the IXS raw data in the entire energy window (see Supplementary Note 1 and Note 2). We selectively probe in-plane transverse phonon modes, whose dispersions (open circles and open squares) and sinusoidal fits (dashed curves) are shown in Fig. 2b. As shown in Fig. 2a, the intensity of the transverse acoustic phonon changes significantly from Γ1 to Γ2, reflecting their different Bragg peak intensities that are plotted in Fig. 2c. Two low-energy optical phonons, P1 and P2, are observed at the Brillouin zone center Γ2, corresponding to $${\omega }_{1}=2.7$$ and $${\omega }_{2}=7$$ meV, which are in good agreement with previous optical and neutron studies19,40. The two optical phonons carry opposite phonon velocities and form an interlaced structure that intercepts the acoustic phonon. An apparent phonon crossing occurs between Γ and M (Fig. 2d and e), suggesting possible Dirac-cone and topological phononic nodal-lines41,42.

In α-RuCl3, JK is estimated to be 5–9 meV in the low-temperature phase below 150 K4,17,18,19,20,21,22,23,24,25,30 (more discussions in Supplementary Note 5), which roughly corresponds to the top of the P1–P2 phonon band. Thus, if Majorana–phonon coupling is present, phonon anomalies are expected in the energy range shown in Fig. 2b. Moreover, a recent theoretical study of the pure Kitaev model predicts that the Majorana–phonon coupling is momentum dependent and peaks near the M and K point28. To uncover the energy and momentum-dependent coupling between the optical phonons and the suggested MFs, we compare the temperature-dependent $$\chi {\prime\prime} ({\bf{q}},\omega )$$ along the M–Γ2 path. A large spectral enhancement can be observed clearly in Fig. 3a–f. Near the M point, the peak intensity of P1 increases dramatically upon cooling from 300 K to 10 K. In contrast, the peak intensity of P2 is unchanged except the 10 K data at the M point. When approaching the Γ2 point (towards larger |q|), the intensity enhancement first decreases near the crossing-point (P1 and P2 crossed at q = 0.75), but then reappears at P2, which is higher in energy near the Γ2 point. Interestingly, we find that the spectral enhancement is different between the symmetry related points q = 0.45 and q = 0.55. As we show in Fig. 2a, the transverse acoustic phonon starts to merge with the optical phonon near the M point. Since the acoustic phonon intensity is stronger at q = 0.45, the asymmetric intensity enhancement suggests that the Majorana–phonon coupling is larger on the acoustic mode than the optical mode near $$\omega \sim {J}_{K}$$. To quantitatively show the spectral enhancement effect, we extract the temperature-induced difference in the integrated phonon intensity, $$\Delta \chi {\prime\prime} ({\bf{q}},{\omega }_{0})={\int }_{{\omega }_{0}-\infty }^{{\omega }_{0}+\infty }[\chi {\prime\prime} ({\bf{q}},\omega ,10{\rm{K}})-\chi {\prime\prime} ({\bf{q}},\omega ,300{\rm{K}})]d\omega$$, and plot $$\Delta \chi {\prime\prime} ({\bf{q}},{\omega }_{0})$$ as function of $$\Delta E={\omega }_{0}-{\omega }_{{{\max }}}$$ in Fig. 3g. Here $${\omega }_{0}$$ denotes the phonon peak position and $${\omega }_{max}=7$$ meV is the band-top energy of P1 and P2. Unlike the broad continuum observed in the spin correlation function17,18,19,21,22,23, $$\Delta \chi ({\bf{q}},{\omega }_{0})$$ decreases rapidly as $${\omega }_{0}$$ moves away from JK (Fig. 3). It also shows strong momentum dependence with the enhancement occuring around the high symmetry points M and Γ2 (see Supplementary Fig. 9). This observation is in qualitative agreement with theoretical calculation that shows energy and momentum dependent Majorana–phonon coupling28 (spectrum near the K point with spectral peak at higher energy is shown in Supplementary Fig. 6). The observed phonon enhancement is also consistent with a recent study of frustrated magnetic systems, which predicts large IXS cross-section for magnetic excitations7. We note, however, a quantitative understanding of the energy and momentum-dependent optical phonon enhancement may require theoretical calculations beyond the pure Kitaev model.

We then turn to the transverse acoustic phonon near Γ1. Figure 4a and b show the temperature-dependence of $$\chi {\prime\prime} ({\bf{q}},\omega )$$ at q1 = (0, 0.1, 0) (or Q1 = (6, −2.9, 0)) and q2 = (0, 0.15, 0) (or Q2 = (6, −2.85, 0)), respectively. At q1, the phonon peak position gradually shifts to lower energies. In contrast, it remains nearly unchanged at q2. The softening-effect is confirmed by directly comparing the raw data, $$S({\bf{q}},\omega )$$, at 10 and 300 K (Fig. 4c and d). The peak position is softened by about 13% at q1, which corresponds to ~0.3 meV shift in energy. Figures 4e and f show the relative peak shift $${\omega }_{0}(T)/{\omega }_{0}(300\,{\rm{K}})$$ at q1 and q2 as function of temperature. We find that the acoustic phonon softening at q1 becomes progressively stronger below 80 K, consistent with the thermal Hall effect in α-RuCl3 where the thermal Hall conductivity, κxy, starts to increase. In Fig. 4e, we further show the phonon softening at q3 = (0, 0.05, 0). The error-bars returned from fittings are larger at q3 as the elastic intensity becomes stronger when approaching the Bragg peak. Interestingly, the relative phonon softening at q3 (~15%) is even larger when compared to q1. This suggests an enhanced renormalization for long wavelength acoustic phonons.

## Discusson

The discovery of temperature and energy dependent phonon softening provides important information on the FPC in α-RuCl3. In the pure Kitaev model [Eq. (1)], quantum fractionalization occurs at TK ~ JK ~100 K43, in agreement with our observations. Below TK, the dispersionless gauge flux excitation crosses the linear dispersing acoustic phonon near $$\omega =0.065{J}_{K} \sim 0.5$$ meV23 and induces a phonon anomaly near this energy scale (Fig. 4g). The observation of enhanced phonon softening [$$\omega ({{\bf{q}}}_{1})=2$$ meV and $$\omega ({{\bf{q}}}_{3})=$$ 1 meV as $$\omega \to 0.065{J}_{K}$$ is consistent with this picture, where the softening effect is expected to be significantly suppressed for $$\omega ({\bf{q}})\gg 0.065{J}_{K}$$. Figure 4h depicts another scenario that attempts to explain the phonon-softening. Here, the acoustic phonon and the itinerant MFs possess nearly identical linear dispersions at $${\bf{q}}\to 0$$29. This enhances Majorana–phonon coupling that yields a renormalization of the phonon dispersion below TK28,29. To justify this conjecture, we extract the acoustic phonon velocity $${v}_{{\rm{ph}}} \sim$$16 meV Å ($$\hslash =1$$), which is based on the room-temperature phonon dispersion shown in Fig. 2. In the isotropic limit16, the velocity of the itinerant MF is $${v}_{{\rm{MF}}}=\frac{\sqrt{3}}{4}{J}_{K}a$$, where the in-plane lattice constant $$a=5.9639$$ Å. Comparing $${v}_{{\rm{ph}}}$$ and $${v}_{{\rm{MF}}}$$ gives $${J}_{K}$$ ~ 6.2 meV, comparable to the experimental value. Besides the Z2 gauge flux and MFs, in more realistic models with non-Kitaev interactions44,45, other fractional excitations may also be consistent with the observed phonon anomalies. It is important to note that the charge and magnetic excitations below 2 meV still remain unresolved in α-RuCl3. In particular, direct experimental evidence of Z2 gauge flux is not well established yet. The observed acoustic phonon softening below 2 meV demonstrate a small energy scale in α-RuCl3 that strongly renormalizes the acoustic phonon spectrum and hence may be responsible for the quantized thermal Hall effect.

Finally, we discuss the possibility of magnon–phonon coupling. Below TN, a gapped magnon excitation between 2–7 meV was observed in α-RuCl3 by previous neutron studies19,21,22,37. However, as we show in Figs. 3 and 4, the phonon anomalies onset at TK, which is well above TN. More importantly, evidence of an enhanced phonon softening is observed at ω =1 meV (see q3 in Fig. 4e and Supplementary Fig. 5), which is well below the magnon gap. Therefore, a magnon–phonon coupling is unlikely giving rise to the observed acoustic phonon softening. However, the magnon–phonon coupling may indeed be present in α-RuCl3. As we show in Fig. 2, the P2 phonon energy is the same as the magnon energy near the M point19,21,38. Interestingly, the P2 phonon intensity at the M point is enhanced at 10 K~TN, supporting magnon–phonon coupling46. In addition, strong anharmonicity is proposed in the magnon excitation of this material47, which represents the break-down of the spin quasiparticles. Such excitations contain extremely broad features47 that are contradictory to the well-defined energy scale of the phonon anomalies observed here.

Our discovery of two-types of phonon anomalies, i.e., the spectral enhancement in the optical phonon and the acoustic mode softening, provides experimental signature of FPC in the proximity of Kitaev-QSL26,27. Beyond the aforementioned implications, our observation has an even deeper impact on correlated topological quantum states. First of all, our approach can be immediately applied to other Kitaev-QSL candidates1,3,4, such as iridates4,48, where the inelastic neutron scattering experiments are difficult to perform due to strong neutron absorption of Ir. Moreover, it has been predicted that in U(1) spin liquids the spinon Fermi surface features a large singularity at 2kF, which induces phonon anomalies at q = 2kF12. Both kagome and triangular lattices have been speculated to host such charge neutral Fermi surfaces49,50. More recently, a giant thermal Hall effect has been observed in the cuprate high-Tc superconductors13 with large phonon contributions51. While mechanisms based on chiral spin liquid or topological spinons14,15 have also been proposed, the theoretically predicted κxy is 50% smaller than the experimental value14, suggesting large phonon effect. Our observation of FPC in α-RuCl3 validates phonons as a sensitive probe to uncover hidden fractional and non-local excitations, and hence can help resolving key puzzles in correlated and entangled quantum states.

## Methods

### Sample preparation and characterizations

Millimeter-sized α-RuCl3 crystals were grown by the sublimation of RuCl3 powder sealed in a quartz tube under vacuum52. The growth was performed in a box furnace. After dwelling at 1060 °C for 6 h, the furnace was cooled to 800 °C at 4 °C/h. Magnetic order was confirmed to occur at 7 K by measuring magnetic properties and specific heat21.

### Inelastic X-ray scattering

The experiments were conducted at beam line 30-ID-C (HERIX) at the Advanced Photon Source (APS). The highly monochromatic X-ray beam of incident energy Ei = 23.7 keV (l = 0.5226 Å) was focused on the sample with a beam cross section of 35 × 15 mm2 (horizontal × vertical). The total energy resolution of the monochromatic X-ray beam and analyzer crystals was ΔE 1.3 meV (full width at half maximum). The measurements were performed in transmission geometry. Typical counting times were in the range of 30–120 s per point in the energy scans at constant momentum transfer Q. H, K, L are defined in the trigonal structure with a = b = 5.9639 Å, c = 17.17 Å at the room temperature.

### Density functional theory calculations of phonon spectrum

Phonon dispersions for α-RuCl3 were calculated using with density functional perturbation theory (DFPT) and the Vienna Ab initio Simulation Package (VASP). The exchange-correlation potential was treated within the generalized gradient approximation (GGA) of the Perdew-Burke-Ernzerhof variety, where the kinetic energy cutoff was set to 400 eV. Integration for the Brillouin zone was done by using a Monkhorst-Pack k-point grids which is equivalent to 8 × 8 × 9.

## Data availability

The data that support the findings of this study are available from the corresponding author on reasonable request.

## References

1. Balents, L. Spin liquids in frustrated magnets. Nature 464, 199–208 (2010).

2. Wen, X.-G. Choreographic entanglement dances: topological states of quantum matter. Science 363, 834 (2019).

3. Broholm, C. et al. Quantum spin liquid. Science 367, 263 (2020).

4. Takagi, H. et al. Concept and realization of Kitaev quantum spin liquids. Nat. Rev. Phys. 1, 246 (2019).

5. Tang, E., Mei, J.-W. & Wen, X.-G. High-temperature fractional quantum Hall states. Phys. Rev. Lett. 106, 236802 (2011).

6. Bradlyn, B. et al. Topological quantum chemistry. Nature 547, 298 (2017).

7. Toth, S. et al. Electromagnon dispersion probed by inelastic x-ray scattering in LiCrO2. Nat. Commun. 7, 13547 (2016).

8. Pouget, J. P. et al. Neutron-scattering investigations of the Kohn anomaly and of the phase and amplitude charge density wave excitations of the blue bronze K0.3MoO3. Phys. Rev. B 43, 8421 (1991).

9. Hoesch, M. et al. Giant Kohn anomaly and the phase transition in charge density wave ZrTe3. Phys. Rev. Lett. 102, 086402 (2009).

10. Miao, H. et al. Incommensurate phonon anomaly and the nature of charge density waves in cuprates. Phys. Rev. X 8, 011008 (2018).

11. Aynajian, P. et al. Energy gaps and Kohn anomalies in elemental superconductors. Science 319, 1509 (2008).

12. Mross, D. F. & Senthil, T. Charge Friedel oscillations in a Mott insulator. Phys. Rev. B 84, 041102 (2011).

13. Grissonnanche, G. et al. Giant thermal Hall conductivity in the pseudogap phase of cuprate superconductors. Nature 376, 571 (2019).

14. Samajdar, R. et al. Enhanced thermal Hall effect in the square-lattice Néel state. Nat. Phys. 15, 1290 (2019).

15. Han, J. H., Park, J.-H. & Lee, P. A. Consideration of thermal Hall effect in underdoped cuprates. Phys. Rev. B 99, 205157 (2019).

16. Kitaev, A. Anyons in an exactly solved model and beyond. Ann. Phys. 321, 2 (2006).

17. Sandilands, L. J., Tian, Y., Plumb, K. W., Kim, Y.-J. & Burch, K. S. Scattering continuum and possible fractionalized excitations in α-RuCl3. Phys. Rev. Lett. 114, 147201 (2015).

18. Nasu, J., Knolle, J., Kovrizhin, D. L., Motome, Y. & Moessner, R. Fermionic response from fractionalization in an insulating two-dimensional magnet. Nat. Phys. 12, 912–915 (2016).

19. Banerjee, A. et al. Proximate Kitaev quantum spin liquid behaviour in a honeycomb magnet. Nat. Mat. 15, 733–740 (2016).

20. Hermanns, M. et al. Physics of the Kitaev model: fractionalization, dynamic correlations, and material connections. Annu. Rev. Condens. Matter Phys. 9, 17–33 (2017).

21. Banerjee, A. et al. Neutron scattering in the proximate quantum spin liquid α-RuCl3. Science 356, 1055–1059 (2017).

22. Do, S.-H. et al. Majorana fermions in the Kitaev quantum spin system α -RuCl3. Nat. Phys. 13, 1079–1084 (2017).

23. Jansa, N. et al. Observation of two types of fractional excitation in the Kitaev honeycomb magnet. Nat. Phys. 14, 786 (2018).

24. Widmann, S. et al. Thermal dynamic evidence of fractionalized excitations in α−RuCl3. Phys. Rev. B 99, 094415 (2019).

25. Laurell, P. & Okamoto, S. Dynamical and thermal magnetic properties of the Kitaev spin liquid candidate α-RuCl3. npj Quantum. Materials 5, 2 (2020).

26. Ye, M., Halász, G. B., Savary, L. & Balents, L. Quantization of the thermal Hall conductivity at small Hall angles. Phys. Rev. Lett. 121, 147201 (2018).

27. Vinkler-Aviv, Y. & Rosch, A. Approximately quantized thermal Hall effect of chiral liquids coupled to phonons. Phys. Rev. X 8, 031032 (2018).

28. Metavitsiadis, A. & Brenig, W. Phonon renormalization in the Kitaev quantum spin liquid. Phys. Rev. B 101, 035103 (2020).

29. Ye, M. et al. Phonon dynamics in the Kitaev spin liquid. Phys. Rev. Res. 2, 033180 (2020).

30. Kasahara, Y. et al. Majorana quantization and half-integer thermal quantum Hall effect in a Kitaev spin liquid. Nature 559, 227–231 (2018).

31. Yamashita, M., Kurita, N. & Tanaka, H. Sample dependence of the half-integer quantized thermal Hall effect in the Kitaev candidate α-RuCl3. Phys. Rev. B 102, 220404 (2020).

32. Nasu, J., Yoshitake, J. & Motome, Y. Thermal transport in the Kitaev model. Phys. Rev. Lett. 119, 127204 (2017).

33. Jackeli, G. & Khaliullin, G. Mott insulators in the strong spin-orbit coupling limit: from Heisenberg to a quantum compass and Kitaev models. Phys. Rev. Lett. 102, 017205 (2009).

34. Yoshitake, J. et al. Fractional spin fluctuations as a precursor of quantum spin liquids: Majorana dynamical meanfield study for the Kiteav model. Phys. Rev. Lett. 117, 157203 (2016).

35. Leahy, I. A. et al. Anomalous thermal conductivity and magnetic torque response in the honeycomb magnet α-RuCl3. Phys. Rev. Lett. 118, 187203 (2017).

36. Hentrich, R. et al. Unusual phonon heat transport in α-RuCl3: strong spin-phonon scattering and field-induced spin gap. Phys. Rev. Lett. 120, 117204 (2018).

37. Kasahara, Y. et al. Unusual thermal Hall effect in a Kitaev spin liquid candidate α-RuCl3. Phys. Rev. Lett. 120, 217205 (2018).

38. Banerjee, A. et al. Excitations in the field-induced quantum spin liquid state of α-RuCl3. njp Quantum Mater. 3, 8 (2018).

39. Balz, C. et al. Finite field regime for a quantum spin liquid in α-RuCl3. Phys. Rev. B 100, 060405 (2019).

40. Reschke, S. et al. Terahertz excitations in α-RuCl3: Majorana fermions and rigid-plane shear and compression modes. Phys. Rev. B 100, 100403(R) (2019).

41. Miao, H. et al. Observation of double Weyl phonons in parity breaking FeSi. Phys. Rev. Lett. 121, 035302 (2018).

42. Zhang, T. T. et al. Phononic helical nodal lines with PT protection in MoB2. Phys. Rev. Lett. 123, 245302 (2019).

43. Yoshitake, J., Masu, J. & Motome, Y. Fractional spin fluctuations as a precursor of quantum spin liquids: Majorana dynamical mean-field study for the Kitaev model. Phys. Rev. Lett. 117, 157203 (2016).

44. Rusnačko, J., Gotfryd, D. & Chaloupka, J. Kitaev-like honeycomb magnets: global phase behavior and emergent effective models. Phys. Rev. B 99, 064425 (2019).

45. Hickey, C. & Trebst, S. Emergence of a field-driven U(1) spin liquid in the Kitaev honeycomb model. Nat. Commun. 10, 530 (2019).

46. Teng, Y. et al. Unquantized thermal Hall effect in quantum spin liquids with spinon Fermi surfaces. Phy. Rev. Research 2, 033283 (2020).

47. Winter, S. M. et al. Breakdown of magnons in a strongly spin-orbital coupled magnet. Nat. Commun. 8, 1152 (2017).

48. Kitagawa, K. et al. A spin-orbital-enhanced quantum liquid on a honeycomb lattice. Nature 554, 341 (2018).

49. Han, T.-H. et al. Fractionalized excitations in the spin-liquid state of a kagome-lattice antiferromagnet. Nature 492, 406 (2012).

50. Shen, Y. et al. Evidence for a spinon Fermi surface in a triangular-lattice quantum-spin-liquid candidate. Nature 540, 559 (2016).

51. Grissonnanche, G. et al. Chiral phonons in the pseudogap phase of cuprates. Nat. Phys. 16, 1108 (2020).

52. May, A. F. et al. A practical guide for crystal growth of van der Waals layered materials. Journal of Applied Physics 128, 051101 (2020).

## Acknowledgements

We thank T. Berlijn, H. Ding, J. K. Keum, G. Kotliar, S. Nagler, N. Perkins, and A. Tennant for stimulating discussions. This research at Oak Ridge National Laboratory (ORNL) was sponsored by the U.S. Department of Energy, Office of Science, Basic Energy Sciences, Materials Sciences and Engineering Division (IXS data analysis, material synthesis and data interpretation) and by the Laboratory Directed Research and Development Program of ORNL, managed by UT-Battelle, LLC, for the U.S. Department of Energy (IXS experiment). Part of IXS data interpretation work at Brookhaven National Laboratory was supported by the U.S. DOE, Office of Science, Office of Basic Energy Sciences, Materials Sciences, and Engineering Division under Contract No. DE-SC0012704. This research used resources of the Advanced Photon Source, a U.S. Department of Energy (DOE) Office of Science User Facility, operated for the DOE Office of Science by Argonne National Laboratory under Contract No. DE-AC02-06CH11357. Extraordinary facility operations were supported, in part, by the DOE Office of Science through the National Virtual Biotechnology Laboratory, a consortium of DOE national laboratories focused on the response to COVID-19, with funding provided by the Coronavirus CARES Act. T.T.Z. and S.M. acknowledge the supports from Tokodai Institute for Element Strategy (TIES) funded by MEXT Elements Strategy Initiative to Form Core Research Center. T.T.Z. also acknowledge the support by Japan Society for the Promotion of Science (JSPS), KAKENHI Grant No. 21K13865. S.M. also acknowledges support by JSPS KAKENHI Grant No. JP18H03678. G.B.H. and S.O. were supported by the U.S. Department of Energy, Office of Science, National Quantum Information Science Research Centers, Quantum Science Center. D.G.M. acknowledges support from the Gordon and Betty Moore Foundation’s EPiQS Initiative, Grant GBMF9069.

## Author information

Authors

### Contributions

H. M. conceived and designed the study. H.L., A.S., G.F., D.G.M., J.K.K., H.N.L., M.P.M.D., and H.M. performed the IXS experiment. H.L. and H.M. analyzed the IXS data. T.T.Z., S.M., G.B.H., and S.O. performed the DFT calculations and theoretical analysis. J.Q.Y. and D.M. synthesized the high-quality single crystal samples. H.L., T.T.Z., M.P.M.D., and H.M. prepared the manuscript with inputs from all authors.

### Corresponding author

Correspondence to H. Miao.

## Ethics declarations

### Competing interests

The authors declare no competing interests.

Peer review information Nature Communications thanks the anonymous reviewers for their contribution to the peer review of this work.

Publisher’s note Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.

## Rights and permissions

Reprints and Permissions

Li, H., Zhang, T.T., Said, A. et al. Giant phonon anomalies in the proximate Kitaev quantum spin liquid α-RuCl3. Nat Commun 12, 3513 (2021). https://doi.org/10.1038/s41467-021-23826-1

• Accepted:

• Published:

• DOI: https://doi.org/10.1038/s41467-021-23826-1